CHECKMATE VERIFICATION TOOL |
CheckMate implements the verification technique that conservatively
approximates the original hybrid system model by purely discrete and finite
models called quotient transition systems or approximating automata.
The verification is initiated by typing the command verify
in the MATLAB command window. The verification process in CheckMate follows
the flow diagram shown on the left.
The class of hybrid systems that can be modeled in CheckMate front end is called the threshold-event-driven hybrid systems (TEDHS). The verification process starts by the conversion of the Simulink model into an equivalent model called a polyhedral-invariant hybrid automaton (PIHA). The resulting PIHA is discretized to form a quotient transition system (QTS) by an initial partition that is constructed according to the parameters specified by the user. Transitions between states in the QTS are computed using the continuous reachability analysis technique called the flow pipe approximations. The QTS is then verified against the ACTL specification using standard model checking technique for finite-state transition systems. Since the verification may fail due to the coarseness of the hybrid system approximation by the QTS, the partition for the QTS can be refined to give a tighter approximation. After the partition refinement, the flow pipe approximation is used to redefined the transitions in the QTS. The process repeats until the QTS satisfies the specification or the user chooses to terminate the verification. The subsequent sections describe each step of the verification in more detail. |
![]() Verification Overview |
Threshold-event-driven Hybrid System
The SCS is the continuous dynamics systems that takes in the discrete-valued input u and produces its continuous state vector x as the ouput. The continuous dynamics for x evolves according to the differential equation or differential inclusions selected by the discrete input u as shown in the above figure. The output of the SCS is fed into the TEG, which produces an event when a component of the vector function g of x crosses its corresponding threshold from the specified direction (rising, falling, or both). The event signals from the TEG drives the discrete transition in the FSM whose output, in turn, drives the continuous dynamics of the SCS.
Transitions between locations are called edges. Each edge is labeled with the guard and the reset conditions on the continuous state. The location transition is enabled, i.e. allowed to be taken, when the guard condition is satisfied. Upon the location transition, the values of the continuous state before and after the transition must satisfy the reset condition.
|
|
'clock' | Continuous dynamics of the form ![]() |
'linear' | Continuous dynamics of the form ![]() |
'nonlinear' | General continuous dynamics dynamics of the form ![]() |
See Using CheckMate Verification Tool for detail on how to specify the parameters for an SCSB.
A sample CheckMate diagram is shown below.
The procedure for converting the TEDHS in the front end into a PIHA is implemented in the m-file piha.m located in the directory ~/frontend/@piha. The m-file is implemented as the constructor for the object class 'piha' but the return variable is never treated as an object in the subsequent code in verify.m. Instead the PIHA is converted into a regular structure variable so that its fields can be accessed directly. Implementing the object class 'piha', however, could prove useful when composition of multiple PIHA is considered in the future. |
Disclaimer: The function check_model_syntax() is not completed yet. The user needs to make sure that the Simulink model conforms to the rules outlined in the previous section. |
Each block in the Simulink model is an object identified by a unique number called a handle. Simulink has its own system of assigning the object handles which is separated from the handle systems of MATLAB standard GUI and Stateflow. Using the function get_param() and set_param(), the user can manipulate various properties of a Simulink object. |
Threshold hyperplanes are introduced into the partition one by one in each stage of the partitioning. In each stage, the partition information is maintained in a tree structure with the whole analysis region at the root as shown in the figure below.
The tree is expanded when a hyperplane is introduced by spliting the leaf nodes as needed. In our examples, the hyperplanes are introduced in the ascending numerical order. Once all hyperplanes are introduced, the leaf nodes consitutes the cells in the analysis region partition as shown in the above figure. The same figure without the animation is reproduced below so that the reader can examine the final tree structure more carefully.
After the partitioning is completed, the leaf nodes (the cells) are intersected with the initial continuous sets (augmented for the full continuous statespace) from SCSBs. The cells that overlap with the initial continuous sets are called the initial cells. These are the cells from which the continuous trajectory of the hybrid system may originate.
Note that we need not consider any subtree for which the hyperplane does not pass through the polytope of the root node. Thus, using the tree structure can improve efficiency of the partitioning process significantly in the case where the number of threshold hyperplanes is large. The same kind of efficiency can be achieved when finding the initial cells by traversing the partition tree and ignore the subtree for which the root node does not overlap with the initial continuous set.
The tree should be as balanced as possible for the analysis region partitioning or the initial cell intersection algorithm to be most efficient. Thus, before the analysis region partitioning begins, the hyperplanes are sorted so that the ones that are most centered with respect to the analysis region are introduced first. To do this, we introduce the quantity called the normalized deviation (not a standard term in literature) which is a non-negtive number that measures the centered-ness of each hyperplane with respect to the analysis region. The smaller the normalized deviation, the more centered that hyperplane is with respect to the analysis region.
CheckMate maintains the following information about the each cell in
the analysis region partition.
boundary | the indices to hyperplanes (in the list compiled earlier) constituting the cell boundary |
hpflags | an array of boolean flags, one for each hyperplane ciTx = di in the list, indicating whether the inequality ciTx <= di is true when the continuous state x of the hybrid system lies in the cell. |
pthflags | an array of boolean flags, one for each PTHB in the list compiled earlier, indicating the output value of the corresponding PTHB when the continuous state of the hybrid system lies in the cell. |
neighbors | indices to other neighboring cells. Note that for any two neighboring cells, their hpflags must be different by exactly one hyperplane. |
The reader is referred to the m-file partition_ss.m in the directory ~/frontend for more information on the analysis region partitioning. |
|
|
|
|
|
|
|
|
|
CheckMate will produce the following results for the expressions of all event and data signals. For the block fsm1,
v1 = 'pth1'For the block fsm2,
v2 = 'pth2 | pth3'
d1 = 'pth1'
d2 = '2 ~= fsm2'
v3 = 'pth3'Note that once the values are assigned to the variables with the same names as the PTHBs and FSMBs, the value of the event and data signals can be evaluated using the command eval in MATLAB (see MATLAB on-line help for more detail). This is indeed what CheckMate does to evaluate the event and data signals later on the PIHA conversion process. To evaluate whether changes in the event signals actually produces any event, CheckMate also maintains the information on the type of each event which could be rising edge, falling edge, and either edge.
d3 = 'fsm1'
d4 = 'pth1'
The initial FSM states are the states which are the destination of the default transition in the Stateflow diagram for each FSMB. The current implementation of CheckMate allows only one default transition per Stateflow block, that is, the initial state for each FSMB is deterministic.
The location transitions in the PIHA are determined as follows. For each location (p1,q1), the cell p1 serves as the location invariant (see Section 2.2). The number of outgoing transitions from the location are the same as the number of hyperplanes on the boundary (faces) of p1. To determine the destination of the transition for each hyperplane hi, we first compute the event that can occur in the FSMBs when the continuous trajectory leaves the cell p1 through the hyperplane hi. Recall that each cell in the analysis region partition uniquely determines the output of all PTHBs when the continuous trajectory resides in that cell. Thus, all event signals can be computed by comparing the values of PTHB outputs in the cells before and after crossing the hyperplane hi. There are three possible cases as illustrated in the figure shown below.
The out-of-bound and terminal locations are not explicitly represented in the location cell array in the m-file piha.m. Rather, they are encoded on the transition for the hyperplane that leads to these special locations. |
--------------------------------
Data structure for a PIHA object
--------------------------------
A PIHA object, HA, obtained after the conversion from a C/E system
consists of
the following fields:
HA.Hyperplanes
: List of threshold hyperplanes in the C/E system
HA.NAR
: Number of hyperplanes on analysis boundary
HA.InitialContinuousSet : Set of initial continuous
states
HA.InitialDiscreteSet : Set of initial
discrete states
HA.Cells
: List of cells in the continuous state space
partition
HA.InitialCells
: List of cells which overlaps with the initial
continuous set
HA.Locations
: List of hybrid automaton locations
HA.InitialLocations : Indices
to initial locations
HA.SCSBlocks
: List of switch continuous system blocks in the
C/E system
HA.PTHBlocks
: List of polyhedral threshold blocks in the C/E
system
HA.FSMBlocks
: List of finite state machine blocks in the C/E
system
The data structure for each field is described below.
(1) Hyperplanes
---------------
Threshold hyperplanes from all PTHBs and the analysis region AR
are collected
in this field. The field is a cell array of hyperplane structures,
each with
the following format
Hyperplanes{i}.pthb : -1 if it belongs to analysis
region AR, otherwise
it is the index to the parent PTHB in PTHBlocks
Hyperplanes{i}.index : The hyperplane index within
the parent PTHB
Hyperplanes{i}.c : Vector
and constant pair representing the hyperplane
Hyperplanes{i}.d : c*x = d
(2) NAR
-------
This field is an integer indicating the number of hyperplanes on
the analysis
region boundary. The first NAR hyperplanes in the Hyperplanes list
are the
hyperplanes from the analysis region.
(3) InitialContinuousSet
------------------------
A linearcon object with parameters CE,dE,CI, and dI representing
the initial
continuous set
CE*x = dE
CI*x <= dI
(4) InitialDiscreteSet
----------------------
A cell array of initial discrete states. Each initial discrete state
(cell
element) is a vector of state indices for FSMBlocks in the same
order as in
FSMBlocks list.
(5) Cells
---------
A cell array of "cells" in the partition of the continuous state
space. Each
cell is a structure of the following format
Cells{i}.boundary : A vector of indices to hyperplanes
in Hyperplanes list
that comprises the boundary of the ith cell.
Cells{i}.hpflags : A vector of the same
length as the Hyperplanes list.
hpflags(j) is a boolean flag indicating the side of
the jth hyperplane in Hyperplanes list in which the
cell lies. Specifically,
hpflags(j) = 1 --> c_j*x <= d_j
hpflags(j) = 0 --> c_j*x >= d_j
for any x in the ith cell.
Cells{i}.pthflags : A vector of the same length
as the PTHBlocks list.
pthflags(j) is a boolean flag indicating the output
value of the jth PTHB in PTHBlocks list for any x
in the ith cell.
Cells{i}.neighbors : A vector of indices to the neighboring
cells.
(6) InitialCells
----------------
A vector of indices to the continuous state space cells in the field
Cells
that overlaps with the initial continuous set.
(7) Locations
-------------
A cell array of locations, each with the following format
LOCATIONS{i}.p
: Index to a continuous cell in the field Cells
LOCATIONS{i}.q
: A vector of discrete state numbers (same format
as each element of InitialDiscreteSet)
LOCATIONS{i}.transitions : A cell array of location
indices. transitions{j}
indicates the destination location(s) for the
location transition taken when the continuous
trajectory exits through the jth hyperplane of
on the boundary of the cell p.
transitions{j} is a structure array with each
elements containing 2 field 'type' and 'value'
If crossing the jth hyperplanes means
leaving the analysis region, then
transition{j} contains a single element with
the following field values
type: 'out_of_bound'
destination: []
If crossing the jth hyperplane may lead to
a "terminal" FSM state q' (a state for
which there is no transition out of any
of the component states), then
transition{j} contains an element with the
following field values
type: 'terminal'
destination: q'
where q' is a row FSM state vector
For each regular location transition,
transition{j} contains an element with the
following field values
type: 'regular'
destination: idx
where idx is the destination location index
(a scalar)
(8) InitialLocations
--------------------
A vector of indices to the locations in the field Locations that
are the
initial locations.
(9) SCSBlocks
-------------
A cell array of switched continuous system blocks, each with the
following
format
SCSBlocks{i}.name
: Name of the ith SCSB
SCSBlocks{i}.nx
: Number of continuous variables
SCSBlocks{i}.nu
: Number of discrete inputs
SCSBlocks{i}.swfunc
: Name of the switching function m-file
SCSBlocks{i}.fsmbindices : A vector of indices to
FSMBs in the FSMBlocks
fields in the order that feeds into the input
of the block SCSBlock{i}.
(10) PTHBlocks
--------------
A cell array of polyhedral threshold blocks, each with the following format
PTHBlocks{i}.name : Name of the ith PTHB.
Name of PTHBs will be used as atomic propositions for CTL verifications.
(11) FSMBlocks
--------------
A cell array of finite state machine blocks, each with the following
format
FSMBlocks{i}.name : Name of the ith FSMB.
FSMBlocks{i}.states : A cell array listing the discrete
states in the ith
FSMB by name.
A QTS is a conservative approximation in the sense that for every trajectory in the original hybrid system, there is a trajectory in the QTS corresponding to the set of states that the trajectory in the hybrid system goes through. Thus, if we can verify that all trajectories in the QTS satisfy some property, we can conclude that all trajectories in the hybrid system also satisfy the same property.
CheckMate only pays attention to the behavior of the hybrid system at the switching instants. Thus, approximates the QTS for the hybrid system from the partition of the switching surfaces, which are the boundaries of the location invariants in the PIHA, and the set of continuous initial states. The reachability analysis used to define the transitions in the QTS is performed using the approximation method called the flow pipe approximations, discussed in the next section. The heuristics for choosing the initial partition is also discussed in a later section. The actual data structure for the quotient transition system, also called approximating automaton, is described in the m-file iauto_part.m in the directory ~/approximation.
![]() 1.Choose the set of enclosing direction vectors. |
![]() 2. Solve the optimization problem ![]() |
For the reachble set between time [tk,tk+1], the optimization problem in step 2 can be posed as
For linear systems, we do not have to solve the optimization problems for each time segment as we have the following result that the flow pipe segment can be obtained by transforming another segment with the same time step Dt.
The user specifies these tolerances in the parameter files that CheckMate references during the verification process (see Using CheckMate Verification Tool). The above heuristics for partitioning the invariant faces is implemented for each type of the continuous dynamics in the m-files clock_partition.m, linear_partition.m, and nonlinear_partition.m in the directory ~/approximation/partition.
The heuristics for splitting a polytope in CheckMate follows the following general steps:
Disclaimer: The initial continuous set is partitioned using the same heuristics if it is of dimension n-1, i.e. same dimension as the invariant faces. Similar heuristics may be generalized to partition polytopes of other dimensions. However, this remains a future work. Currently, no partitioning is done for polytopes of dimensions other than n-1 in the m-file iauto_part.m in the directory ~/approximation. |
After using the above heuristics, the invariant face partitions are partitioned further with the polytopes obtained from the reachability analysis from each initial continuous set. Roughly, this additional partitioning schemes proceeds as follows.
![]() |
||
|
|
|
||||
|
|
|
where ap denotes an atomic proposition and ~, &, and | denote
logical not, and, and, or, respectively. CheckMate
only considers a subclass of CTL called ACTL which is given by the grammar
|
Note that only the universal path quantifier A is allowed in an ACTL formula. This is due to the fact that CheckMate uses the conservative approximations (the quotient transition systems) to verify properties of the hybrid system. One can conclude that the original hybrid system satisfies the specification from the conservative approximation only when a universal specification (a specification which requires that a certain property holds for all behaviors of the system) is used. We give a few examples of the ACTL expressions.
|
The above problem can be solved by performing the reachability analysis on the finite-state transition graph using well-known graph search algorithms. The reader is referred to the m-files in the directory ~/ACTL for the implementation of the model checking algorithms in CheckMate.
|
|
|
|
PTHB is the name of a PTHB in the Simulink diagram. | True iff the output of the block PTHB is 1 for the given continuous state x of the Simulink model. |
|
FSMB is the name of an FSMB in the Simulink diagram and state is the name of a state in the Stateflow diagram for the block FSMB. | True iff state is the active state of the block FSMB for the given discrete state u of the Simulink model. |
The following refinement scheme is used in CheckMate for each state that is to be refined: