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