SyLVer Disturbance Model v. 1.0

System Level Formal Verification (SyLVer) Disturbance Model v 1.0 is distributed under the MIT License. This software is used for SyLVer and SyLVaaS applications.

Before using SyLVer Disturbance Model, read the following notes.

Notes on Disturbance Model

Any model can be disturbed by external signals. Independently from the model and surrounding environment, for the sake of simplicity we can classify disturbances in failures and model parameter change not representing a failure.

We call faults disturbances representing failures. We call inputs disturbances representing change in model parameters. Since a system is not expected to work normally when subject to failures, we consider faults as recoverable disturbances.

Thanks to considerations above, we can write a generic disturbance model, which can be instantiated for different systems by changing parameters on disturbances.

We choose the model checker CMurphi input language (describing FSMs in procedural way) for describing the disturbance model.

Parameters for disturbances are set in model Const section. They are as follows.

  • The discretization step depends on TICKS_PER_SECOND. As an example, if TICKS_PER_SECOND is 2, it means that there are two discrete ticks per second, making the discretization step equal to 0.5 seconds. Note that when using this disturbance model to generate traces for SyLVer Simulink Driver, the discretization step (0.5 in the example above) must be supplied to the driver via appropriate option, since this is required when reading RUN commands in the simulation campaign.
  • The number of faults in the model is NUM_FAULTS. The time after which a fault is recovered is called REMOVE_FAULT_TIME. We do not allow more than MAX_NUM_OF_FAULTS faults within a trace. Moreover, faults can be simoultaneous but we do not allow more than MAX_NUM_OF_ACTIVE_FAULTS faults active simultaneously.
  • The number of inputs in the model is NUM_INPUTS. We do not allow more than MAX_NUM_OF_INPUTS faults within a trace. For limiting state explosion in trace generation, we allow inputs variation only at time multiple of INJECT_INPUT_PERIOD seconds.

Note that from the disturbance model point of view, it is enough for the service provider to set parameters to values. The correspondence between fault and Simulink meaning is only known by the modeller.


SyLVer Disturbance Model is a Shell program generating to stdout a disturbance model written in CMurphi modelling language.

Options are:

  • -t arg number of ticks per second
  • -f arg total number of faults
  • -g arg maximum number of faults within a trace
  • -e arg maximum number of simultaneously active faults
  • -r arg fault duration in seconds
  • -i arg total number of inputs
  • -j arg maximum number of inputs in a trace
  • -k arg inputs can be injected in seconds multiple of arg
  • -l arg disturbances can be injected after arg ticks

Option -h prints the help and exits. No option is mandatory. Defaults of each option can be read in the output of help.

$ sh -h

Generates Disturbance Model for SyLVer in CMuphi procedural language.

 Usage: [options]
        [-t ticks-per-second]
        [-f number-of-faults]
        [-g max-number-of-faults-in-trace]
        [-e max-number-of-active-faults-in-same-moment]
        [-r fault-duration-in-seconds]
        [-i number-of-inputs]
        [-j max-number-of-inputs-in-trace]
        [-k seconds-multiple-of-which-inputs-can-be-injected]
        [-l seconds-after-which-to-inject-disturbaces]

 Disturbances can be 1) faults or 2) input variations.
 1) Faults are considered as temporary (in order not to destroy the system)
 2) Inputs are permanent variations to the system.

Ticks per second (-t arg) . . . . . . . . . . . . . . : 2
Total number of faults (-f arg) . . . . . . . . . . . : 4
Max number of faults in a trace (-g arg). . . . . . . : 2
Max number of simultaneously active faults (-e arg) . : 1
Fault duration in seconds (-r arg). . . . . . . . . . : 1
Total number of inputs (-i arg) . . . . . . . . . . . : 1
Max number of inputs in a trace (-j arg). . . . . . . : 1
Inputs can be injected in seconds multiple of (-k arg): 2.0
Disturbances can be injected after seconds (-l arg) . : 0.0