Overview

在本例中,您分析模型的公关operties 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 theOpen Modelbutton 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, seeVerification Subsystem.

2. View the requirements. In the model, click theShow Perspectives viewsicon at the lower right and selectRequirements. TheRequirementspane opens. Expandthrust_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 browser and selectVerification Status. TheVerifiedunexecu列表明需求ted.

4. Analyze the model properties. In theAppstab, clickDesign Verifier. In theDesign Verifiertab, clickProve Properties.

When the property analysis completes, click theRefreshbutton to update the status in theVerifiedcolumn. 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, clickHTMLto 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 theDesign Verifiertab, click theHighlight in Modelbutton.

2. Select the airspeed valid assertion block in theTest Unit > Safety Properties > airspeed propertysubsystem.

3. In theDesign Verifiertab, click theDebug Using Slicerbutton. 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 theSafety Propertiessubsystem. Step back through the counterexample simulation time. In theSimulationtab, clickStep 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 thereqs_validation_property_proving_redesigned_modelmodel. Open thethrustReverserschart.

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 theAppstab, clickRequirements Manager.

2. In theRequirementstab, clickRequirements Editor.

3. Openthrust_reverser_safety_requirementsin theRequirements 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 theDetailspane, underLinks.

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 theDelete Linkicon.

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 pane.

The results show that the properties are valid.