基于 Kripke 结构的 UML 状态图的形式语义和自动证明1.doc

《基于 Kripke 结构的 UML 状态图的形式语义和自动证明1.doc》由会员分享，可在线阅读，更多相关《基于 Kripke 结构的 UML 状态图的形式语义和自动证明1.doc（9页珍藏版）》请在三一办公上搜索。

1、精品论文推荐基于 Kripke 结构的 UML 状态图的形式语义和自动证明1赵也非，杨宗源，谢谨奎 华东师范大学信息学院计算机系，上海 (200241) E-mail: derekzhaoecnu摘要：给 UML 赋予形式化的动态语义，可以在软件生命过程早期，对系统进行自动推导 和证明。把模型检测应用于 UML，是在软件架构中引入形式化方法的一个重要方向。本文使用 UML 状态图表示变量值的迁移，而非系统状态的迁移，以处理不能穷举系统有限状态 自动机的情况；显式的提出了 UML 状态图和 Kripke 结构语义的映射关系；最后，用实验验 证了该理论的有效性。本文提出的映射规则是双射的，因此，既

2、可以应用于设计阶段的软件正向工程，又可以应用于实现阶段的逆向软件工程。关键词：UML；状态图；Kripke 结构；模型检测；软件架构 中图分类号：TP311.51. 引言UML(Unified Modeling Language)是一种图形化的面向对象建模语言，包括类图，对象 图，状态图，序列图，构件图等，可以描述系统的静态拓扑结构和动态行为。现在 UML (1, 2)已经成为工业界事实的标准建模语言。但是，UML 是一种元模型，只有静态语义，没有 形式化的动态语义，不能对系统进行自动推理和证明。模型检测(3, 4)技术使用时态逻辑描述系统属性，使用 Kripke 结构表示系统状态空间， 可以

3、自动的穷举证明系统属性是否在状态空间上成立。现在模型检测技术已经广泛应用于硬 件验证，通信协议分析，临界安全系统验证等。但是 Kripke 结构的抽象层次较低，模型检 测通常是以文本（代码）的形式，出现在系统实现阶段，而非设计阶段。近年来，把模型检测应用于软件架构，已成为一个重要方向。P. Inverardi(5,6)在设计 阶段引入类 UML 图符，构造 UML 图符到 ADL 的映射，通过层层模型精化，转换为 SPIN 代码。该理论已形成一套框架 CHARMY，应用于软件设计阶段。V.S.W. Lam(7)提出，把 UML 状态图转换为 pi-calculus，再根据 LTS 结构到 Kr

4、ipke 结构的映射关系，将其转换为 SPIN 代码。文献(8,9,10)首先给 UML 状态图、活动图赋予操作语义，然后将其转换为模型检 测代码。这些研究的主要思路是：首先给出 UML 图符的操作语义，然后构造系统状态迁移 图，最后生成模型检测代码。本文的研究内容和意义在于：(1) UML 状态图的某些子集和 Kripke 结构之间，具有隐式的映射关系。本文明确的给 出了定义和映射规则，显式的提出了 UML 状态图和 Kripke 结构之间一对一的映射关系，给 UML 状态图赋予了形式化语义。(2) 在把模型检测应用于软件架构的研究工作中，通常把 UML 状态图（序列图等）的 状态进行泛化处

5、理，使用一个变量记录系统的状态迁移，在很多情况下是有效的。但是，在 不能显式的画出系统的有限状态机时，例如摆渡问题，该方法无效。本文用 UML 状态图表 示变量值的迁移，而非状态的迁移，解决了不能穷举所有系统状态的问题。(3) 实现了 UML 状态图到 Kripke 结构语义的映射之后，使用时态逻辑描述系统的关键 属性。模型检测器可以自动证明该系统属性是否在系统状态空间上成立。1 本课题得到国家自然科学基金(60703004)；高等学校博士点基金(20060269002); 华东师范大学 2007 年优 秀博士研究生培养基金的资助。- 9 -(4) 本文提出的理论，不但可以应用于软件正向工程，

