Description
This model was taken from the Simulink examples library. A full description of this model can be found on the Simulink web site.
This is a model of a fuel control system where Stateflow(R) is used to handle the fault management of the system. The system contains four separate sensors: a throttle sensor, a speed sensor, an oxygen sensor, and a pressure sensor.
Each of these sensors is represented by a parallel state in Stateflow. Each parallel state contains two substates, a normal state and a failed state (the exception being the oxygen sensor, which also contains a warmup state). If any of the sensor readings is outside an acceptable range, then a fault is registered in Stateflow, and the substate of the corresponding subsystem transitions to the failed state. If a subsystem recovers, it can transition back to the normal state.
A state regulates the oxygen to fuel mixture ratio. If a failure is detected, then the oxygen to fuel ratio is increased. If multiple failures are detected, then the fuel system is disabled until there are no longer multiple failures in the system.
Modelisation for SMC
Important!
Our probabilistic model can be downloaded here:- Plasma project: sldemo_fuelsys.plasma
- Simulink model: sldemo_fuelsys_estasys.mdl
To execute the model you will need to build the S-Function Builder in Simulink:
- Locate the S-Function Builder block in the block “Speed Sensor/Poisson”
- Right click on “Properties”
- Launch “Build”
In the original model, sensors’ faults are decided by the user using manual switch block for each sensor. The interest of the SMC approach come from the possibility to observe a large set of execution trace produced by a probabilistic procedure.
A general view of the probabilistic model
To do this we replaced Speed, EGO and MAP manual switches by custom probabilistic switches. These switches use a Poisson distribution and are parameterized by a rate to decide when a fault happen. A sensor will repair itself after a duration of 1 second. Although we modified the original model ourselves, we used the description of the probabilistic model from Bayesian Statistical Model Checking with Application to Stateflow/Simulink Verification (Zuliani, Platzer, Clarke).
Poisson distribution block
The Poisson distribution block draw a time T in second before the next fault happen and use a Stateflow chart as a timer. Once the time T is reached, the block emit a signal corresponding to a fault. In this block, the S-Function block call the C function rand. We had to use C to overcome the lack of equivalent random block in Simulink.
The probabilistic switch with repair timer
The signal from the Poisson block is then used in a switch. In case of a fault signal the fault value (a constant) is returned instead of the sensor value. A Stateflow repair timer is used to maintain the fault signal for a duration of 1 second.
fuel and airflow/fuel rates
Statistical Model Checking we checked the property already used in the paper Bayesian Statistical Model Checking with Application to Stateflow/Simulink Verification (Zuliani, Platzer, Clarke).
Important!
!(F<=100 G<=1 (air_fuel_ratio = 0))Plasma-Lab analysis estimates the probability is in the interval [0.87251, 0.97549 ] with a confidence of 99%.
