文摘
英文文摘
论文说明：图表目录
声明
致谢
第一章绪论
1.1模型验证的概念和特点
1.2模型验证的建模方法
1.2.1混杂自动机模型
1.2.2混杂Petri网模型
1.2.3层次结构模型
1.2.4时段演算模型
1.3模型验证中的可达集
1.3.1可达集过近似方法
1.3.2可达集的表示方法
1.4模型验证工具
1.5模型验证的发展史与研究状况
1.6本文的结构和内容
第二章模型验证的基础概念
2.1混杂系统
2.2混杂自动机
2.3可达集的过近似
2.3.1流管道过近似法
2.3.2问题的声明
2.3.3基本的计算步骤
2.4迁移系统和仿真关系
2.3.1迁移系统
2.3.2商迁移系统
2.3.3仿真与仿真对
2.4验证规范的形式化语言
2.4.1计算树逻辑CTL
2.4.2基于动作的时序逻辑ACTL
2.5系统的划分
2.5.1混杂自动机可达集的划分
2.5.2商迁移系统的细划分
2.5.2细划分的原则
第三章形式验证工具CheckMate的介绍
3.1可切换连续系统模块(Switched Continuous System Block，SCSB)
3.2多面体阈值事件模块(Polyhedral Threshold Block,PTHB)
3.3有限状态机模块(Finite State Machine Block,FSMB)
3.4参数设定
3.4.1初始集和分析区域的参数
3.4.2函数文件
3.5 CheckMate的仿真与验证过程
3.5.1模型仿真
3.5.2验证过程
3.5.3验证结果
第四章形式验证工具PHAVer的介绍
4.1数据类型、运算符和表达式
4.1.1数据类型
4.1.2常量与变量
4.1.3运算符介绍
4.2自动机
4.3执行命令函数
4.3.1输出文件和数据结构选择函数
4.3.2可达集分析函数
4.3.3仿真关系检验函数
4.3.4可达集划分函数
4.3.5自动机操作数函数
4.4参数设定函数
4.5小球系统验证
4.5.1问题的描述
4.5.2建立自动机模型
4.5.3提出验证规范
4.5.4验证过程
第五章CheckMate和PHAVer的验证原理分析
5.1 CheckMate和PHAVer自动机模型比较
5.1.1 CheckMate的自动机模型
5.1.2 PHAVer的自动机模型
5.1.3 两种自动机模型的比较
5.2 CheckMate和PHAVer流管道过近似方法比较
5.2.1 Checkmate的流管道过近似
5.2.2 PHAVer的流管道过近似
5.2.3两种过近似方法的比较
5.3 CheckMate和PHAVer的验证流程比较
5.3.1 Checkmate的验证流程
5.3.2 PHAVer的验证流程
5.3.3两种验证工具的验证流程比较
第六章基于CheckMate和PHAVer的验证结果分析
6.1常压加热炉系统的形式验证
6.1.1常压炉加热系统的数学建模
6.1.2常压炉加热系统混杂自动机模型
6.1.3常压炉加热系统验证规范
6.1.4用PHAVer对常压炉加热系统模型验证
6.1.5用CheckMate对常压炉加热系统模型验证
6.1.6常压加热炉系统的验证结果
6.1.7 PHAVer和CheckMate的线性系统验证效果比较
6.2汽车自适应巡航系统的形式验证
6.2.1汽车自适应巡航系统的数学模型
6.2.2建立汽车自适应巡航系统混杂自动机模型
6.2.3汽车自适应巡航系统的验证规范
6.2.4用PHAVer对汽车自适应巡航系统模型验证
6.2.5用Checkmate对汽车自适应巡航系统模型验证
6.2.6汽车自适应巡航系统的验证结果
6.2.7 PHAVer和CheckMate的非线性系统验证效果比较
第六章总结与展望
7.1本文总结
7.2后续研究工作
参考文献
