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

Hybrid system modeling and verification with CheckMate

作　　者：李健[1] 方敏[1] 李加良[1] 

机构地区：[1]合肥工业大学电气与自动化工程学院,安徽合肥230009

出　　处：《合肥工业大学学报（自然科学版）》2010年第1期50-54,共5页Journal of Hefei University of Technology：Natural Science

摘　　要：形式验证是混合系统中的重要研究方向,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.

关 键 词：形式化验证 混合系统 商迁移系统 流管道 

分 类 号：TP301[自动化与计算机技术—计算机系统结构] TP15[自动化与计算机技术—计算机科学与技术]