How to Model and Formally Verify Safety Requirements
Some requirements are nearly impossible to completely verify using simulation-based testing, such as safety requirements that define when a given condition should NOT occur.
Learn how to use a Requirements Table from Requirements Toolbox™ to model a set of formal safety requirements, Simulink Design Verifier™ to prove that the requirements will always be met, and Model Slicer from Simulink Check™ to debug a counterexample.
Published: 7 Apr 2023
Some requirements are nearly impossible to verify completely using simulation-based testing, such as safety requirements which define when a given condition should not occur. In this video, I will show you how to use a requirements table from Requirements Toolbox to model a set of formal safety requirements and use Simulink Design Verifier to prove that the requirements will always be met. I will also show you how to use Model Slicer to debug a counterexample.
The example I will use in this video is available using the link below. This example includes a simplified aircraft thrust reverser system. Pilots often deploy thrust reversers to slow the aircraft upon landing. Deploying thrust reversers in the air is a hazard. With this in mind, we can write a set of safety requirements which define when not to deploy thrust reversers.
Let's use a requirements table to formally define these requirements. Each requirement can be written in a row of a requirements table. The postcondition is the deploy command for the thrust reversers. For each of the four requirements, we want deploy to be false.
We can use common MATLAB functions to define the precondition for each requirement. For example, we can define the airspeed threshold requirement using the mean of the airspeed sensors. We can also define the weight on wheels requirement using the sum of the four Boolean weight on wheels inputs.
We can now use Simulink Design Verifier in property-proving mode to formally verify these requirements. Simulink Design Verifier will automatically consider each requirement in the requirements table as a proof objective and will analyze the design model to look for violations for each requirement. It turns out three of the requirements can be invalidated.
Simulink Design Verifier has generated a counterexample for each invalidated requirement. Let's debug the weight on wheels requirements counterexample by clicking on the highlighted deploy cell and then clicking Debug in the Simulink Design Verifier Results window.
Model Slicer is automatically set up to help us step through the counterexample for the weight on wheels requirement. Model Slicer, a feature in Simulink Check, allows you to step through a simulation to see which parts of a model are active and what the signal values are during any step within a simulation. If we step back and then forward through the short counterexample simulation, we can see that there is a specific transient condition wherein a sudden change in the airspeed and wheel speed sensor values can violate the weight on wheels requirement.
This is an unusual scenario, but represents the type of condition, which would be difficult to define in a simulation-based test. We can fix this issue by adding a short delay to enable thrust reverser deployment after the appropriate conditions are met. Let's open the fixed model and run Simulink Design Verifier in property-proving mode again-- all set.
In this video, you learned how to use a requirements table from Requirements Toolbox to model a set of formal safety requirements, how to use Simulink Design Verifier to prove that the requirements will always be met, and how to use Model Slicer from Simulink Check to debug a counterexample. Click on the link below to try the example.