Open the Model
To begin entering a model from scratch, type
simulink in the Matlab command window.This
will open the Simulink Library Browser containing the special
CheckMate blocks along with some standard Matlab blocks. It
is best to use only the blocks in this category for modeling as
CheckMate does not support any other Simulink blocks.
Layout and connect
blocks
Descriptions of the CheckMate customized blocks are given
below. Use these special blocks along with the standard
Matlab blocks to enter the system model.
Switched Continuous System Block (SCSB)
Use SCSBs to enter sets of switched dynamic equations. Each block takes a single discrete input u and outputs the continuous state vector x according to the dynamics selected by u. The switched dynamics should be entered as a MATLAB function. The function can be implemented either as an M-file or as a mex file. See the section labeled Entering Parameters for a description of how the user-defined switched dynamics m-files are created. The name of this switching function can then be entered as a parameter in the corresponding SCSB.
The option of using parameter constraints is currently disabled.
![]()
Polyhedral Threshold Block (PTHB)
CheckMate uses polyhedra to define sets in continuous state space. PTHBs can be used to construct conditions using polyhedra, which are then used as switching surfaces in the state space. A PTHB block must be associated with a 'linearcon' object in the base workspace. See the entering parameters section for a description of how to use 'linearcon' objects to define PTHB regions. The PTHB takes as input the continuous state vector x and outputs a 1 if x satisfies the constraints, and a 0 otherwise.
![]()
Finite State Machine Block (FSMB)
The discrete dynamics of the hybrid system are entered using FSMBs. These are standard Stateflow machines with a few restrictions from CheckMate. The inputs to the block must obey the following restrictions. Each component of the vectorized event input must be a logical function of PTHB outputs only (i.e. events cannot be generated from any FSMB). Each data input must be a logical function of the outputs of PTHBs or FSMBs.
Initial Continuous Set
The initial continuous set is the set of continuous states that the switched continuous system may start from. Create a linearcon object of class linearcon in the MATLAB command window workspace using the following command:bounce_ICS = {linearcon([],[],[1 0; -1 0; 0 1; 0 -1],[1; 0; 2; 0])};
Note that bounce_ICS as shown above is a cell array of linearcon objects. Each linearcon object represents a convex polyhedral region in the continuous state space (type help linearcon at the Matlab command prompt for more information on creating and using linearcon objects). This particular initial continuous set is a hyperbox where x1 is between 0 and 1 and x2 is between 0 and 2.
The initial continuous set must be a cell array so that non-convex initial sets can be represented as a union of convex polyhedra. The Initial Continuous Set field in the SCSB dialog should point to the linearcon object that represents the initial continuous set.
The user should familiarize themself with standard objects in MATLAB, especially cell arrays and structures.
Analysis Region
The analysis region (AR) is the (full dimensional) bounded convex polyhedron that represents the region of interest. In other words, no analysis is performed for the system beyond the analysis region. Create an analysis region object using
bounce_AR = linearcon([],[],[1 0; -1 0; 0 1; 0 -1],[40; 20; 20; 20]);
To display the content of each object in MATLAB command window, simply type the name of the object (without the semi-colon) and hit enter. For example, to display the content of bounce_AR,
» bounce_AR
bounce_AR =
[ 1.000000 0.000000 ]x <= 40.000000
[ -1.000000 0.000000 ]x <= 20.000000
[ 0.000000 1.000000 ]x <= 20.000000
[ 0.000000 -1.000000 ]x <= 20.000000Similar to the initial continuous set, we have associated the variable bounce_AR with the analysis region in the parameter window for block xy. As we can see from above, bounce_AR is the region {-20 <= x <= 40} and {-20 <= y <= 20}.
Parameter Constraint
The parameter constraint is an object that the SCSB points to. It represents a region of the parameter space for which the system is to be analyzed. The parameter constraint is a linearcon object and should be specified in the same way as the Analysis Region.
Configuring Polyhedral Threshold Blocks
To configure polyhedral threshold blocks (PTHB's), create a linearcon object in the Matlab workspace (as described above for the Analysis Region) , and then point the field named Polyhedron in the PTHB dialog to it. Note that unlike in the Initial Continuous Set and Analysis Region cases, the polyhedron that a PTHB points to need not be closed.
Function Files
Two Matlab m-file functions are used to pass parameters to the verification tool:<param_func>.m returns a structure containing partition parameters for the verification. The global variable GLOBAL_APARAM should contain the name of this file (as a string). For example, type
global GLOBAL_APARAM at the command line. Then type GLOBAL_APARAM = 'file_name' where file_name is the name of the parameter m-file. This allows CheckMate to use the user's parameters during the verification procedure.Note that if any or all of these parameters are not specified by the user, default values are used. If present, this function should return an approx_param structure with some or all following fields:
- approx_param.dir_tol % tolerance in the direction (angle offset)
- approx_param.var_tol % length of the projection in the cell
- approx_param.size_tol % maximum size of each piece
- approx_param.W % matrix to square the axes to avoid numerical problems
- approx_param.T size of each flowpipe segmen
- approx_param.quantization_resolution
- approx_param.max_bissection % maximum number of bissection for simulation reachability
- approx_param.max_time % maximum time of processing
- approx_param.reachability_depth
- approx_param.min_angle % Angle value (degrees) for eliminating faces in the mapping
- approx_param.med_angle % Angle value (degrees) for eliminating faces in the mapping
- approx_param.extra_angle % Angle value (degrees) for eliminating faces in the mapping
- approx_param.max_angle % Angle value (degrees) for eliminating faces in the mapping
- approx_param.unbound_angle % Angle value (degrees) for eliminating faces in the mapping
- approx_param.edge_factor % Factor to decide if edge will be dropped in the mapping
- approx_param.edge_med_length % Factor to decide if an edge is too small (compared to the mean) to be eliminate
- approx_param.grow_size % For growing operations (when there is a loss of dimension), objects are grown by this much ON EACH SIDE.
- approx_param.max_func_calls % Maximum number of function evaluations allowed for fmincon operations. Note that this value will be multiplied by the system dimension.
- approx_param.func_tol % Termination tolerance on the function value for fmincon operations. Note that this number will be multiplied by the time step size for shrink wrapping operations during flowpipe computations.
- approx_param.max_iter % Number of iterations for fmincon calls. Note that this number will be multiplied by the dimension of the problem.
- approx_param.poly_epsilon % *'epsilon'--tolerance used in feasibility check
- approx_param.poly_bigM % *'bigM'--big M used to check constraint's redundancy
- approx_param.poly_point_tol % *'point_tol' tolerance used in point comparison (distance based)
- approx_param.poly_vector_tol % *'vector_tol' tolerance used in vector comparison (direction based)
- approx_param.poly_hyperplane_tol % *'hyperplane_tol'--tolerance used in hyperplane comparison and in identifying which hyperplanes in a PTHB correspond to a given vertex (in partition_ss)
- approx_param.step_rel_tol % Relative tolerance for step responses.
- approx_param.step_abs_tol % Absolute tolerance for step responses.
<switch_func>.m is used to enter the switched dynamics for each of the SCSBs. This file name is entered as a property of each SCSB. It should return the type of overall dynamics (i.e. clock, linear, or nonlinear) and the state derivatives. If the overall dynamics are clock, the function should return the derivatives as a constant vector of rates for the state variables. If the dynamics are linear, the function should return a structure sys with the fields sys.A the "A-matrix" for the system, and for affine systems, sys.b containing the constant "b-matrix" of the system. For nonlinear systems, the function simply returns the right hand side of the differential state equations.Also, the behavior of resets and parameters is specified in the switched dynamics file. If resets are present in the system (i.e. if they are specified in the SCSB dialog inside the model), the reset value of the state should be returned along with the derivatives of the state vector. Parameters, if they are present in the model, should be passed to the switched dynamics function as a paramter. Note that the parameter should only affect the behavior of the vector field and not the reset behavior. See below for an example of how resets and parameters are specified.
The following is an example of a switched dynamics file that specifies a two dimensional system with clock dynamics and no resets or parameters.
The following is an example of a switched dynamics file that specifies a two dimensional linear system with no resets or parameters.
The following is an example of a switched dynamics file that specifies a three dimensional nonlinear system with resets and parameters. Note that the resets defined are associated with the destination of a transition. For example, if a transition from state u=1 to u=2 is taken, the reset associated with state u=2 is applied to the state vector.
Additional ParametersIn addition to the m-file functions above, three global variables must be set prior to running a verification. The name of the Simulink model representing the TEDHS should be entered in GLOBAL_SYSTEM. GLOBAL_PARAM should contain the name of the parameter m-file function described above, and the ACTL specification to be verified must be entered in GLOBAL_SPEC. These additional parameters can be entered manually at the command prompt, or can be set using an m-file script or function.
CheckMate models can be simulated like any other Simulink model. When the play button is hit in the Simulink window, the system is simulated using the initial conditions specified in the SCSB Initial Conditions field inside the SCSB dialog. The type of solver and the solver parameters specified in the Simulation Parameters dialog in the Simulink window menu are used to simulate the system. Any general Simulink sinks may be used to capture or view the behavior of the system during a simulation (i.e. the user is not restricted to the blocks in the CheckMate library).
The explore tool is invoked from the Matlab command window by typing explore at the prompt. In this form, the tool simulates the point entered as the initial condition in the SCSB block parameters for the time specified in the Simulink simulation parameters. After the simulation is complete, the explore routine checks the simulated trajectory against the ACTL specification and informs the user whether or not the trajectory violates the specification. As mentioned above, if an ICS is defined, explore can be invoked with a -vertices option which will cause the procedure above to be performed on each of the ICS vertices.A sample run of the explore tool is shown here.
This tells the user the initial state of the system, the value of the output of the PTHB's at the initial instant, and that the specification was satisfied.
As mentioned above, instead of one simulation instance, explore can investigate simulation runs for several initial condition points. At the command line, type the following:
explore -vertices
This explore option will take the vertices of the boing_ICS linearcon and use them as initial conditions for simulation. Explore then tests if the specification holds for each simulation point.
Also, the user can specify a set of initial condition points. At the command line type:
a=[0 0 ; 1+sqrt(2) 1+2 ; 0 0];
explore -points a
This will cause the analysis to explore the trajectories starting from the points x=[0 1+sqrt(2) 0] and x=[0 2 0].
Once the model and parameters are entered, the verification is performed by typing verify at the command prompt. With no options, verify will run through one iteration of the verification process, determine whether or not the system satisfies the specification, and prompt the user accordingly. If the system verifies, the user is informed and the program terminates. If the system does not satisfy, the user is informed and prompted to "press any key to start refining the automaton....". At this point the user can press a key and continue with another refinement iteration, or break the program, save the workspace data and continue the process at a later time. Several option flags are available for the verify command. These options are summarized in the table below.Option | Description |
step <step> | Execute only the single verification step step |
resume | Continue the verification process using the current workspace data |
nopause | Refine the quotient system without prompting the user for input |
save <savefile> | Save the workspace data after each iteration using savefileN.mat to save the data after the Nth iteration |
close | Close the Simulink model after the PIHA has been constructed |
discard | Throw away all unreachable states in each iteration |
The basic steps of the verification routine are shown
below.
Starting the routine
The refinement decision
Positive verification result and program termination
Viewing the Results of a Verification
After a verification has been performed, CheckMate gives the user more information beyond dtermining if a specification was satisfied. CheckMate also produces data structures that give the user information about verifaction that was performed. All information about the finite state representation of the system (see the introduction to the theory behind the CheckMate verification procedure) is stored in the Matlab workspace. Three global variables may be of specific interest to the user: GLOBAL_PIHA, GLOBAL_AUTOMATON, and GLOBAL_TRANSITION. The following gives a brief description of each variable:The CheckMate routine document takes as an argument any one of these three variables and produces a text file. This text file lists all of the information conatined in the variable.
Creating a CheckMate model and performing a successful verification can be a tricky task. This section presents some hints to help the user with the process.