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.
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_SECONDis 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_FAULTSfaults within a trace. Moreover, faults can be simoultaneous but we do not allow more than
MAX_NUM_OF_ACTIVE_FAULTSfaults active simultaneously.
- The number of inputs in the model is
NUM_INPUTS. We do not allow more than
MAX_NUM_OF_INPUTSfaults within a trace. For limiting state explosion in trace generation, we allow inputs variation only at time multiple of
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.
-t argnumber of ticks per second
-f argtotal number of faults
-g argmaximum number of faults within a trace
-e argmaximum number of simultaneously active faults
-r argfault duration in seconds
-i argtotal number of inputs
-j argmaximum number of inputs in a trace
-k arginputs can be injected in seconds multiple of
-l argdisturbances can be injected after
-h prints the help and exits. No option is mandatory. Defaults of each option can be read in the output of help.
$ sh sylver-disturbance-model.sh -h Generates Disturbance Model for SyLVer in CMuphi procedural language. Usage: sylver-disturbance-model.sh [options] Options: [-h] [-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