UML状态图的检测算法生成

王佳婧++冯长宝++佟鑫

摘 要在软件系统设计中，经常应用UML 状态图对系统行为进行完整建模，其正确性尤为重要。在其他文献中虽然已提出基于HA和EMC的检测规则，但是并未给出具体算法。因此根据算法生成的关键问题主要探讨：基于状态图HA的自动生成及存储、基于HA的Kripke自动生成、以及基于Kripke结构和EMC检测规则的算法实现。

【关键词】HA自动生成 Kripke自动生成 检测规则算法实现

1 引言

UML状态图检测采用HA的Kripke结构表示，使多对象组成的复杂软件系统的行为状态层次清晰，使对象内状态转换与整个系统的状态转换之间关系表达更加直观。在其他文献中已经提出了基于此种结构及EMC思想的检测规则。其算法生成的关键问题如下：状态图如何自动转换为HA；如何基于HA存储结构自动生成其Kripke结构；如何基于Kripke结构和EMC思想的检测规则实现算法。下面将围绕上述三个主要问题对检测算法生成进行探讨。

2 HA的自动生成

2.1 HA的逻辑结构

当系统比较复杂时，其状态图的往往代表多个对象的状态行为，并且对象之间的状态通过事件互相影响。如图1所示在系統内部，状态S1内仍有状态转换，此说明系统内初始运行对象的状态转换，例如当通过事件r1由S1内子状态S6跳转S2时，那么就是系统内S2所代表的另一个对象开始工作。从上述描述可以看出，系统状态图内具有明显的层次关系，按照其层次关系转换为HA（如图2所示）。其逻辑结构各个顺序自动机之间关系与树的结点之间关系相同，例如：顺序自动机A0其为根自动机，其无父状态，只有一个根自动机，具有树只有一个根结点的特征；除根自动机外，其他顺序自动机A1和A2只有一个父状态s1与之相对应，与树中每个结点只有一个双亲结点相同；同一个父状态的顺序自动机互为兄弟。如果将HA的每个顺序自动机看成结点，那么按照传统树的结点间的关系每个顺序自动机的双亲结点应该同样是一个顺序自动机，但是顺序自动机的双亲是某个顺序自动机中的状态。基于此种区别，顺序自动机的在双亲结点包括了其父状态及父状态所属的顺序自动机。由于每个结点内是一个顺序自动机，即一个状态图，因此结点内的结构可以采用有向图的结构：每一个状态就是一个顶点，状态间的迁移关系即顶点间的邻接关系，状态件迁移事件即有向图中顶点间的权值。综上所述，HA的层次关系基于树结构描述，顺序自动机基于有向图结构描述。

2.2 HA的存储结构

HA的每个状态其子顺序自动机的数量没有限制，即树中每个结点其孩子结点数量没有限制，需要选择的存储方式能够在统一结点存储结构的情况下，存储每个结点和所有孩子结点之间的关系。基于上述原因，采用孩子兄弟表示法即二叉链表，同二叉树的存储结构一致，此种方法通过每个结点只记录其第一个孩子，通过其孩子记录兄弟的方式记录所有的孩子结点。顺序自动机的有向图存储结构要存储状态、每个状态间的迁移关系及迁移事件。采用有向带权矩阵，每个元素即迁移事件，无迁移关系的状态对应的矩阵元素为0。

3 Kripke自动生成

3.1 关键问题

Kripke结构的M（SH，S0，R，L）定义，SH的生成是首要关键问题。SH是格局并配以格局内某状态的迁移事件，因此先生成格局，再根据格局中的状态遍历每个状态的迁移事件，从而生成SH。由于HA的存储结构基于树及图，因此基于树和图的遍历生成SH，其基本思想是：根顺序自动机图的深度遍历开始，对正在访问的某个状态从左至右遍历的前序遍历的每一棵子顺序自动机，生成格局；遍历每个格局所有状态的顺序自动机的有向带权矩阵，生成SH。例如，如图2，从根顺序自动机A0应用图的深度遍历，访问状态s1后，遍历其子顺序自动机A1和A2，每次各从其自动机中取出一个状态，生成不同的状态组合，从而生成了s1所属的所有格局，C0={s1，s6，s8}， C1={s1，s6，s9}， C2={s1，s7，s8}， C3={s1，s7，s9}；其后，回溯至根顺序自动机A0，访问状态s4和s5，生成格局C4={s2}，C5={s3}。Kripke生成的第二个关键问题为S0，S0为Kripke的初始状态，其格局为初始格局C0，但是迁移事件不固定，可以默认包含C0的第一个状态为初始状态。R代表的是SH之间的迁移关系，受到所处格局和迁移事件影响，例如状态S0其格局C0状态包括{s1，s6，s8}，其迁移事件e1，根据状态图迁移关系为

