Power Window Controller Temporal Properties

Open Script

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™ library provides three basic temporal operator blocks which 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 correlation 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
open_system('sldvdemo_powerwindowController')
open_system('sldvdemo_powerwindowController/control')

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
open_system('sldvdemo_powerwindow_vs')

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:

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, Detector1 constructs a 5-step fixed temporal duration at its output, which you will subsequently use in combination with other constraints.
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 both driver up and down are "true" or both are "false" in less than 5 steps after down is pressed. By taking the AND of this driver neutral and the Detector output, enforce the constraint that driver down can be pressed for any number of consecutive time steps less than 5.
You also need to ensure that, during this period, other signals such as obstacle, EndStop and DriverUp are not true, since these will take the controller out of responding to the down press. This is captured using Detector2 by enforcing that NOT(HaltDown) is true for 5 time steps. Detector2 has "Delayed Fixed Duration" output type. It also has "Time steps for input detection" = 5 and "Time steps for output duration" = 1.
Take the AND of these constructed durations.
For the AutoDown feature, you do not want to limit the number of time steps for which 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 press an up or down command again, or an obstacle or the physical end of the window frame is not hit. 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.
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 this initial property specification, you can use it for property proving with Simulink Design Verifier. You will get a counterexample for this property. The counterexample shows a scenario where the down command is given when the controller was in the emergency down state due to the response to an earlier detected obstacle. After you add a constraint to avoid this, you will 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 can see a pattern that the AutoDown feature is enabled only 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 is proven 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 location to place a Test Objective block (with "true" value) is on the signal feeding into the first input of the Implies block (as shown in the above property). On running test generation, this Test Objective is satisfied and you will get a test case exercising the various constraints encoded in the property. Simulink Design Verifier can also create a test harness to simulate this test case. 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 specified property behaves as intended.

This Test Objective block helps in identifying a scenario where the property is valid while the Implies block is not trivially true. An Implies block is trivially true when its output is true because of its first input being 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.

close_system('sldvdemo_TOBlocks',0);
close_system('sldvdemo_powerwindowController',0);
close_system('sldvdemo_powerwindow_vs',0);