Public Repository

Last pushed: 2 months ago
Short Description
SyLVer is a software performing Bounded System Level Formal Verification of Cyber-Physical Systems
Full Description

Supported tags

  • 1.0.1-alpine
  • 1.0.0-alpine

What is SyLVer?

SyLVer is a software performing Bounded System Level Formal Verification (SLFV) of Cyber-Physical Systems (CPSs).

SyLVer takes as input a disturbance model for the CPS at hand, modelling the CPS operational environment (in terms of, e.g., failures in sensors or actuators, variations in the system parameters, etc.) that the system should withstand.

SyLVer output consists in a set of simulation campaigns, i.e., sequences of simulation instructions that be used to drive a simulator in order to perform parallel Hardware-In-the-Loop Simulation (HILS) based SLFV of the CPS at hand, checking that desired properties (modelled as monitors within the CPS model) hold.

Simulation campaigns computed by SyLVer are highly optimised, as they exploit capabilities of modern simulators to:

  • Save a simulation state
  • Restore a saved simulation state
  • Inject a disturbance
  • Run simulation for a given duration.

SyLVer already offers a driver to execute the computed simulation campaigns in Simulink. Drivers for other simulators (offering the features above) can be easily developed.

SyLVer Workflow

SyLVer takes as input a Disturbance Model, which describes the admissible operational scenarios the System Under Verification (SUV) (composed by the CPS together with a monitor checking for desired properties) must withstand.

The disturbance model is defined as a Finite State Machine (FSM) representing all sequences (of a given finite length h, horizon) of disturbances (including 'no disturbance') admissible in the SUV operational environment.

SyLVer takes as input disturbance models defined in the CMurphi high-level input modelling language.

Given a disturbance model and a value for h (horizon), SyLVer:

  1. Generates the entire set of admissible disturbance sequences from the disturbance model
  2. Evenly splits such a set into k (a positive integer number) slices, in order to enable parallel verification
  3. Computes (in parallel) and returns an optimised simulation campaign from each slice.

The k generated simulation campaigns can be finally executed (in parallel) on a set of k independent simulator (e.g., Simulink) instances.

How to Use This Image

This docker image provides the following commands:

  1. Run the complete SyLVer Workflow;
  2. Run SyLVer step-by-step;
  3. Automatically generate a sample disturbance model from parameters.

Run the Complete SyLVer Workflow

To compute the set of simulation campaigns from disturbance model 'model.m' stored in folder 'folder/', run the following command:

docker run --rm -it -v $PWD/folder:/folder mclab/sylver sylver --input /folder/model.m --output /folder/ --memory <memory> [--n <num. cores>] --h <horizon> --k <num. sim. campaigns> [--simMemory <sim. memory>] [--shuffle]

Possible arguments are the following:

  • --input, the filepath of the disturbance model, which must end with '.m'

  • --output, the desired output directory

  • --memory, the amount of memory (in MB) available to SyLVer

  • --n, the number of cores available to SyLVer for parallel computation (optional, default 1)

  • --h, the horizon of disturbance traces entailed by the disturbance model

  • --k, the number of simulation campaigns to be computed, which can then be run in parallel

  • --simMemory, the max number of states that can be kept simultaneously stored by the simulator (0 means 'no limits')

  • --shuffle, a flag which, if given, randomises traces verification order.

The command above returns in the output folder the sylver-simulink-driver which contains:

  • Disturbances dictionary file (dictionary.txt)
  • Subfolder containing all simulation campaigns (simulation-campaigns/)
  • MATLAB scripts *.m containing the core code of driver
  • Bash program run.sh which is the entry point for running simulation campaigns
  • Python program to post-process execution times log file (simulator_driver_split_times_log_in_separate_files.py).

Please refer to file README.md in the output folder for full instructions on how to use the driver to run your k simulation campaigns on k parallel Simulink instances.

A non-customised version of the SyLVer Simulink Driver can also be downloaded from the SyLVer Simulink Driver repository.

