SyLVaaS

Details
Category: Software
Last Updated on Friday, 23 December 2016 15:36

SyLVaaS [MicPro16,PDP15,PDP14,CAV13,SpaceOps12,DASIA11] is a Web-based tool enabling execution of SyLVer as a Service. SyLVaaS, as its master software SyLVer, implements an assume-guarantee approach to the problem of System Level Formal Verification (SLFV).

The goal of SLFV 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 (HILS) based approach, by considering all relevant scenarios in the System Under Verification (SUV) operational environment.

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 SyLVer Simulink Driver, delivered together with SyLVer, or SyLVaaS, or separately downloadable from BitBucket repository sylver-simulink-driver.

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.

Effectiveness of the SyLVaaS algorithms and infrastructure is shown in [PDP15] by evaluating the system on industry-scale input related to the verification of the Fuel Control System (FCS) model in the Simulink distribution.