| 基于CheckMate的混合系统建模和验证 |
| |
| 引用本文： | 李健,方敏,李加良. 基于CheckMate的混合系统建模和验证[J]. 合肥工业大学学报(自然科学版), 2010, 33(1) |
| |
| 作者姓名： | 李健 方敏 李加良 |
| |
| 作者单位： | 合肥工业大学,电气与自动化工程学院,安徽,合肥,230009;合肥工业大学,电气与自动化工程学院,安徽,合肥,230009;合肥工业大学,电气与自动化工程学院,安徽,合肥,230009 |
| |
| 摘 要： | 形式验证是混合系统中的重要研究方向,Checkmate是基于MATLAB/Simulink和Stateflow工具箱开发的一种混合系统建模、仿真和形式验证工具。文章首先介绍了混合系统形式验证的概念和验证过程,从用户的角度介绍了CheckMate的每个自定义模块的设置及其功能原理,通过一个三维线性混合系统的例子,说明了使用CheckMate进行建模、仿真以及验证的方法,最后指出了CheckMate验证工具的局限性。
|
| 关 键 词： | 形式化验证 混合系统 商迁移系统 流管道 |
Hybrid system modeling and verification with CheckMate |
| |
| LI Jian,FANG Min,LI Jia-liang. Hybrid system modeling and verification with CheckMate[J]. Journal of Hefei University of Technology(Natural Science), 2010, 33(1) |
| |
| Authors: | LI Jian FANG Min LI Jia-liang |
| |
| Abstract: | 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. |
| |
| Keywords: | formal verification hybrid system quotient transition system flow pipe |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