6、即用 UML 状态图以图形化的方法进行系统设计，再根据映射规则，自动生成 Kripke 结构语义；还可以应用于软件逆向工 程，即已知系统的 Kripke 结构语义，可以将其自动转换为 UML 状态图，呈现给用户直观的 图形化设计方案。本文的结构是：第 2 节给出了 Kripke 结构的形式化描述，NuSMV 输入语言是 Kripke 结构的抽象表示；第 3 节，UML 状态图和 Kripke 结构各组成元素之间具有一一映射关系， 并给出定义和映射规则；第 4 节，用 UML 状态图给出了一个临界资源竞争的设计方案，应 用本理论，生成 Kripke 结构语义，对系统关键属性进行自动证明；第 5

7、节是结论和展望。2. Kripke 结构和 NuSMV 输入语言Kripke 结构是一个四元组，k = ( Qk ,I k ,k ,Lk )。Qk 是有限状态的集合；I k Qk ，是初始状态的集合；k Qk Qk ，是一个迁移关系，表示一个状态演化到其后继状态；Lk :kQ 2 AP ，是一个函数，输入一个状态，返回在该状态成立的原子断言的集合。使用 Kripke 结构，可以表示系统的静态拓扑和动态行为。每个系统状态，和在该状态 中成立的原子断言的集合相联系。NuSMV(11, 12)是基于 Kripke 结构的自动模型检测器，用于证明用时态逻辑描述的、 有限状态系统的属性。NuSMV 输入

8、语言，用系统内变量值的变化，表示状态之间的迁移， 是 Kripke 结构的高层抽象表示。使用 NuSMV 输入语言，作为 Kripke 结构的抽象表示。一个模块(module)的定义分为三部分：变量定义，变量的初始化，在下一状态变量值的 改变。模块之间的组装，分为同步组装和异步组装，模块之间的参数传递是通过按引用调用 (call-by-reference)。3. UML 状态图的 Kripke 结构语义3.1 变量声明定义 1 变量声明. 函数 VD: Vname Vtype。输入 Vname，代表变量名，输出 Vtype， 代表变量类型。NuSMV 输入语言的变量类型包括：bool 型，枚举

9、型，整数范围。变量声明的 BNF 范式为：S VAR VD/ 变量声明VD Vname : Vtype; VD | Vname : Vtype;Vname (a.z)Vname | (A.Z)Vname | a| .| z | A | . |ZVtype Boolean | EnumElement | BoundInt/ bool 型，枚举型，整数范围EnumElement Vname, EnumElement | VnameBoundInt StartIndex . EndIndex/ 开始下标.结束下标规则 1. 在 UML 状态图中，符合上述 BNF 范式的文本，映射为 NuSMV 输入

10、语言中的 变量声明。下面是 NuSMV 代码中，变量声明的一个典型例子：VAR x : boolean; color : red, blue, green; n : 2.9;3.2 变量初始化定义 2 变量初始化. 函数 VI：Vname Vvalue，给一个变量名 Vname，赋予一个初始 值 VvalueNuSMV 输入语言的变量初始化语句的 BNF 范式为：S ASSIGN VI/ 变量初始化VI init(Vname) := Vvalue; VI | init(Vname) := Vvalue;Vvalue true | false | (value EnumElement) | (n

11、um BoundInt)Vname 在上一节中定义，Vvalue 要在变量定义类型的取值范围之内，否则为非法。规则 2.在 UML 状态图中，初始状态内部的变量赋值，若符合上述 BNF 范式，则映射 为的 NuSMV 输入语言的变量初始化。图 1 变量初始化 实心圆圈表示初始点，起始点指向的状态是初始状态。初始状态内部是变量赋值。 由定义 2 和规则 2，图 1 所示的 UML 状态图，可以生成 NuSMV 代码：ASSIGNinit(x) := true; init(color) := green; init(n) := 3;3.3 变量值的顺序迁移变量值的变迁包括 3 种：顺序迁移，无冲突

12、选择迁移，有冲突选择迁移。定义 3 变量值的顺序迁移. 函数 ST: Vname VnextExp，对一个变量名 Vname，变量值 的变迁有且只有一种可能 VnextExp，VnextExp 是合法的变量运算表达式。顺序迁移的 BNF 范式为：S ASSIGN VN/ variable next() statementVN next(Vname) := Expression; VN | next(Vname) := Expression Expression Expression Operator Expression | Operator Expression | Vname Operat

