How to Debug a Property Proving Counterexample

Some requirements are difficult to verify completely through simulation-based tests.

Let’s use four requirements for a simplified airplane thrust reverser system to demonstrate. Thrust reversers are used to slow the airplane down on the runway after landing.

We need to make sure that the thrust reversers are not deployed during certain unsafe conditions. Therefore, there are four safety requirements which define when to prohibit thrust reverser deployment.

Notice the use of “shall not” in each requirement? The use of “shall not” in a requirement may indicate that the requirement is difficult to verify completely. How can you be sure you have accounted for unusual conditions?

With simulation-based testing, we would need to create many, many test cases to accomplish this goal, if that is even possible!

This is where property proving can help.

Property proving with Simulink Design Verifier is a static analysis technique that uses formal methods to prove whether a given property will always be valid. This technique can help you formally verify that specific requirements implemented in your design will always be met.

This video will walk you through an example which shows you how to use Simulink Design Verifier and the Model Slicer feature in Simulink Check to formally verify these four thrust reverser safety requirements and debug an automatically generated counterexample.

This Simulink model contains logic defined in a Stateflow state chart to determine when to deploy thrust reversers after the airplane has landed.

Four properties have been defined to verify the safety requirements; one property per requirement. The properties have been defined in a Verification Subsystem, which does not generate code. Properties can be defined using Simulink blocks, Stateflow state charts, or MATLAB code in a MATLAB Function Block.

Let’s look at the Weight-on-Wheels requirement’s property as an example. The Weight-on-Wheels, or “WOW”, sensors are used to determine when the airplane is on the ground.

The property description for the WOW safety requirement is shown as an Annotation in the Verification Subsystem: “If two WOW sensors are false, deploy cannot be true.” In other words, if the airplane is in the air, the thrust reversers should not be deployed.

The WOW property definition uses an Implies block from the Simulink Design Verifier library. The Implies block lets you specify a condition to produce a given response. The Assertion block from the Simulink Model Verification library is also used, which lets Simulink Design Verifier know that a property has been defined.

Let’s run Simulink Design Verifier in Property Proving Mode to verify that all four of the safety requirements are being met by the design.

Simulink Design Verifier was able to invalidate three of the four properties.

A counterexample test vector for each property violation has been automatically generated for debugging.

Counterexamples can be difficult to debug because Simulink Design Verifier will try to find a violation in as few time steps as possible, and the tool does not have any knowledge of what is physically realistic in your overall system.

You need to provide the engineering insight. One way to do this is to use Proof Assumptions to limit a signal’s range, rate of change, or other characteristics. Simulink Design Verifier will use these assumptions when analyzing the model.

We don’t want to add assumptions quite yet as to not rule anything out.

Instead, let’s use Model Slicer from Simulink Check to debug a counterexample. Let’s start with the WOW property.

This is as simple as selecting the Assertion block in the WOW property subsystem, then clicking “Debug” in the Design Verifier results window.

Model Slicer is automatically set up to help us step through the counterexample for the WOW property.

Model Slicer 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 WOW requirement. This is an unusual scenario but represents the type of condition which would be difficult to define in a simulation-based test.

After analyzing the counterexamples for the other properties, and by using my own engineering experience designing similar logic, I can see that the design does not adequately account for sudden changes in signal values after landing.

There are many ways we could address this. I’ve decided to add a new requirement which will add a short delay to enable thrust reverser deployment after the appropriate conditions are met. This short delay will not affect the physical performance of the thrust reversers.

Let’s open the fixed model and run property proving again.

All set!

This example showed how to use Simulink Design Verifier and Model Slicer from Simulink Check to use property proving to analyze safety requirements and debug a counterexample.

You can also link proof objectives to requirements in Requirements Toolbox to manage verification results for property proving in addition to simulation-based tests.

Visit the Simulink Design Verifier product page or the Simulink Check product page to request a trial.