SyLVer

Details
Category: Software
Last Updated on Wednesday, 01 February 2017 12:15

SyLVer [MicPro16,PDP15,PDP14,CAV13,SpaceOps12,DASIA11] is a software allowing System Level Formal Verification (SLFV) of Cyber Physical Systems (CPSs). SyLVer implements an assume-guarantee approach to the problem of 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.

SyLVer is a stand-alone software completely running on the user premises. Furtherly, it is possible to exploit MCLab Group cloud infrastructure potential for SyLVer, by using our derived and dedicated Web-based software SyLVer as a Service (SyLVaaS). With SyLVaaS, the generation of relevant scenarios is executed in MCLab cloud infrastructure but HILS activity still takes place on the user premises (as for SyLVer), thus allowing full Intellectual Property protection on the SUV model and the user verification flow.

SyLVer takes as input a high-level model defining the SUV operational environment and computes 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 separately downloadable from BitBucket repository sylver-simulink-driver.

The simulation campaigns computed by SyLVer 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.

Start enjoying SyLVer by connecting to Docker hub SyLVer page.