CAJ | 학술논문

形式验证是混合系统中的重要研究方向,Checkmate是基于MATLAB/Simulink和Stateflow工具箱开发的一种混合系统建模、仿真和形式验证工具.文章首先介绍了混合系统形式验证的概念和验证过程,从用户的角度介绍了 CheckMate的每个自定义模块的设置及其功能原理,通过一个三维线性混合系统的例子,说明了使用CheckMate进行建模、仿真以及验证的方法,最后指出了CheckMate验证工具的局限性.
형식험증시혼합계통중적중요연구방향,Checkmate시기우MATLAB/Simulink화Stateflow공구상개발적일충혼합계통건모、방진화형식험증공구.문장수선개소료혼합계통형식험증적개념화험증과정,종용호적각도개소료 CheckMate적매개자정의모괴적설치급기공능원리,통과일개삼유선성혼합계통적례자,설명료사용CheckMate진행건모、방진이급험증적방법,최후지출료CheckMate험증공구적국한성.
The formal verification is an important research direction in hybrid svstems.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 systern example.Finally,the limitations of the verification tool CheckMate are presented.