Simulink Design Verifier
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.
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 English requirement. These blocks are low-level building blocks for constructing more complex temporal properties.
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')
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, construct a 5-step fixed temporal duration at the output of Detector1, which you will subsequently use in combination of 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 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.
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.
Take the AND of these constructed durations.
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.
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')
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.
There is an additional advantage to having such a test objective on the implies block. During property proving, you can ensure that the implies is not getting trivially true making the property valid; in other words, the output of the implies block becoming true because the first input is always false. When you get a test case satisfying this objective, you know that there is at least one case where the first input to implies becomes true.
This exercise can help you validate your property specifications by manually inspecting the test cases automatically generated by Simulink Design Verifier.
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);