SyLVaaS: System Level Formal Verification as a Service*
Issue title: Special issue of the 22nd RCRA International Workshop on “Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion”
Guest editors: Stefano Bistarelli, Andrea Formisano, Marco Maratea and Paolo Torroni
Affiliations: [a] Computer Science Department, Sapienza University of Rome, Italy {tmancini, mari, massini, melatti, tronci}@di.uniroma1.it
Correspondence:
[†]
Address for correspondence: Computer Science Department, Sapienza University of Rome, Italy
Note: [*] This is an extended and revised version of [1].
Abstract: The goal of System Level Formal Verification is to show system correctness notwithstanding
uncontrollable events (disturbances), as for example faults, variations 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 assume-guarantee approach to (Hardware In the Loop Simulation based)
System Level Formal Verification. SyLVaaS takes as input a finite state automaton 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 (i.e., with no communication among the parallel processes) 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., on a private cluster), SyLVaaS allows full Intellectual Property protection of the SUV model as well as of 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 case studies consisting of input operational environments entailing up to 35 641 501 scenarios related to the system level verification of models from the Simulink distribution (namely, Inverted Pendulum on a Cart and Fuel Control System).
Keywords: Verification as a Service, Model Checking, Hybrid Systems, System Level Fo Verification, Distributed Multi-Core Hardware in the Loop Simulation
