基于形式化方法的混成系统验证

唐敏 吴熊 李平 唐晨 杨国荣

摘 要：对混成系统进行安全性验证是计算机领域具有重要意义和挑战性的课题，传统的测试仿真技术不足以确保系统的绝对安全性和完备性。基于形式化方法是根据混成系统的形式规范与属性，使用数学方法证明其正确性或非正确性。对温控系统实现了抽象算法的形式化，首先对线性混成系统的状态空间进行分割，然后将其转化为图的可达性问题，利用图算法求解，最终对系统进行了安全性验证。实验结果表明，采用形式化方法对混成系统进行安全性验证具有较高的可靠性与可信性。

关键词：形式化方法；抽象算法；混成系统；温控系统

DOI：10.11907/rjdk.172346

中图分类号：TP301

文献标识码：A 文章編号：1672-7800（2018）004-0039-03

Abstract：The safety verification of hybrid systems is an important and challenging subject in the computer field. The traditional test and simulation technology is not enough to ensure the absolute security and completeness of the system. The formal verification method is based on the formal specification of hybrid systems and properties， using mathematical method to testify its correctness. We implement the formalization of the abstraction algorithm to verify the safety of temperature control systems. We first divide the state space of a linear hybrid system into several parts， and then transform it to the reachability problem of a graph， finally we use graph algorithm to verify the safety of this system. Compared with the simulation and testing methods， the formal method has higher reliability and credibility.

Key Words：formal methods； abstract algorithms； hybrid systems； temperature control systems

0 引言

混成系统是由连续变量系统和离散事件系统相互作用而构成的一类动态系统。连续变量系统的动态特征随时间推移在不断演化，离散事件系统的动态演化则受事件的驱动，两者相互作用使系统表现出更加复杂的动态行为[1]。以统一化、一般化的模式对混成系统进行深入研究，形成了当今控制科学与计算机科学界的前沿热点。一般来说，保障软件质量与系统稳定的主要方法可以采用测试和仿真，但传统的测试仿真[2]不足以确保系统的绝对安全性和完备性[3]，模型检测[4]与演绎推理[5]适用于有限状态空间的系统，对于无限状态的混成系统，不能覆盖其全部状态空间。形式化方法则是基于数学基础，对系统进行说明、设计及验证，包括语言、技术与工具[6，7]。本文基于形式化验证理论，结合形式化技术对混成系统模型的可达性及安全性验证进行研究，并将形式化方法具体应用到温控系统中。

1 混成系统形式化定义

令房间初始温度为20℃，加热器处于关闭状态，初始状态为（loff，x0），x0=20，c=0。从安全性上描述该系统，在加热器工作期间，能够确保房间内的温度保持在安全区域，保证温度处在最低温度与最高温度范围内。

2 基于抽象形式化验证方法

由于混成系统复杂性高，可达状态可能是无穷的，导致从初始状态集计算所有可达状态变得困难甚至不可能。利用抽象来减少复杂度，通过对状态空间进行分割，将混成系统分成多个有限的状态空间，然后将混成系统的安全性验证问题转换为图的可达性分析问题进行验证。

2.1 相关概念

为了进一步说明抽象方法的思想，引入混成系统的几个重要概念。

2.2 抽象算法

抽象算法[9]的关键在于抽象状态的安全性与混成系统实际的状态空间安全性直接的对应关系。抽象算法的基本步骤为：①抽象化混成系统的状态空间；②利用有效转换，把混成系统的安全性问题转化为图的可达性分析问题；③利用图算法对其进行求解。以恒温器为例阐述抽象算法的实现。

假设一个恒温系统具有3种工作状态：①Heat：加热；②Cool：制冷；③Check：在不加热不制冷的状态下自我检查。恒温器的连续状态空间有两个变量：①环境温度，用T表示；②内部时钟，用c表示。使用不变式谓词描述每个工作状态所允许连续变量值的范围。恒温器系统模型如图2所示。

2.2.1 抽象状态空间

有几种方法来抽象状态空间，它可以将状态空间抽象为多面体，或将状态空间抽象为网格。混成系统行为比较普遍复杂，导致抽象算法主要停留在启发式阶段。状态空间的抽象算法包含3个部分：守卫函数、重置函数和边界值。把恒温器系统在Heat位置时的状态空间进行分割，如图3所示，灰色区域显示的是在Heat状态下不定式的不可达区域。

2.2.2 抽象函数

