张 磊，马光胜

(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)一个事件是相关的如果：

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

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