Simulink Design Verifier

Power Window Controller Temporal Properties

This example shows how to model temporal system requirements in a power window controller model for property proving and test case generation using Simulink® Design Verifier™ Temporal Operator blocks.

Temporal Operators

The Simulink® Design Verifier™ librarySimulink® Design Verifier™ library provides three basic temporal operator blocks can be used to model temporal properties. The intent of the temporal operators is to support the specification of temporal requirements, such that the modeled property has a closer co-relation to the actual textual requirement. These blocks are low-level building blocks for constructing more complex temporal properties.

Power Window Controller

The power window controller responds to the driver and passenger commands by giving the commands for moving the window up or down. It also responds to an obstacle and to reaching the end of the window frame in either direction.

Consider the following two requirements for the power window controller:

Requirement 1 (Obstacle Response)

Whenever an obstacle is detected, the controller shall give the down command for 1 second.

Requirement 2 (AutoDown feature)

If the driver presses the down button for less than 1 second, the controller keeps giving the down command until the end has been reached or the driver presses the up button.

%Model of the power window controller

Property Specification

The power window verification system is the top-level model that contains a model reference to the power window controller model specifying the controller behavior and the modeled requirements.

%Model of the top-level verification system

Global Assumptions: The power window controller is an open system. This makes the environment controlled inputs, obstacle and endstop (end of the window frame) to occur freely. To constrain the environment, add two global assumptions for your controller model.

1) The obstacle and the endstop inputs never become true at the same time.

2) The obstacle does not occur multiple times within the following 1-second interval.

For the temporal assumption on obstacle, use a Detector block with output type of "Delayed Fixed Duration" to capture the fixed duration of 1 second (5 time steps with 0.2 sample time).

% Global Assumptions
open_system('sldvdemo_powerwindow_vs/Global Assumptions')

Now consider the first controller requirement for Obstacle Response.

% Obstacle Response
open_system('sldvdemo_powerwindow_vs/Verification Subsystem2')

Here, use the Detector block with output type of "Delayed Fixed Duration" for the property specification. After detection of the obstacle, construct a fixed interval of 4 steps. Note that the input is not observed during the output construction phase for the Detector with "Delayed Fixed Duration" output type. In the case where the obstacle can occur freely in absence of the assumption, you might wish to observe all the intermediate occurrences of the obstacle. This can be achieved through an Extender block with "Finite" extension duration of 4 time steps.

Now consider the AutoDown feature of the power window controller.

For illustration, consider this property specification in smaller parts:

  1. The first temporal duration of interest "driver presses the down button for less than 1 second" is captured by Detector1. At sample rate of 0.2, the 1-second interval is broken down into 5 time steps. On detection of the down signal, construct a 5-step fixed temporal duration at the output of Detector1, which you will subsequently use in combination of other constraints.

  2. For the AutoDown feature, you know that the down signal cannot be pressed for more than 1 second, or 5 time steps. Thus, you want to ensure that the either both driver up and down are "true" or both are "false" in less than 5 steps after down is pressed. By having an AND block connect this driver neutral to the other two Detector outputs, enforce the constraint that the driver down can be pressed for any number of consecutive time steps less than 5.

  3. You also need to ensure that during this period other signal, such as obstacle, EndStop, or DriverUp are not true, since these will take the controller out of responding to the down press. This is captured in Detector2 enforcing that NOT(HaltDown) is true for 5 time steps. This is achieved by using a Detector block with "Delayed Fixed Duration", with the "Time steps for input detection" = 5 and "Time steps for output duration" = 1. output.

  4. Take the AND of these constructed durations.

  5. For the AutoDown feature, you do not want to limit the number of time steps that the controller gives the down command. You know that you want the controller to keep giving the down command as long as the driver does not again press an up or down command, or you hit an obstacle or the physical end of the window frame. This behavior can be captured by the Extender block with "Infinite" extension period and an external reset signal that encodes the condition to end the extension.

  6. The final piece is an Implies block that takes the temporal duration constructed as explained above and checks if the controller down command is true for every time step of this duration.

Once you have the initial property specification, you can use it for property proving using Simulink Design Verifier. You immediately get a counterexample for the above property. The counterexample shows a scenario where the down command is given when the controller was in the emergency down state due to response to a earlier detected obstacle. When you add a constraint to avoid this, you get another counterexample. If the down button is pressed when previously the up command was being given, the AutoDown feature is disabled and the down command is given only as long as the down button is pressed. Looking at these counterexamples and observing the model, you see a pattern that the AutoDown feature is only enabled when the controller is in a neutral state to begin with when the driver presses the down button.

Incorporate this constraint by forcing the controller output to be neutral - neither up nor down command is true - as a precondition for the AutoDown property. This property proves valid.

% Valid AutoDown
open_system('sldvdemo_powerwindow_vs/Verification Subsystem3')

Test Case Generation for Property Validation

Once the properties are specified, in addition to property proving, you can run Simulink Design Verifier to automatically generate test cases that exercise various conditions in the property. This can be achieved by placing custom test objective blocks at appropriate locations in the property.

One such place is to put a test objective block ("true" value) on the signal feeding into the first input of the Implies block (as shown in the above property). On running test generation, when the test objective is satisfied, you can get a test case exercising the various constraints encoded in the property.

Consider the valid AutoDown property specified above. On running test generation, Simulink Design Verifier satisfies this test objective and creates a test harness. The Signal Builder block with relevant signals is shown below.

One can now simulate this test case and see how the temporal durations are created in the property by placing a scope that displays the input and output values of the two Detector blocks, and No_Cmd.

Manually inspecting the test case values enables you to see if the property specified behaves as intended.

This specified test objective prevents the property from being proven valid in the case where the Implies block is trivially true, that is, in the case where the output of the Implies block is true because the first input is always false. When you get a test case satisfying this test objective, you know that there is at least one case where the first input to the Implies block is true.

This exercise can help you validate your property specifications by manually inspecting the test cases automatically generated by Simulink Design Verifier.

Clean Up

To complete the example, close all the opened models.