NOTE:

CheckMate is a hybrid systems research tool developed by:

Alongkrit Chutinan
Ansgar Fehnker
Zhi Han
Jim Kapinski
Rajesh Kumar
Bruce H. Krogh
Braz Izaias Silva Jr.
Olaf Stursberg

CheckMate has been tested on MATLAB R2006b and later releases. Clicking on the "Download" link to the left will take you there.

For the latest developments in hybrid systems verification tools, we suggest PHAVer, http://www.cs.ru.nl/~goranf/, developed by Goran Frehse.

CheckMate is a MATLAB®-based tool for modeling, simulating, and verifying properties of hybrid dynamic systems. These are dynamic systems with both discrete and continuous state variables. Hybrid systems often arise in computer-controlled systems where the discrete dynamics corresponds to logic for switching control modes and the continuous dynamics corresponds to the physical system being controlled.

CheckMate models are constructed using custom and standard Simulink® and Stateflow® blocks. The continuous state equations, parameters and specifications (the properties to be verified) are entered using the Simulink GUI and user-defined m-files. Specifications express properties of trajectories of the CheckMate model. The CheckMate verification function determines if the given specifications are true for all trajectories starting from a polyhedral set of initial continuous states and continuous ranges of parameter values.

What can CheckMate do?

Simulation. CheckMate models can be simulated as standard Simulink models. This is useful for debugging Checkmate models.

Exploration. The explore command evaluates the specifications for the trajectories starting from the vertices of the set of initial continuous states for the parameter values at the vertices of the parameter set. This provides some preliminary insight into whether the specifications will be true for all of the initial continuous states and parameters.

Verification. The verify command evaluates the specifications for all possible trajectories, starting from states in the initial state set and for all values of parameters in the parameter set. The computation time for verification can be large, so it is important to make sure the model has been simplified as much as possible before applying the verify command to a CheckMate model.

What are the system requirements?

As a MATLAB-based tool, the current version of CheckMate requires the following MATLAB components:

  • MATLAB 6.5
  • Simulink 4.1 or higher
  • Stateflow 4.1 or higher
  • Optimization Toolbox
  • Control System Toolbox

CheckMate is developed and tested within the Windows 2000/XP environment. Some modifications may be needed to make it work correctly under Unix or Linux.

Where do I start?

New CheckMate users should look at some of the demonstration examples available in the CheckMate distribution. In order of complexity, the demonstrations are:

  • Bouncing Ball
  • Concentration Plant
  • Electronic Throttle Control (5th order model)
  • Electronic throttle regulator (constant reference signal)
  • Variable Cam Timing System

Each example comes with a working CheckMate model and documentation explaining the example. To run an example, go to its directory in the demos directory.

What do I need to know?

Despite our effort to make things intuitive, CheckMate users need to be familiar with MATLAB, Simulink, Stateflow and some basic theory related to hybrid systems, dynamic systems and polyhedral computations. To get the most out of CheckMate, the user should be familiar with the following topics:

  • Linear algebra
  • Automata theory
  • Model checking and computation tree logic
  • Hybrid automata

Knowledge of the following topics is essential for advanced users who have to deal with the underlying code and algorithms in CheckMate:

  • MATLAB object oriented programming
  • Standard MATLAB objects, especially cell arrays and structures
  • Computational geometry, especially the operation convex hull
  • Optimization, especially linear programming

How do I get more information?

After installing Checkmate, type "cmhelp" at the MATLAB command prompt to bring up the documentation page.

Additional documentation is contained in the distribution. The User's Guide describes how to model and analyze systems in CheckMate. CheckMate Verification: Theory and Implementation provides an introduction to the theory behind CheckMate's verification procedure.

How do I get the documenation of the MATLAB code?

You may try to use the M2HTML tool found here.