混杂系统验证中可达集过近似方法的研究

摘要

混杂系统是连续变量动态系统和离散事件动态系统相结合，并且二者相互影响相互作用的一类系统。混杂系统形式验证是混杂系统的一个研究方向，它是分析在给定的初始条件下，系统的可达集是否都在目标状态集合内。形式验证的目的是检验混杂系统是否在任何环境下都能安全运行。如今混杂系统的形式验证已经成为混杂系统研究的一个热点和难点。
　　 混杂系统形式验证中计算可达集是重要的一步，选用何种可达集表示法对整个验证的精度有重要影响。本文所有的论述均围绕混杂系统形式验证中可达集计算这个主题展开，主要工作有：
　　 1.通过大量的国内外文献阅读，对混杂系统形式验证方法进行整理和总结，对形式验证中可达集分析方法进行归纳，对现阶段混杂系统形式验证的主要问题进行总结。
　　 2.在介绍混杂系统形式验证基本概念的基础上对可达集表示法中的有向矩形壳和凸多面体法进行了较为深入的研究。提出了新的可达集表示方法—有向凸多面体法，这种表示法的特点是以上两种可达集表示法的折中。通过样本点实验分析了三种表示法的计算复杂度，对三种表示法构造的几何体顶点数和面数进行比较。
　　 3.总结了流管道保守性判定方法—观察比较法和误差比较法，针对误差比较法的缺点进行了改进。在此基础上提出了新的流管道保守性判定方法—体积比较法。给出了有向矩形壳和凸多面体混合算法的思想并且在已有的流管道保守性判定方法基础上给出了具体的算法。
　　 4.根据文中提出的有向凸多面体法算法和有向矩形壳和凸多面体混合算法，结合一个非线性分段系统实例编写了验证程序，实现了验证过程。并在计算量和保守性两方面进行了详细的分析比较。分析结果表明：利用文中提出的两算法在验证过程中能够更好地在计算量和保守性两方面达到折中。
　　 5.在对全文研究工作进行总结的基础上，对今后的研究方向作了展望。

目录

文摘

英文文摘

论文说明：图表目录

声明

致谢

第一章绪论

1.1混杂系统的概念和特点

1.2混杂系统的两个例子

1.2.1两容水箱系统

1.2.2汽车运动系统

1.3混杂系统的发展概况

1.4混杂系统研究的主要方向

1.5混杂系统的形式化验证问题

1.5.1形式化验证方法

1.5.2混杂系统形式化验证

1.5.3混杂系统形式验证研究现状

1.6本文的主要内容

第二章 混杂系统验证的基本概念和原理

2.1 混杂系统验证中的基本概念

2.1.1迁移系统

2.1.2商迁移系统

2.1.3仿真关系

2.1.4仿真对

2.1.5计算树逻辑CTL

2.2混杂系统的形式化验证原理

2.2.1混杂系统形式化验证的流程

2.2.2混杂系统建模

2.2.3初始划分

2.2.4混杂系统的流管道近似

2.2.5构造商迁移系统

第三章可达集表示方法研究

3.1可达集表示方法

3.1.1常见的可达集表示方法比较

3.1.2有向矩形壳法和凸多面体法

3.2有向凸多面体法的研究

3.2.1有向凸多面体算法

3.2.2有向矩形壳法、凸多面体法与有向凸多面体法比较分析

3.3实例

第四章形式验证中流管道过近似混合算法

4.1流管道保守性判定方法

4.1.1观察比较法

4.1.2误差比较法

4.1.3体积比较法

4.2有向矩形壳和凸多面体混合算法

4.3有向矩形壳和凸多面体混合算法程序框图

4.3.1以误差比较法作为流管道保守性判断方法的算法程序框图

4.3.2以体积比较法作为流管道保守性判断方法的算法程序框图

第五章验证实例

5.1三维空间非线性系统

5.1.1问题描述

5.1.2建立混杂自动机模型

5.1.3验证规范

5.1.4当可达集用凸多面体和有向矩形壳表示时进行验证

5.1.5当可达集用有向凸多面体表示时进行验证

5.2四维空间非线性系统

5.2.1问题描述

5.2.2建立混杂自动机模型

5.2.3验证规范

5.2.4当可达集用凸多面体和有向矩形壳表示时进行验证

5.2.5当可达集用有向凸多面体表示时进行验证

5.3验证结果分析

5.4使用流管道过近似混合算法进行形式验证

5.4.1使用体积比较法作为保守性评价方法进行验证

5.4.2使用误差比较法作为保守性评价方法进行验证

第六章总结和展望

参考文献