Run SyLVer Step-by-Step

The following sections describe additional commands of this docker image that allow you to run each SyLVer workflow step separately.

1. Generating Disturbance Traces from a Disturbance Model

To compute the set of disturbance traces entailed by disturbance model 'model.m' stored in folder 'folder/', run the following command:

docker run --rm -it -v $PWD/folder:/folder mclab/sylver generator --input /folder/model.m --output /folder/traces.bin --memory <memory> --h <horizon>

Besides file 'folder/traces.bin', the command returns a dictionary file which maps disturbance numbers to mnemonic labels. This file will be needed in the last step of the SyLVer workflow (i.e., execution of simulation campaigns with the SyLVer Simulink driver).

Arguments for the command above are the following:

  • --input, the filepath of the disturbance model, which must end with '.m'

  • --output, the filepath of the file containing the disturbance traces

  • --h, the length of the produced disturbance traces (horizon)

  • --memory, the amount of memory (in MB) available to the generator.

2. Splitting Disturbance Traces into Slices

To evenly split disturbance traces stored in file 'folder/traces.bin' into k slices (which would enable parallel simulation on k independent Simulink instances), run the following command:

docker run --rm -it -v $PWD/folder:/folder mclab/sylver splitter --input /folder/traces.bin --output /folder/slice_*_of_*.bin --k <k>

Arguments for the command above are the following:

  • --input, input trace filepath

  • --k, the number of output slices to be produced

  • --output, a template filepath for the the output slices, containing one or two occurrences of '': the first will be expanded to the slice number (1, 2, ..., k); the second * (if present) will be expanded to value k.

3. Computing an Optimised Simulation Campaign

To compute the optimised simulation campaign from file 'folder/traces.bin' of disturbance traces (e.g., a file created by the generator in point 1 or a slice thereof as created by the splitter in point 2), run the following command:

docker run --rm -it -v $PWD/folder:/folder mclab/sylver optimiser --input /folder/traces.bin --output /folder/simCampaign.txt [--simMemory <simulator memory>] --optMemory <optimiser memory> [--shuffle]

Arguments for the command above are the following:

  • --input, filepath of the input trace file

  • --output, filepath of the output simulation campaign

  • --simMemory, max number of states that can be kept simultaneously stored by the simulator (0 means 'no limits')

  • --optMemory, max memory (in MB) available to the optimiser

  • --shuffle, if given, the trace verification order is randomised, thus enabling computation of omission probability.

Getting the SyLVer Simulink Driver

There are two ways to get the SyLVer Simulink driver:

  1. Download it from our official BitBucket Repository here.

  2. Copy it from the container into folder 'folder/' of your file-system, with the following command:

docker run --rm -it -v $PWD/folder:/folder mclab/sylver cp -r sylver-simulink-driver /folder/

In both cases, you will find complete instructions in file README.

Automatically Generate a Sample Disturbance model from Parameters

If you do not yet master the CMurphy syntax for defining disturbance models, you can automatically generate a sample disturbance model for your SUV starting from a few parameters with the following command:

docker run --rm -it mclab/sylver sylver-disturbance-model [args]

Full details about this command and the allowed arguments can be found in the official SyLVer Disturbance Model repository.

License

Use of SyLVer is granted at no fee for non-commercial purposes. Please contact the authors if you wish to use SyLVer for commercial purposes.

SyLVer is provided under an AS-IS basis and without any guarantee.
The software authors shall never, and without any limit, be liable for any damage, cost, expense or any other payment incurred by the user as a result of the software’s actions, failure, bugs and/or any other interaction between the software and the user end-equipment, computers, other software or any 3rd party, end-equipment, computer or services. Moreover, the authors shall never be liable for any defect in source code written by the user when relying on the software.

Full terms of the SyLVer license are contained in this docker image.

Issues

If you have any problems or questions, please feel free to contact us:

Docker Pull Command
Owner
mclab

Comments (0)