抽象函数指系统允许抽象的离散或者连续转换[9]。采用overestimate技术描述，用多个转换来代替系统原有的转换→ACD，但是要确保初始状态等于最终状态，如图4所示。恒温器系统在区间[0.5，1）×[5，6）中，所有可能的抽象转换用箭头描述。

c2.2.3 抽象算法

由2.2.1中得到的每一块区域作为有向图的顶点，将2.2.2中抽象函数转化为有向图的边，实际研究内容转变为解决图的可达性问题。采用深度优先算法，流程描述如下：

hash_map=new Hash_map（）；

while hash_map->T ！=null do

stack=new Stack（）；

（l，b）=hash_map.pop（T）；

Stack.push（（l，b））；

while（！stack.isEmpty（））

if==null return stack；

if stack.top（）！=null

（l，b）=stack.top（）；

stack.push（（l，b））；

else if stack.top（hash_map->PostC）！=null

（l，b）=stack.top（hash_map->PostC）；

stack.push（（l，b））；

else stack.pop（）；

算法描述如下：设哈希表hash_mapA存放所有待访问的状态，hash_mapB存放所有已经访问过的状态。

（1）选取初始状态集的一个点作为初始状态，将其放入hash_mapA中。

（2）如果hash_mapB的集合小于状态空间，就取hash_mapA中的一个状态（l，b）放入栈里面。如果栈顶不为null，循环做以下操作：①检查栈顶元素（l，b）是否满足安全条件，满足取其元素，不满足跳出循环；②检查是否访问过（l，b）的离散后继。如果未访问，取其全部离散后继放入hash_mapA；③检查是否访问过（l，b）的连续后继。如果未访问，取其全部连续后继放入hash_mapA；④否则，将状态（l，b）放入hash_mapB。

（3）如果栈为空，表明系统安全；否则说明系统存在状态的可达状态为不安全区域，系统不安全。

抽象算法是形式化验证研究的一种新方法，以恒温器作为实例，研究得出恒温器系统在Heat状态下的安全性验证形式化抽象算法。Heat状态下的抽象状态空间由图3决定，在该状态空间中，随机抽取下面两组状态集作为待检测状态（状态仅检测T）：{2.5，4.5，3.6，8.7，2.2}和{5.6，4.5，10.6，7.6，3.8}，分别代入上述算法的具体实现中，验证结果如下：“可达状态空间不存在不安全区域”和“可达状态空间存在不安全區域”。

3 结语

验证混成系统的安全性是十分困难的问题，传统算法难以判定[10]。抽象方法降低了问题的复杂度，把系统的状态空间映射到抽象状态集，同时确保系统的行为保持一致性。混成系统有多种抽象方式，如连续系统可以被抽象成离散系统；非线性系统可以被抽象成线性系统等。本文基于形式化方法，根据混成系统的形式规范和属性，并结合抽象方法，对混成系统的安全性进行验证，使用数学的方法证明其正确性或非正确性。与仿真、程序测试方式相比，形式化方法具有更高可靠性与可信性。

参考文献：

[1] SCHAFT A， SCHUMACHER J M. An introduction to hybrid dynamical systems[M]. Beijing： Tsinghua University press，2007.

[2] GLOVER W， LYGEROS J. A stochastic hybrid model for air traffic control simulation[J]. Hybrid Systems： Computation and Control. Heidelberg： Springer-Verlag，2004：372-386.

[3] 古天龙.软件开发的形式化方法[M].北京：高等教育出版社，2005.

[4] EDMUND M C， ORNA G， DORON P. Model checking[M]. Cambridge： MIT Press，2000.

[5] MANNA Z， PNUELI A. Temporal verification of reactive systems[M]. Heidelberg： Springer-Verlag，1995.

[6] LEE E A， SESHIA S A.嵌入式系统导论CPS方法[M].北京：机械工业出版社，2011.

[7] GEUVERS H， KOPROWSKI A， SYNEK AUTOMATED D， et al. Machine-checked hybrid system safety proofs[M]. Heidelberg： Springer-Verlag，2010.

[8] BERTOT Y， CATERAN P.交互式定义证明与程序开发——Cop归纳构造演算的艺术[M].北京：清华大学出版社，2010.

[9] 李倩.基于形式化方法的混成系统安全性验证[D].上海：华东师范大学，2015：12-46.

[10] GULWANI S. Automating string processing in spreadsheets using input-output examples[J]. ACM Sigplan-sigact Symposium on Principles of Programming Languages，2011，46（1）：317-330.

（责任编辑：刘亭亭）