基于形式化方法的混成系统安全性检验

《基于形式化方法的混成系统安全性检验》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、基于形式化方法的混成系统安全性检验第一章绪论1.1研究背景随着信息技术的发展，传统的物理系统、控制系统等发生了巨变。诸如信息物理融合系统和智能控制系统等新型系统快速发展，并已经深入到日常人们生产生活的方方面面。例如：飞行系统[57]、自动公路系统[30]，列车控制系统[50]以及机器人系统[33]等等。信息物理融合系统是一种综合计算、网络和物理环境的复杂系统，智能控制系统则主要处理有输入信号的动力系统的行为。这两类系统都包含各种子系统，它们依靠离散逻辑控制和连续动态行为相互作用，从而实现整个复杂系统的功能。以飞机控制系统为例，典型的飞行控制系

2、统存在多种不同的控制模式来应对不同的飞行模式和各种突发状况，如飞行速度、飞机的所处的高度、飞机的飞行角度等系统中的重要参数都会随着时间连续变化。飞机在飞行过程根据不同的气象环境对于飞行模式进行调整，而在不同的飞行模式中，飞机的这些参数的变化规律完全不同，并且对各种事件的响应方式也有所区别。由飞机系统的例子可以看出，通过逻辑控制和时间性的交错地有机结合，构成了可以实现重要功能的复杂系统[42]。混成系统(HybridSystems)是离散事件与动态系统的混合体，它同时具有离散事件的瞬时性和连续动态系统的实时性。信息物理融合系统和智能控制系统等

3、都是典型的混成系统的例子。这些系统都属于安全攸关系统一系统的失误、错误或者失效会造成人身损伤甚至死亡，或者严重的设备损坏，或者环境的危害。现代社会工业发达，安全攸关系统的应用越来越广，对日常生产生活的影响不可小视，任何这些系统细小的失误都可能导致非常严重的生命财产损失。因此，对于这些系统的安全性保证异常重要。.1.2国内外研究现状混成系统是离散系统与连续时间动态系统的有机结合，因此对混成系统的安全性研究可以从单独的离散系统与连续时间动态系统的研究着手。对单独的离散系统和连续时间动态系统的安全性验证己经有了较为成熟的理论方法。针对离散系统的安全

4、性验证主要有两类方法：模型检测[15]和演绎式推理[40]。模型检测适用于有限状态空间的系统，对于有连续状态空间的混成系统而言状态空间是无限的，模型检测不能够覆盖全部的状态空间。演绎式推理通过推理规则集合验证系统的性质，但是这个过程中往往需要人工干预，难以达到较高程度的自动化。针对连续系统的安全性验证主要从控制理论的角度出发，有基于系统稳定和鲁棒性分析的一系列算法。对于混成系统来说，理论方法结合和扩展上面离散系统和连续系统的研究成果，并且综合混成系统的特点，主要针对以下问题展开研究：1)如何设计具有准确且有足够表达能力的建模语言来描述混成系统

5、中的复杂行为;2)如何设计有效的模型检验方法、定理证明方法对复杂系统进行研究以验证系统是否满足安全性等性质等[42]。经过近20年的密集投入与研究之后，出现了很多各种混成系统安全性验证的方法：例如[20]中提出利用仿真通过模拟系统的运动轨迹，观察这些轨迹是否始终在安全区域内;[45]中提出通过平方和理论构造障碍函数的来判定系统是否会越过障碍函数进入不安全区域;[43][44]中提出基于微分动态逻辑的形式化验证方法，着重将问题模块化，将问题的形式化分解成为多个子问题进行独立验证，加快了验证速度等等。这些方法各有优势和局限，很多方法已经成功应用

6、到了实际系统的安全性验证中。第二章混成系统的形式化验证2.1混成系统混成系统可以被形象化看作一个图，图的节点内表示连续演变，图的边代表离散转换。混成系统的形式化定义可以用类似混成自动机[h]的概念来定义。对于一个混成系统，给定初始状态集、安全区域和非安全区域，从初始状态集开始的任意状态，经过符合系统定义的离散跳变和连续动态变化之后，不能抵达非安全区域，即状态轨线一直停留在安全区域内。根据定义2对于混成系统安全性的描述，混成系统安全性的向题就是要验证从初始集合出发，系统是否能够达到非安全区域。因此，安全性问题可以很好地对应到可达性问题分析。但是

7、，如文献[1][26]中的讨论，一般情况下混成系统的验证问题是算法上无法判定(un-decidable)的。因此，人们提出了符号的可达性分析算法。符号的可达性算法概要来说就是对于混成系统M，以迭代的方式从其初始状态集计算出混成系统的可达状态集/?。在每一步的迭代计算过程中，算法都会检查状态集是否在安全区域内。如果不在安全区域内，算法会终止并且抛出一个反例;如果在安全区域内，则迭代继续。理论上来说，没有办法保证算法可以终止，因为状态集可能是无穷的，因此此类方法的关键点在于是否能够有效地找出一个可以代表整个混成系统的子状态集。..2.2混成系

8、统的简单实例下面使用温度控制系统作为例子来说明混成系统的性质。一个房间的简单温度控制系统由一个自动调温器控制，自动调温器一直检测室内的温度，如果室内温度超过最大阈值