Validate Requirements by Analyzing Model Properties

Overview

In this example, you analyze model properties that are based on four requirements of an engine thrust reverser system. Falsified results from the property analysis suggest that the system design requirements are incomplete -- the system allows behavior that violates several of the following requirements:

To better understand the model behavior, you analyze dependencies for a time series input that causes undesirable model behavior because the system lacks required control logic. Then, you analyze a revised control system model which passes the property analysis.

Analyze the Safety Properties

1. Click the Open Model button to open the original model and create a working directory of the example files.

The Safety Properties subsystem is a Verification Subsystem block from the Simulink® Design Verifier™ library. The verification logic in Safety Properties models the safety requirements. For example, the airspeed requirement is verified by:

For more information about Verification Subsystem blocks, see Verification Subsystem.

2. View the requirements. In the model, click the Show Perspectives views icon at the lower right and select Requirements. The Requirements Perspective opens. Expand thrust_reverser_safety_requirements.

The safety requirements link to the Assertion blocks in the Safety Properties subsystem. The Assertion blocks are considered proof objectives. The verification status for each requirement reflects the property analysis results of its corresponding Assertion block.

3. Display the verification status for the requirements. Right-click one of the requirements in the Requirements Browser and select Verification Status. The Verified column indicates that the requirements are unexecuted.

4. Analyze the model properties. In the Apps tab, click Design Verifier. In the Design Verifier tab, click Prove Properties.

When the property analysis completes, click the Refresh button to update the status in the Verified column. The results show that three out of four objectives are falsified -- analysis found a signal condition that falsifies the properties, and therefore violates the requirements.

Analyze Model Behavior with Counterexamples

From the Design Verifier Results Summary window, click HTML to open the detailed analysis report. In Chapter 4, each falsified property lists a counterexample. For example, in the counterexample that falsifies the airspeed requirement:

The counterexample time series indicates a condition that might be difficult to encounter in simulation, but nonetheless causes model behavior that violates a requirement. Investigate the behavior by analyzing signal dependencies in the counterexample:

1. In the Design Verifier tab, click the Highlight in Model button.

2. Select the airspeed valid assertion block in the Test Unit > Safety Properties > airspeed property subsystem.

3. In the Design Verifier tab, click the Debug Using Slicer button. The model highlights dependencies of the airspeed valid assertion, and displays signal values at T = 0.2.

4. Move up one level in the model, to the Safety Properties subsystem. Step back through the counterexample simulation time. In the Simulation tab, click Step Back.

5. At T = 0.1, the average airspeed is below the threshold, and the thrust reverser is deployed. Stepping forward, at T = 0.2, the average airspeed is above the threshold, and the thrust reverser is still deployed. This violates a requirement.

The falsified property and the dependency analysis suggest that the control system algorithm is incompletely designed, and the requirements are incomplete.

Analyze the Redesigned System

Redesigning a control system requires rethinking requirements. In this case, the lack of an intermediate standby state allows undesirable system behavior when inputs change suddenly. Adding an intermediate deployment mode which delays thrust reverser response resolves the issue.

Open the reqs_validation_property_proving_redesigned_model model. Open the thrustReversers chart.

The additional design requirement states that the thrust reverser shall deploy after a pause. The redesigned model includes:

Create links from the verification blocks in the redesigned model to the requirements:

1. In the model, from the Apps tab, click Requirements Manager.

2. In the Requirements tab, click Requirements Editor.

3. Open thrust_reverser_safety_requirements in the Requirements Editor.

4. For requirement 1.1, Airspeed Condition, link to the airspeed valid block in the Safety Properties > airspeed property subsystem. Drag R1.1 from the Requirements Browser to the airspeed valid block in the model.

5. The new link appears in the Requirements Editor, in the right pane, under Links.

6. Delete the link to the assert block in the original model. If the original model is closed, this link appears unresolved. Next to the link, click the Delete Link icon.

7. Repeat for the other three requirements and verification blocks in the redesigned model.

Run the property analysis on the revised model. View the results in the Requirements Browser.

The results show that the properties are valid.