13、or + | - | * | / | mod | & | ! | .规则 3. 在 UML 状态图中，var 在源状态中，exp 在目标状态中，若 var Vname exp VnextExp，则映射为符合上述 BNF 范式的 NuSMV 输入语言中的变量值顺序迁移。图 2 变量值的顺序迁移使用 UML 状态图表示变量值的变化，而不是不同状态之间的迁移。根据定义 3 和规则3，图 2 所示的 UML 状态图，可以生成相应的 NuSMV 代码为：next(b0) := !b0;3.4 变量值的选择迁移定义 4 变量值的无冲突选择迁移. 函数 VNC：Vname coni VnextExpi ，V

14、name 是变 量名，coni 是第 i 个卫式条件，VnextExpi 是第 i 个表达式，且对 coni ，存在 j 1.n，i1.n使得 coni =true，且对任意的 k 1.n，k j conk =false无冲突选择的 BNF 范式为：S ASSIGN VNC/ variable next case statementVNC next(Vname) := ConExp esac/ ConExp: Condition ExpressionConExp Condition : Expression; ConExp | Condition : Expression;其中，Conditi

15、on 表示卫式条件，Expression 表示表达式。规则 4. 在 UML 状态图中，一个变量名，在不同的卫式条件下，有且只有一个卫式条 件成立，则此变量被赋予一个确定的值。在 NuSMV 输入语言中，映射为符合上述 BNF 范 式的 NuSMV 输入语言的变量值无冲突选择迁移。图 3 变量值的无冲突选择迁移根据定义 4 和规则 4，图 3 所示的 UML 状态图，生成的 NuSMV 代码为：next(v) := case con1 : E1;con2 : E2;conn : En;定义 5 有冲突选择迁移. 函数 STC：Vname ( coni VnextEXpi )，对 coni ，i

16、1.n j,k 1.n，使得 con j =true conk =true j k。有冲突选择的 BNF 范式，和无冲突选择迁移的 BNF 范式相类似，不再赘述。规则 5.在 UML 状态图中，一个变量名 Vname，在不同的卫式条件( coni )下，可能有多 个卫式条件成立，则此变量被非确定选择的赋予一个表达式(VnextEXpi )。在 NuSMV 输入 语言中，映射为符合上述 BNF 范式的变量值有冲突选择迁移。图 4 是 UML 状态图中，变量值有冲突选择迁移的一个典型例子，可以应用定义 5 和规则 5，生成相应的 NuSMV 代码。3.5 同步并发组合图 4 变量值的有冲突选择迁移

17、上一节我们讨论了 UML 状态图和 NuSMV 输入语言的模块定义之间的映射关系，本节 会讨论模块间的嵌套关系。一个模块可以由若干个子模块组成。定义 6 同步并发组合.同时移动。V1 |V2 | Vn ，n 个类型为 module 的变量并发组合，且按一步同步并发组合的 BNF 范式为：S VAR VD/ variable definitionVD Vname : Mname; VD | Vname : Mname;/ 约束： Mname (module)规则 6. 在 UML 状态图中，若干个状态的并发组合，在 NuSMV 输入语言中，映射为若干个变量，且其为符合上述 BNF 范式的，已定义

18、模块的实例化。如图 5 所示，模块 main 由 3 个子模块 bit0，bit1, bit2 组成，这 3 个子模块是同步并发 组合关系，假设已定义了一个模块 counter。bit0，bit1，bit2 是 cell 的实例化，且这 3 个模 块按一步移动。图 5 同步并发组合根据定义 6 和规则 6，图 6 所示的 UML 状态图，对应的 NuSMV 代码为：Module cell(in)Module mainVAR bit0 : cell(1); bit1 : cell(bit0.done); bit2 : cell(bit1.done);3.6 异步并发组合定义 7 异步并发组合.

19、多个模块是异步并发组合的，当且仅当，一步只有一个模块的实 例化移动。异步并发组合的 BNF 范式为：VD Vname : process Mname; VD | Vname : process Mname;模块定义的 BNF 范式为：S Module Mname FAIRNESS running规则 7. 在 UML 状态图中，若干个由初始状态指向的 UML 状态图的并发组合，是异步 并发组合的，且在 NuSMV 中，映射为用关键字“process”定义的模块实例化，且使用关键字“FAIRNESS running”，保证进程的公平调度。图 6 异步并发组合根据定义 7 和规则 7，图 6 所示

