混杂系统模型验证工具的验证效果分析

论文摘要

混杂系统的形式验证技术是利用数学分析方法对混杂系统的安全性进行验证。近十年来,模型验证技术是形式验证研究的主要方法。模型验证技术是指,利用计算机强大的计算功能自动地对混杂系统的数学模型进行整个状态空间中进行遍历搜索,对系统所有可能的运行轨迹进行收敛计算或过近似计算,以检验系统的实现方案是否满足系统的设计要求。论文首先介绍了模型验证的概念和特点,常用的混杂系统建模方法如混杂自动机、混杂Petri网、层次结构和时段演算。分析了可达集的两种计算方法—前向和后向可达集算法,对可达集的过近似方法作了系统的阐述。最后详细介绍了模型验证的国内外研究状况和常用的模型验证工具。针对混杂系统连续子系统和离散子系统相互作用的特点,研究了混杂自动机模、多面体混杂自动机和混杂I/O自动机的建模方法;对于混杂系统的流管道过近似问题,给出了齐诺多面体(zonotopes)的基于中心点和生成元(generators)的表达式和过近似算法,分析了该算法的保守性、封闭性、集合交并处理能力以及收敛性。通过比较凸多面体过近似和齐诺多面体过近似算法的适用对象、计算方法、过近似保守性和随维数增长的计算复杂度,对两种算法的优劣和特点进行了详细的分析。针对常压炉加热炉系统(线性混杂系统)和汽车自适应巡航系统(非线性混杂系统)建立数学模型,抽象出验证问题,给出ACTL验证规范。使用PHAVer和CheckMate验证工具分别对上述两种系统建立混杂I/O自动机模型和阈值切换系统模型,应用齐诺多面体流管道过近似方法和凸多面体流管道过近似方法进行模型检验,对系统的状态可达性和运行安全性进行了分析,并给出验证结论。通过上述结论,分析验证工具CheckMate和PHAVer的保守性、消耗时间和内存空间占用率,对上述两种验证工具的验证效果进行了比较。

论文目录

• 摘要
• ABSTRACT
• 致谢
• 第一章 绪论
• 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.4.1 迁移系统
• 2.4.2 商迁移系统
• 2.4.3 仿真与仿真对
• 2.5 验证规范的形式化语言
• 2.5.1 计算树逻辑CTL
• 2.5.2 基于动作的时序逻辑ACTL
• 2.6 系统的划分
• 2.6.1 混杂自动机可达集的划分
• 2.6.2 商迁移系统的细划分
• 第三章 形式验证工具CheckMate 的介绍
• 3.1 可切换连续系统模块
• 3.2 多面体阈值事件模块
• 3.3 有限状态机模块
• 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 后续研究工作
• 参考文献