Formal verification of hybrid systems using CheckMate: a case study
Formal verification of hybrid systems using CheckMate: a case study
复制标题
使用 CheckMate 对混合系统进行形式化验证：案例研究
DOI：
10.1109/acc.2000.879487
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
J. Cury
中科院分区：
文献类型：
--
作者：
T. Niinomi;B. Krogh;J. Cury
我们在截止模式下对文献中四缸四冲程发动机的控制算法进行了正式验证。使用Checkmate对受控系统进行建模，模拟和验证，Checkmate是用于对卡内基梅隆大学开发的混合系统形式验证的工具。 Checkmate自动从混合系统的MATLAB/SIMULINK模型中构造了多面体 - 不变的混合体（PIHA），并使用离散模型近似进行验证。该案例研究说明了如何直接在混合系统动力学模型上执行验证，而无需首先使用定时自动机或线性混合自动机模型构建对连续动力学的近似值。
We present a formal verification of a control algorithm from the literature for a four-cylinder four-stroke engine in the cutoff mode. The controlled system is modeled, simulated and verified using CheckMate, a tool for formal verification of hybrid systems developed at Carnegie Mellon University. CheckMate automatically constructs a polyhedral-invariant hybrid automaton (PIHA) from a Matlab/Simulink model of the hybrid system and performs the verification using discrete model approximations. This case study illustrates how verification can be performed directly on a model of the hybrid system dynamics without first constructing an approximation to the continuous dynamics using timed automata or linear hybrid automata models.