20、的 UML 状态图，对应的 NuSMV 代码为：Module counter(in)FAIRNESS runningModule mainVAR b0 : process counter(0); bit1 : cell(bit0.done); bit2 : cell(bit1.done);4. 基于 Kripke 结构语义的自动证明第 3 节定义了从 UML 状态图到 Kripke 结构语义的一对一映射关系，下面使用一个例子， 说明上述理论在系统关键属性自动证明中的应用。图 7 表示一个资源竞争系统，包括两个竞争者 pr1 和 pr2，和一个调度者 arb；arb 是模 块 arbiter 的

21、实例化，当发生临界资源访问冲突时，对两个竞争者进行调度；pr1 和 pr2 是模 块 prc 的实例化，其状态属于集合n,t,c，且不能同时访问临界资源；在 main 主模块中， pr1,pr2,arb 是异步并发组合的，模块之间的参数传递是按引用调用。当临界资源竞争系统包括多个竞争者时，在系统设计阶段，不可能穷举的给出系统的有 限状态自动机，所以，根据本文提出的规则和映射关系，用 UML 状态图表示变量值的变化， 而非状态的迁移，给出该系统的图形化设计方案，如图 7 所示：图 7 临界资源竞争系统的设计方案根据第 3 节的定义和映射规则，图 7 所示的 UML 状态图，相对应的 NuSMV

22、代码是：MODULE mainVARpr1 : process prc(pr2.st, arb.turn, 0); pr2 : process prc(pr1.st, arb.turn, 1); arb : process arbiter(pr1, pr2);MODULE arbiter(usr1, usr2) VARturn : boolean; ASSIGNinit(turn) := 0;next(turn) := caseturn = 0 & usr1.st = c : !turn;turn = 1 & usr2.st = c : !turn;1 : turn; esac; FAIRNE

23、SS runningMODULE prc(other-st, turn, myturn) VARst : n, t, c;ASSIGNinit(st) := n;next(st) := case(st = n) : t,n;(st = t) & (other-st = n) : c;(st = t) & (other-st = t) & (turn = myturn) : c; (st = c) : c,n;1 : st; esac; FAIRNESS running上述 NuSMV 代码是系统的 Kripke 结构语义的抽象表示，使用时态逻辑(CTL，LTL)，描述待验证系统关键属性，诸如活

24、性，安全性，原子性等。手动添加的 LTL 公式是：LTLSPEC G!(pr1.st = c) & (pr2.st = c)该 LTL 公式用于验证系统的安全性，即不可能同时出现：pr1 访问临界资源，同时 pr2也访问临界资源。LTLSPEC G(pr1.st = t) - F (pr1.st = c) LTLSPEC G(pr2.st = t) - F(pr2.st = c)以上 LTL 公式用于验证系统的活性，即任意进程，只要申请访问临界资源，则在以后的某个时刻，即可进入临界区，不会出现死锁。在 arbiter 模块，需要手动添加以下公平路径限制：FAIRNESS turn=1，FAIR

25、NESS turn=0， 即在调度模块内，不会出现任意竞争者永远不被调度的极端情况。实验环境为：操作系统 Red Hat 9.0，2.4G Pentium CPU，1G 内存，模型检测工具 NuSMV2.4.2，实验结果如图 8 所示，LTL 公式(1),(2),(3)的模型检测自动证明结果为 true，表示系统 满足安全性，活性，不会出现死锁，系统调度是公平的。5. 结论和展望图 8 模型检测器的自动证明结果把模型检测应用于软件架构，是软件工程发展的一个重要方向。在给 UML 图符赋予形 式化语义的研究工作中，通常的做法是，首先给 UML 图符赋予操作语义或 pi 演算语义，然 后把系统状态

