基于事件集的反应系统模型的验证

张 磊，马光胜

(1.黑龙江东方学院 计算机科学与电气工程学部,黑龙江 哈尔滨150008;2.哈尔滨工程大学 计算机科学与技术学院,黑龙江 哈尔滨150003)

本文在没有其他模型检测工具的情况下使用UML状态图验证已建模的反应系统。反应系统在这里认为是面向状态并对外部或内部行动做出反应，反应有可能产生状态或行为的变化，一个反应系统（事件驱动）的行为由一系列的状态、事件和行为集所规范。

1 提出的验证技术

1.1 假设

假定正在考虑中的系统有多个合作的对象，这些对象通过事件相互联系。每个对象的动态行为都用UML状态图建模。这些对象在接收一个正确的外部或内部产生事件及相应的保护条件变为真实状态发生改变。要验证的属性用时态逻辑表示并由符号φ代表。验证过程包括每个UML状态图到一个元组{Si,Ei,Ti,Ii}形式的转换。其中i代表对象，Si代表非空有限的状态集，Ei代表事件集，Ti⊆Si×Si是一套转换集。Ii⊆Si是一套初始状态集。让 Et为总的事件集即 Et={E1∪E2…En},其中 n是系统对象的数量[1]。

1.2 基于事件的验证方法

一旦在Et中所有事件都发生时就合并所有对象的状态转换来建造系统的状态空间,在状态空间 (on the fly)的状态图中找到表示为┐φ的错误状态(否定行为),如果终止了更深层的状态空间的搜索，就会演示出错误轨迹（反例）。

本节中描述的算法[2]如下：

(1)一个事件是相关的如果：

①存在着一个与这个事件相关的转换并且当前状态是一个错误状态（┐φ）

②存在于一个与这个事件相关的转换并且下一个状态为一个错误状态（┐φ）

(2)一套事件是相关的如果：

存在着一套与这些事件相关的转换，并且能将对象从最初状态转到错误状态（┐φ）。即将对象从一个对象的最初状态转到错误状态的事件集合叫做相关的事件集。

相关事件集计算完，每个对象的UML状态图都转换成这种元组{Si,Eri,Ti,Ii}，其中Eri代表联系对象 Oi的相关事件集，Ert代表总的相关事件集,即 Ert={Er1∪Er2∪…Ern}。搜索状态空间只考虑在总的相关事件集Ert中的事件。一旦到达了错误状态或访问了所有的状态，就终止搜索状态图。

2 实例研究

(1)火车道口问题是实时系统中的一个典型问题。火车道口系统用来操纵道口的栏杆。对于两个铁轨上的门位于区域 A上，火车在两个铁轨（T1,T2）上任意方向运行[3]。图 1中显示了已经定位的传感器(S1,S2,S3,S4和 S5)。传感器表明当火车行驶到区域A、进入RC、离开区域A或退出RC。传感器S5表明门是关着的还是开着的。“占用期间”指RC上有一个或更多火车的时期。系统被期望满足如下的属性：

①道口在所有占用期间是关闭的(安全)；

②如果占用期间没有火车,道口是开放的(实用性)；

③道口在尽可能的时间里是开放的(活性)。

(2)GRC的UML状态图模型

对象道口栏杆和铁轨的动态行为用UML状态图规范化了，如图2所示，栏杆的UML状态图显示了一个最初状态和4个简单状态，即开着、正关闭、关闭和正打开。栏杆通过正打开和正关闭对外界信号做出反应[4]。每个正交区域都有一个最初状态和5个简单状态。

2.1 状态空间的构建

对象铁轨有两个正交状态Track1和Track2。对象栏杆有4个局部状态，Track1有5个局部状态，Track2有5个局部状态。GRC系统的 U包括（4×5×5）100个状态。通常模型限定可到达状态的数量。表1显示了所有可能的状态。

表1 所有可能的状态

2.2 基于事件的算法应用到火车道口系统

在GRC模型中要检测的安全属性“当火车在Track1或 Track2上的 RC时，道口始终关闭”[5]，时态逻辑表示为：(T1.Crossing∨T2.Crossing)⇒G.Closed，如果成立则此模型有漏洞，产生一个反例/错误轨迹[3]，否定形式表示为 ：(T1.Crossing∨T2.Crossing)⇒ ┐(G.Closed)，这 就 意 味着火车通过时大门开着或正开着或正关闭的状态中。

图3中，状态搜索从最初状态 S1开始，由事件“tkevarrive”引发的后续状态为 S2、S5、S6，随便选择状态 S2进行更深层的搜索[6]，直到到达状态 S15，它不响应任何相关事件，所以回来遍历状态S29后，会产生由事件“tkevexit”引发状态 S42。 状态 S42是一个错误状态，因为它违背了安全属性（即当一个火车经过道口时，大门是开着的），一旦状态搜索终止，反例和错误轨迹就能产生(如图4)，产生反例的路径长度为6。同理如果遍历S29后又遍历S45，也会违背安全属性，也会产生路径长度为6的反例。

3 结果及讨论

3.1 GRC模型的改进

图4中的错误轨迹描绘出栏杆打开时，当一个火车穿过RC时就会导致错误的状态，模型中的这个漏洞可以通过保证占用期间没有火车后才允许栏杆打开的情况下予以避免[7]，对象栏杆的正确的UML状态图。将全局变量“train count”加进了模型中，它当每次火车进入道口时递增，火车离开道口时递减。

3.2 算法的执行

通过在状态搜索期间减少遍历状态数量方面验证该算法，在带有6个状态的GRC的UML状态模型中，由每个对象的状态图组合成相关事件集构成的状态空间后，即状态空间中仅由19个状态组成，在检测违反安全属性方面，将基于相关事件的算法应用到GRC系统后，只搜索遍历整个状态空间的41%，状态空间大大减少，并产生长度为6的反例（见表2）。

表2 算法的执行

[1]周清雷,姬莉霞,王艳梅.基于UPPAAL的实时系统模型验证[J].计算机应用,2004，24(09):129-131.

[2]李勇,李宣东,郑国梁.实时系统时段性质的模型检验[J].计算机科学,2002，29(11):165-167.

[3]徐雨波,晏荣杰.一种基于有限精度时间自动机的模型检测工具[J].计算机应用研究,2006(05):121-125.

[4]LANGE E.The degree of realism of gis-based virtual landscapes:Implications for spatial planning[C].In:D.Fritsch and R.S piller(eds),Photogrammertric Week’99,Herbert Wichmann Verlag,Heidelberg,1999:367-374.

[5]HENZINGER T A,JHALA R,MAJUMDAR R,et al.Software verification with blast[C].in Proc.of 10th SPIN Workshop on Model Checking Software(SPIN),LNCS 2648.Springer-Verlag,2003:235-239.

[6]BEER I,BEN-DAVID S,EISNER C,et al.Rulebase-an industryoriented formal verification tool[C].in Proc.of 33rd Design Automation Conference(DAC).Asociation for Computing Machinery,1996:655-660.

[7]MIKK E,LAKHNECH Y,HOLZMANN G,et al.Implementing statecharts in promela/spin[C].in Proc.of 2nd IEEE workshop on industrial strength formal specification techniques WIFT’98,1998:90-101.