The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variation in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment. In this paper, we present SyLVaaS, a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assumeguarantee approach to the verification problem outlined above. SyLVaaS takes as input a high-level model defining the 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, using a platform independent Simulink driver downloadable from the SyLVaaS Web site. 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. The simulation campaigns computed by SyLVaaS randomise the verification order of operational scenarios and this enables, at anytime during the parallel simulation activity, the estimation of the completion time and the computation of an upper bound to the Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario which violates the property under verification. This information supports graceful degradation in the verification activity. We show effectiveness of the SyLVaaS algorithms and infrastructure by evaluating the system on industry-scale input related to the verification of the Fuel Control System (FCS) model in the Simulink distribution.

SyLVaaS: system level formal verification as a service / Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico. - STAMPA. - (2015). (Intervento presentato al convegno 23rd Euromicro International Conference on Parallel, distributed and network-based Processing (PDP 2015) tenutosi a Turku) [10.1109/PDP.2015.119].

SyLVaaS: system level formal verification as a service

MANCINI, Toni;MARI, FEDERICO;MASSINI, Annalisa;MELATTI, IGOR;TRONCI, Enrico
2015

Abstract

The goal of System Level Formal Verification is to show system correctness notwithstanding uncontrollable events (disturbances), as for example faults, variation in system parameters, external inputs, etc. This may be achieved with an exhaustive Hardware In the Loop Simulation based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment. In this paper, we present SyLVaaS, a Web-based tool enabling Verification as a Service (VaaS). SyLVaaS implements an assumeguarantee approach to the verification problem outlined above. SyLVaaS takes as input a high-level model defining the 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, using a platform independent Simulink driver downloadable from the SyLVaaS Web site. 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. The simulation campaigns computed by SyLVaaS randomise the verification order of operational scenarios and this enables, at anytime during the parallel simulation activity, the estimation of the completion time and the computation of an upper bound to the Omission Probability, i.e., the probability that there is a yet-to-be-simulated operational scenario which violates the property under verification. This information supports graceful degradation in the verification activity. We show effectiveness of the SyLVaaS algorithms and infrastructure by evaluating the system on industry-scale input related to the verification of the Fuel Control System (FCS) model in the Simulink distribution.
2015
23rd Euromicro International Conference on Parallel, distributed and network-based Processing (PDP 2015)
Hybrid systems; Verification; hybrid automaton
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
SyLVaaS: system level formal verification as a service / Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico. - STAMPA. - (2015). (Intervento presentato al convegno 23rd Euromicro International Conference on Parallel, distributed and network-based Processing (PDP 2015) tenutosi a Turku) [10.1109/PDP.2015.119].
File allegati a questo prodotto
File Dimensione Formato  
Mancini_Sylvass_2015.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 834.53 kB
Formato Adobe PDF
834.53 kB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/645263
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 36
  • ???jsp.display-item.citation.isi??? 20
social impact