26、图进行泛化，生成有限状态自动机，最后生成模型检测输入代码。这种方法在 系统状态可以穷举时，是有效的。但是，一些复杂系统的状态无法穷举，或者画出系统状态 的过程，即为求解的结果（例如摆渡问题），这种方法就无效了。我们注意到，UML 状态图的某个子集，和 Kripke 结构语义之间，具有隐式的一对一的 映射关系。所以，本文显式的提出了 Kripke 结构各组成元素的精确定义，给出了 UML 状态图和 Kripke 结构之间的映射规则。最后，用一个临界资源竞争的例子，使用本文提出的定义和映射规则，生成 NuSMV 输入代码，模型检测器给出了实验结果，证明了上述理论是可 行的。本文提出的映射规则是双射

27、的。既可用于设计阶段的正向软件工程，即给出系统的 UML 状态图设计方案，根据映射规则，自动生成模型检测输入代码；又可用于实现阶段的逆向软 件工程，在已知 NuSMV 输入代码的条件下，根据本理论，生成图形化的设计方案。以后的工作，根据上述理论，开发一套从 UML 状态图到模型检测输入语言的自动映射 框架。一条可能的技术路线是：Poseidon for UML XMI 文本格式 Lex/Yacc 词法/语法分析器 NuSMV 输入语言。 把模型检测技术应用于软件工程领域，只能对系统关键属性进行定性分析。我们以后一个可能的研究方向是：在形式化方法中引入时间，概率，使用 Markov 过程，Bay

28、es 公式等 数学工具，在软件需求设计阶段，进行量化分析，得到系统关键属性的量化性能指标。参考文献1 OMG. OMG Unified Modeling Language specification version 1.5, March 2003. http:/www.omg.org2 G. Booch, J. Rumbaugh and I. Jacobson. UML notation guide, version 1.1. Rational Software Corporation, Santa Clara, CA, 1997.3 Clarke E , Grumberg O , Peled

29、 D. Model checking. MIT Press , 2000.4 E Clarke, O Grumberg, S Jha, Y Lu, H Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM (JACM), 2003.5 Muccini H. Software architecture for testing , coordination and views model checking : PhD dissertation .Roma

30、 : Universita degli Studi di Roma La Sapienza Dottorato di Ricerca in Informatica , 2002.6 P Inverardi, H Muccini, P Pelliccione. CHARMY: an extensible tool for architectural analysis. ACM SIGSOFT Software Engineering Notes, 20057 V.S.W. Lam and J. Padget. Symbolic model checking of UML statechart d

31、iagrams with an integrated approach. In Proceedings of Eleventh IEEE International Conference and Workshop on the Engineering of Computer-Based Systems, pages 337346. IEEE Computer Society, 2004.8 G Kwon. Rewrite Rules and Operational Semantics for Model Checking UML Statecharts. LECTURE NOTES IN CO

32、MPUTER SCIENCE, Springer, 2000.9 S Gnesi, F Mazzanti. A Model Checking Verification Environment for UML Statecharts. XLIII Annual ItalianConference AICA, Udine, IEEE Computer Society, 2005.10 R Eshuis. Symbolic model checking of UML activity diagrams. ACM Transactions on Software Engineering and Met

33、hodology, 2006.11 A Cimatti, E Clarke, E Giunchiglia, F Giunchiglia. NuSMV 2: An OpenSource Tool for Symbolic ModelChecking. LECTURE NOTES IN COMPUTER SCIENCE, Springer, 2002.12 A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV : a new symbolic model checker. International Journal on So

34、ftware Tools for Technology Transfer (STTT), 2(4), March 2000. 359Formal Semantics of UML State Diagram and AutomaticVerification Based on Kripke StructureZhao Yefei, Yang Zongyuan, Liu QiangDept . of Computer Science, East China Normal University, Shanghai (200241)AbstractIf UML is formalized with

35、dynamic semantics, automatic verification can be performed for systemmodel in the early stage of software procedure. It becomes more and more important to apply model checking in UML, such that software architecture can be formalized with dynamic semantics. We explicitly proposed the mapping rules b

36、etween UML state diagram and Kripke structure semantics. UML state diagram is used to represent value transition of variable rather than transition of states, thus the situation in that system finite state automata cant be exhausted can be resolved. Finally, a critical resource competition example i

37、s illustrated according to the theory. The mapping rules we proposed are bi-direction, as a result, the theory can be applied in both forward software engineering in design phase and reverse software engineering in implementation phase.Keywords: UML; State diagram; Model checking; Kripke structure; Software architecture