，S0可迁移包括格局A2的状态S7、S8及S9。R的迁移关系中迁移事件已经包含在状态内，所以Kripke状态间的迁移关系可以通过邻接矩阵存储。L为每个状态原子命题集合，为该HA具备的所有基本性质，每个状态的基本性质，即在该状态的格局和迁移关系下满足的基本性质，例如图2Kripke状态S0满足其格局C0内所有状态在迁移事件e1影响下的基本性质，即只有格局C0中只有状态s6发生迁移，其他未变，此类性质如何保存成为关键。为每个Kripke状态建立一个L，例如S0的集合L0，建立一个邻接表，其格局C0所有状态的迁移情况进行记录，包括了其顺序自动机内迁移状态及迁移的Kripke状态，其生成过程，可以在生成R时同时进行。

3.2 算法

输入：HA存储结构

输出：HA的Kripke结构

1.定义格局数组C[MAX] [MAX]，初始化为空，其长度CLength初始化为0，k初始化为0；

2.定义Kripke状态数组S[MAX]，其长度SLength初始化为0，l初始化为0；

3.深度优先遍历HA的根顺序自动机A[0]

（1）root=A[0].VERTEX[K]，栈s初始化为空；

（2）循环直到root为空且栈为空

a.循环直到root为空

将root保存到栈中；

继续遍历root的左子树顺序自动机顶点VERTEX[i]，i=i+1；

b.如果栈s不为空，则

如果root的右子树为空，循環读取栈的元素输入到C[k][MAX]数组，k=k+1；

弹出栈顶元素至root；

准备遍历root的右子树顺序自动顶点VERTEX[j]；

4.CLength=k，k=0；

5.循环直到k=CLength

（1）循环直到C[k] [MAX]为空

a.j初始化为0；

b.遍历状态C[k] [j]的有向带权矩阵arc所处m行

S[l].C= C[k] [MAX]， S[l].E=arc[m][j]；

j++，l++；

（2） k++；

6. SLength=l，l=0；

7. R[SLength][SLength]数组初始化为0， L[SLength]初始化为空

8.循环直到l=SLength

（1） m=0；

（2）循环直到S[l]找到所有迁移状态

a. S[m]如果是S[l]迁移状态，R[m][l]=1；

b. 将此命题相关原子命题记录L[l]

c.m++

（3） l++；

4 检测规则的算法生成

已在文献[3]中提出了基于LTL和CTL的检测规则，这里不重复描述，主要讨论基于此规则和HA的Kripke存储结构的算法生成相关问题。检测规则算法生成中的首要关键问题命题如何输入表示，命题在初始输入时，分解输入，存入命题数组P[n]。 每个命题单元p[i]包括表达式包括五部分： p[i].no（是否非运算）、p[i].Sout（迁出状态）、p[i].E（迁移事件队列）、p[i].Sto（迁入状态）、p[i].logic（逻辑运算符）。其次是每个命题单元如何分解成原子命题的形式，可以通过迁移事件队列从Sout进行逐步迁移分解。最后，如果发现新的命题成立记录LP[MAX][MAX]数组中，便于后续帮助其他命题判断。具体算法如下：

输入：HA的Kripke存储结构，命题P[n]，成立命题LP[MAX][MAX]

输出：命题是否成立

1. 遍历LP[MAX][MAX]看是否存在P[n]，若存在结束；

2. i初始化为0，flag[n]初始化为1；

3.循环直到i=n；

（1） C= p[i].Sout的格局；

（2） e=p[i].E；

（3） 循环直到e为空

a.遍历C格局的所有状态迁移事件，若e不存在、p[i].no=1则结束当前循环， 若e不存在且e且p[i].no=0且flag[i]=0结束当前循环；

b.C=经过e迁入格局

c.e=p[i].E出队事件；

4.，flag[n]之间用将p[n].logic连接计算，若结果为1，P[n]存入LP[MAX][MAX]；

5.输出结果。

5 总结

在以往的相关文献中提出了基于Kripk的复杂演绎判断规则及形式化语义推导的理论，但较少给出实际算法，缺乏实用性。针对上述问题，基于已提出的检测规则，从存储结构HA定义、Kripke结构生成及基于Kripke结构检测规则算法实现进行讨论，给出了具体存储结构及算法，算法易于理解与实现，具有非常重要的实际意义。

参考文献

[1]Latella D，Majzik I，Massink M. Towards a formal operational semantics of UML Statechart diagrams.In：Ciancarini P， Fantechi A，Gorrieri R，eds.Proceedings of the 3rd International Conference on Formal Methods for Open Object-Oriented Distributed Systems. Boston：Kluwer Academic Publishers， 1999：15-18.

[2]边计年，薛宏熙，苏明，吴为民.数字系统设计自动化[M].北京：清华大学出版社，2005（07）.

[3]王佳婧.基于EMC和HA的UML Statecharts检测研究[J].通讯世界，2017（16）.

作者简介

王佳婧（1982-），女，吉林省吉林市人。硕士学位。现为吉林动画学院讲师。研究方向为计算机应用技术。

作者单位

吉林动画学院 吉林省长春市 130012