Using the CheckMate Verification Tool

Modeling Front End
Entering Parameters
Simulating the Model
Running the Exploration
Running the Verification
Viewing the Results of a Verification
Useful Hints

Return to Main Documentation Page


Modeling Front End

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 window for modeling as CheckMate does not support all 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 an m-file function. 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. If parameters are present in the model, information about them should be entered in the last two fields in the SCSB dialog. The Default Parameter field should contain the value of the parameter that is to be used when the system is simulated. The Parameter Constraints field should contain a pointer to a linearcon object that represents the range of parameters to be analyzed during Exploration and Verification. See the Entering Parameters section for a description of how to specify parameter regions as well as how to specify the Analysis Region and the Initial Continuous Set.

    




Polyhedral Threshold Block (PTHB)
PTHBs can be used to construct switching surfaces and regions in the state space. Within each PTHB, a linear constraint object is used to define a polyhedron. See the entering parameters section for a description of how to use linear constraint 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 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.

return to top
 

Entering Parameters

Initial Continuous Set


The initial continuous set is the set of continuous states that the switched continuous system may start from. Create a linear constraint 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.000000

Similar 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 Parameters

In 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_APARM 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.

return to top

Simulating the Model

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).

return to top

Running the Exploration

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].

return to top

Running the Verification

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

return to top

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.

Also, the CheckMate routine plotpoly may be used to visualize the result of a CheckMate verification for two or three dimensional systems. Typing plotpoly at the command line (after a verfication has run) will display the reachable sets that resulted from the verification routine.

return to top

Useful Hints

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.

return to top