基于CheckMate的混合系统建模和验证

Hybrid system modeling and verification with CheckMate

形式验证是混合系统中的重要研究方向,Checkmate是基于MATLAB/Simulink和Stateflow工具箱开发的一种混合系统建模、仿真和形式验证工具。文章首先介绍了混合系统形式验证的概念和验证过程,从用户的角度介绍了CheckMate的每个自定义模块的设置及其功能原理,通过一个三维线性混合系统的例子,说明了使用CheckMate进行建模、仿真以及验证的方法,最后指出了CheckMate验证工具的局限性。

The formal verification is an important research direction in hybrid systems.CheckMate is a tool for modeling,simulating specific situation and formally verifying hybrid dynamic systems based on the MATLAB/Simulink and Stateflow Toolbox.Firstly the concept of formal verification and the verification procedure of hybrid systems are presented in the paper.The setting of each customized block of CheckMate and the functions are introduced from the user＇s perspective,and the methods of modeling,simulating and verifying hybrid systems are illustrated using a three dimensional linear system example.Finally,the limitations of the verification tool CheckMate are presented.