System Level Formal Verification as a Service
SyLVaaS is a Web-based service allowing System Level Formal Verification (SLFV) of Cyber Physical Systems (CPSs).
SyLVaaS takes as input a disturbance model (which model failures in sensors or actuators, variations in the system parameters, etc.) and effectively computes the set of simulation campaigns (sequences of simulation instructions, which exploit the capabilities of moderns simulators to: save a simulation state, restore a saved simulation state, inject a disturbance, advance the simulation for a given time length) to be used for a parallel Hardware-In-the-Loop Simulation (HILS) based SLFV on the user premises.
The following picture synthesises SyLVaaS workflow.
Points 1 to 3 are carried out on the SyLVaaS cloud, without knowledge of the CPS modelling.
Point 4 is carried out on the user premises, by using the general purpose Simulink driver available at the SyLVaaS tools page.
The main features of SyLVaaS can be summarised in the following points: Protection of the System Under Verification (SUV) Intellectual Property (IP); Protection of the Verification Flow IP; Fast Response Time via Parallel Computation.
SyLVaaS introduces the new Verification as a Service (VaaS) paradigm, allowing verification engineers (SyLVaaS users) to use an external (Web) service (SyLVaaS) to compute the simulation campaigns needed for their HILS based SLFV activities, without actually sending around neither the System Under Verification (SUV) model nor the property to be verified.
Of course, such an IP protection is mandatory for a VaaS service to be actually usable, since companies, of course, consider the CPS design (hence the SUV model) an important (IP) asset.
To enable IP protection, SyLVaaS takes as input only a disturbance model defined as a CMurphi model describing the admissible operational scenarios the SUV must withstand. The actual verification activity is performed in parallel at the user premises (e.g., on a private cluster) running an arbitrarily large set of Simulink simulators, using the optimised simulation campaigns computed by SyLVaaS and plugging-in a Simulink driver downloadable from the SyLVaaS tools page.
In case an error is found during the verification activity, a counterexample is generated. Such a counterexample can then be used to revise the SUV, thereby producing a new SUV model. At this point a new SLFV activity can start. Note that, given that the set of admissible operational scenarios (hence: the disturbance model) has not changed, there is no need to interact with SyLVaaS again, as the previously computed simulation campaigns can be reused. This property hides the verification flow of SyLVaaS users to outsiders.
In order to achieve a fast response time, SyLVaaS uses a novel parallel algorithm for the generation of operational scenarios from a disturbance model.