System Level Formal Verification as a Service

T. Mancini, F. Mari, A. Massini, I. Melatti, E. Tronci

Аннотация


We present SyLVaaS, a Web-based tool enabling Verification as a Service (VaaS) of Cyber-Physical Systems (CPS). SyLVaaS takes as input a high-level model defining the System Under Verification (SUV) operational environment and computes, using parallel algorithms deployed in a cluster infrastructure, a set of highly optimised simulation campaigns, which can be executed in an embarrassingly parallel fashion on a set of Simulink instances, each one defining a copy of the SUV model. As the actual simulation is carried out at the user premises (e.g., in a private cluster), SyLVaaS allows full Intellectual Property protection on the SUV model and the user verification flow. SyLVaaS randomises the verification order of operational scenarios, thus enabling anytime estimation of completion time and computation of Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario violating the property under verification. This information supports graceful degradation in the verification activity.

Ключевые слова


modelled; system; methodology; simulation campaigns

Полный текст:

PDF (English)

Литература


Alur R. “Formal verification of hybrid systems”. In: Proc. EMSOFT (2011), Taipei, Taiwan, 2011, pp. 273-278.

Mancini T., Mari F., Massini A., Melatti I., Merli F., Tronci E. “System level formal verification via model checking driven simulation”. In: Proc. CAV (2013), Saint Petersburg, Russia, 2013, pp. 296-312.

Mancini T., Mari F., Massini A., Melatti I., Tronci E. “Anytime system level verification via random exhaustive hardware in the loop simulation” . In: Proc. DSD (2014), Verona, Italy, 2014, pp. 236-245.

Mancini T., Mari F., Massini A., Melatti I., Tronci E.. “System level formal verification via distributed multi-core hardware in the loop simulation”. In: Proc. PDP (2014), Turin, Italy, 2014, pp. 734-742.

Penna G. Della, Intrigila B., Melatti I., Tronci E., Zilli. M. Venturini “Exploiting transition locality in automatic verification of finite state concurrent systems”. STTT, 2004; 6: 320–341.

Zuliani P., Platzer A., Clarke E.. “Bayesian statistical model checking with application to Simulink/Stateflow verification”. In: Proc. HSCC (2010), Stockholm, Sweden, 2010, pp. 243-252.

Mancini T., Mari F., Massini A., Melatti I., Tronci E. “SyLVaaS: System Level Formal Verification as a Service”. In: Proc. PDP (2015), Turku, Finland, 2015.


Ссылки

  • На текущий момент ссылки отсутствуют.


(c) 2021 T. Mancini, F. Mari, A. Massini, I. Melatti, E. Tronci