基于扩展层次自动机的UML状态图完备性和一致性检验

1、基于扩展层次自动机的 UML状态图完备性和一致性检验基于扩展层次自动机的 U ML 状态图完备性和一致性检验 1 ,2 2 刘晓建, 李战 怀( 1 山东省科学院 自动化研究所 , 山东 济南 250014 ;) 2 西北工业大学 计算机学院 , 陕西 西安 710072摘 要 : U ML 状态图是 U ML 中重要的建模元素之一 , 用以描述软件系统的 离散行为 。完备性和一致性是 U ML状态图模型最重要的性质之一 , 是进一步验证模型行为正确性的前提 。给出 了状态图模型完备性和一致性的定( ) 义 , 研究了对完备性和一致性进行检验的方法 。该方法首先把状态图模 型变换成扩展层次自动

2、机EHA,然后对EHA进行分析。EHA中间格式消除了状态图的复杂性,简化了冲突迁移的优 先级判别 , 便于设计简捷有效的算法对完备性和一致性进行检验 。该方法的主要优点是利用了 EHA 的特性 , 给出 了组合状态上迁移的传播算法 , 解决了完备性和一致性分析的难点 。关键词 : U ML 状态图 ; 完备性 ; 一致性 ; 扩展的层次自动机() 文章编号 : 1000 - 7180 200801 - 0039 - 06中图分类号 : TP31 文献标识码 : AUsing EHS to Check Completeness andConsistency of UML Statemachine

3、s1 ,2 2 L IU Xiao2jian,L I Zhan2huai(1 Instit ute of Auto matio n , Shando ng Academy of Science , Jinan 250014 , China ;) 2 School of Co mp uter , Nort hwest Polytechnical U niversity ,Xi an 710072 , China( ) Abstract : U ML U nif ying Modeling L anguageis a de2facto standard for t he design of sys

4、tems , and has been widely usedto specif y safet y2critical reactive co nt rol systems. Inco mpleteness and inco nsistency are t wo co mmo n specificatio n flaws inU ML State2machines models. The early checking of t hese errors is crucial for system develop ment . This paper gives t hedefinitio ns o

5、f co mpleteness and co nsistency , p roposing an approach to checking t he co mpleteness and co nsistency. Our ap2p roach firstly t ransforms State2machines formalism into a clearerand equivalent intermediate format Extended Hierarchical( ) Auto mata EHA, and t hen checks EHA model for t hese p rope

6、rties.The advantages of EHA allow us to develop an effi2cient and simple algorit hm to check co mpleteness and co nsistency.Key words : U ML statemachines ; co mpleteness ; co nsistency ; EHA法 , 该方法不是直接对状态图模型进行分析 , 而是把 1 引言 它变换成一种等 价的 、结构更清晰的中间表示形式 12 U ML 状态图是 Statechart s 的变种 , 它 在平坦扩展的层次自动机 EHA ,

7、 然后对 EHA 来分析完备性和一致性。EHA中间格式只允许单个状状态机基础上引入了“层 次”、“并发”和“通信”三个机制 , 成为一种高度结构化 、具有很强表达能力的可 态间的迁移 , 消除了状 态图中由于层间迁移、多源/视语言。U ML状态图的核心是状态分 解 、层 间 迁 多目标迁移而引起的复杂性 , 简化了冲突迁移的优 移和并发部件 之间的广播通信机制 。 先级判别 。由于 EHA 中间格式具有显式的树状结文中主 要 研 究 在 嵌 入 式 控 制 系 统 中 , 对 U ML 构 , 使得可以设 计简捷有效的算法对完备性和一致 状态图模型的完备性和一致性 进 行 自 动 检 查 的

8、方 性进行检验 。法 , 提出了一种基于扩展层次自动机的自动检验方收稿日期 : 2007 - 03 - 13() () 基金项目 : 国家自然科学重点基金项目 60736017/ F0202; 国家自然科 学基金项目 60573096态 , 进 入 WO R KIN G 状 态 。由 于 WO R KIN G 状 态 U ML 状态图 2 是 组合状态 , 必须说明进入 WO R KIN G 的哪些子状态 , 这时必须考虑初始状态以说明进入哪些子状态 。 U ML 状态图是对平坦状 态图的扩充 。本节通过事 例 说 明 U ML 状 态 图 中 的 主 要 概 念 。有 关比如 , 当 进 入

9、 WO R KIN G 状 态 时 , 同 时 进 入 IM2U ML 状态图的详细说明参见文献 3 。图 1 是 描 A GE , P IC TU R E 和 SOU ND ,ON 子状态 。() 述电视机状态的 U ML 状态图 。 5 层间迁移 。跨越了状态边界的迁移为间迁移”。图1中迁移o n和off 跨越了状态 WA I T2IN G的边界,因此是层间迁移。()6范围。为了判定迁移的冲突和优先级文献()1 ,3引入了“范围” scope的概念。一个迁移的范围是指该迁移既不退出也不进入的层次最低的“与”状态。在图1中,迁移off 从WO R KIN G迁移至UWA I T IN G ,

10、但是仍然没有超出TV状态,因此TV是迁移off 的范围。图1电视机的状态图模型()7冲突和优先级策略。一般情况下，当一个事()1层次和并发状态。图1中状态TV位于层件发生时，多个迁移可能会同时处于就绪状态，有些次状态的最顶层,包含两个子状态WO R KIN G和就绪的迁移可 以通过特定的优先级策略进行解消,WA I T IN G 。状态WO R KIN G又包含两个 并发子状而那些不能通过优先级解消的 迁移可能会出现冲态IMA GE和 SOU ND，它们之间以虚线隔开。每一突,引起系统行为的非确定性。个子 状 态，如 IMA GE , SOU ND 和 WA I T IN G 又可完备性和一致

11、性3以继续细化为层次更低的状态 。诸如TV , IMA GE ,()在嵌入式控制系统中，控制器通过传感器接收SOU ND和WA I T IN G这样的状态称为“或” O R状态,而把诸如WO R KIN G这样的可以分解为并发 外部环境产生的事件, 并对此作出响应。在这类系()子状态的状态称为“与” AND犬态。所有“与”状 统中,通常使用U ML 状态图描述控制器的内部行态和“或”状态合称为“组合状态” , 而 P IC TU R E 和为以及对外部事件的 响应 。 U ML 状态图模型的完(M U T E这样的无法再分解的状态称为“基本” ba2备性和一致性是这类系统行为模型最重要的性质之

12、 ) sic 状态 。一 , 也是进一步验证行为正确性的前 提 。在嵌入式() 2 状态配臵 。由于状态具有组合性 , 通常用 控制系统中 , 完备性和一致性 具有特定的内涵 , 完备 “配臵”的概念来描述系统状态 。比如 P IC TU R E , 性是指 : 对每一可能的输入事件序列 , 模型都必须作 IMA GE ,ON , SOU ND , WO R KIN G , TV , S TAND2 出响 应 ; 一 致 性 是 指 : 模 型 中 没 有 冲 突和非确定4 B Y , WA I T IN G , TV 和 D ISCON N EC T ED , WA I T2 性 。IN G

13、 , TV 均是系统配臵 。 定义 1 U ML 状态图模型是完备的 , 当且仅当() 3 状态迁移 。状态迁移是三元组 , 其中 so urce 和 target 分别是迁移的源 () 1 对任一可能 输入事件 , 每一个状态都必须 状 态 配 臵 和 目 的 状 态 配 臵 。 lable 的 形 式 为 Ev 有一个迁移 ;Co nd / Act , 其中 Ev 表示触发事件 ,Co nd 是迁移条 () 2 从任一状态发 出的 、由同一事件所触发的 件 ,Act 是后效 , 这三个参数都是可选参数 。比如 在 ( 所有迁 移 的 迁 移 条 件 的 析 取 形 成 重 言 式 Taut

14、olo2 图 1 中 , 所有迁移只有 Ev 参数 。状态迁移表示 : 当 ) gy;系统处于状态 so urce 时 , 如果事件 Ev 发生 , 而且布 () 3 任一状态都必须 对超时事件作出响应 。 条尔条件 Co nd 满足 , 那么系统退出 so urce 状态 , 执行()() 件1和2说明当一个事件发生时,至少有 动作Act后,进入到 target状态。一个迁移是就绪的。这三个条件保证了控制系统能()4初始状态。初始状态在状态图中用黑点表够对所有可能的输入作出实时 响应。示。比如当系统处于配臵 S TANDB Y , WA I T IN G , 定义2 U ML 状态图模型是一

15、致的，当且仅当模型的迁移之间没有冲突和非确定性。TV时，事件o n发生，那么系统退出 WA I T IN G 状out in :tnltst ;TKX I(MUTL J由于U ML状态图具有层次化特征，这给完备性和一致性检验带来了困难。比如，对如下U ML ()状态图模型 参见图2,设外部事件的集合为 e, 1e, e,简单状态A、B分别对事件e和e作出响2 3 1 2应。由于迁移e作用在组合状态S上,因而e也3 3隐式的作用在状态A、B上。由此可见，在分析完备性和一致性时，不仅要考虑直接作用在状态上的迁移，还要考虑从组合状态上“继承”而来的迁移，这就给分析完备性和一致性带来了困难。图3电视机

16、控制状态的HA模型乂PO W ER ,WO R KIN G状态被细化为两个并发的顺序自动机IMA GE和SOU ND。状态图模型的根状态细化为根顺序自动机，如TV。带有双边框的状态是初始状态,如IN I T - TV 、P IC TU R E 等。U ML状态图模型中的层间迁移被提到退出和进入的最外层状态之间，比如图1中的off 、o n和o ut ,分别被提 图2 U ML状态 图模型到TV自动机的WO R KIN G和WA I T IN G 间的迁移I 、丨和I ,这样就消除了层间迁移，只有单源/ 1 3 2 扩展的层次自动 机4单目标迁移。一般的，顺序自动机和层次自动机可 现有的对一致性

17、 和完备性进行检验的方以作如下定义：4 - 5 法是直接对U ML状态 图模型进行静态分析，(定义3顺序自动机A是一个四元组，？ 这就要考虑 由于U ML状态图的层次和并发组合状 S ) s, L , 其中 是A的状态集合，s 是A的初始0 0 ?态而引起的诸多复杂性，如组合状态上迁移的继承、S状 态，L 是A的迁移标号的集合，A X L X ?冲突迁移的解消、层间迁移和多 源/多目标迁移等。是迁移关系。因此检验完备性和一致性的思路为不是直接 对状态 顺序自动机可以并行或层次的组合成层次自动图模型进行分析，而是把它变换成一种等价的、结构 机。假定参与层次自动机的顺序自动机具有互斥的更清晰的中间

18、表示形式扩展层次自动机EHA ,() 状态集合。引入“组合函数”或细化函数的概念来 然后对EHA分析完备性和一致性。EHA中间格式 表示 顺序自动机的层次或并发组合 。只允许单个状态间的迁移，消除了状态图中由于 层 定义 4 设 F = A , A 为顺序自动机的 1 n 间迁移 、多源 / 多目标迁移 而引起的复杂性 , 简化了有限集合 , 记 A ? F 的状态集合为 。当如下条 ?A 冲突迁移的优先级判别 。另外 , EHA 中间格式具有丫件满足时,称？?？ P F为F上的组合函A ?F显式的树状结构,使得可 以设计简捷有效的算法对？A完备性和一致性进行检验 。本节给出扩展层次自动 数

19、, 其中 P 为幂集算 子 :存 在 惟 一 的 根 自 动 机 : ? ! A ? F. A | ? 机 EHA 的概念 。(丫)y ran ., 表示为4.1 层次自动机root每个非根的自动机只能有一个父状态 :( ) 层次自动机 HA 是顺序自动机的并行和层次Y . A n A ? F .? ! s ? root A?F A 组合。HA 类似于 UML 状 态 图 , 但 是 没 有 层 间 迁 ?A( ) y ?s 移 。可以把图 1 的状态图模型变换成如图 3 所示的组合函数无环 : 层次自动机模型 。?n sa ?. ? s ? s . s 这里，虚线框表示顺序自动机，从一个状态

20、指向( ) y A ?sA ?F ? ?A A 顺序自动机的虚线箭头表示把该状态细化为一个或 = ?。 多个顺序自动机 。如 果 细 化 自 动 机 的 个 数 多 于 一 y ( ) 如果 |s| = 1 , 那么 s 被细化为一个自动机 ; 个 , 表示这些顺序 自 动 机 之 间 是 并 发 的 或 并 行 的 。 y ( ) 如果 | s| 1 , 那么 s 被细化为自动机的并 行组( ) y 合 ; 如果 s= ?, 称 s 为基本状态或简单状态 , 记 比 如 , 这 里 WA I T IN G 状 态 被 细 化 为 顺 序 自 动 机( ) ( ) t d l = P IC T

21、U R E ,ON 。为 B asics 。比如 , 图 3 的组合函数为：丫 3丫 = T V ,由此可见，扩展层次自动机仅仅是对层次自动root丫机的迁移标号作了扩展,其他元素没有任何改变。= O F F ? PO WER ,WO R KIN G ? IMA GE ,( SOU ND ? s ? ?| s ? P ICTU R E , T EX T , 5 检验算法 ON ,MU T E ,S TANDB Y ,D ISCON N EC T ED 从第4节中可以看出，EHA中间格式只允许单(丫)定义5层次自动机HA 是三元组 F , E , 消除了状态图中由于层间迁移 、多个状态间的迁移

22、其中 F = A , A 是具有互斥状态空间的顺序 1 n丫源/多目标迁移而引起的复杂性，简化了冲突迁移的 自动机的集合，E是 事件的集合 , 是 F 上的组合函优先级判别 。另外 , EHA 中间格式具有显式层次结 数 。 类似于状态图中的迁移 , 可以定义自动机迁移 构 , 这些优点可以设计简捷有 效的算法对完备性和)(S 致性进行检验。本节给出在EHA中间格式上对 的投 影 函数。如 果 l ? L , s , l , s ?A ,则( ) ( ( 完备性和一致性进行检验的算法 , 该算法是在 EHA ) so urce s ,l , s = s , target s , l , s =

23、 s , label s , l ,) 树上的深度优先递归算法 , 如下 ： s = 1 , 迁移 l 的属性函数分别为 ：t rigger 、 guard 和算法 1 co mpleteness detectio neffect。 为了定义层次状态机中一个状态的所有直输入：顺序自动机 A ?F i 接子)(co mpleteness detectio n A ix 状态,引入如下“后继函数” :bool tautology = false 1定义6 丫 设是F = A , A 上的组合函2 fo reach s ? 1 n Ai )( 3 if ins s= ? ( ) x 数 , 则后继函

24、数 ? P ? 定 A ?F A ?F ?A A 4 Repo rt inco mpleteness erro r 义为 5 if s is leaf6 ( ) ) )( ( t rans s?= t rans s?o ut s sx ( ) ( ) Ay s= s |? A ?F. A ?ss ? ?A ( ) ) ) ( ( 7 event s s?= t riggers t rans s( ) x 因此 , s ?s 当且仅当 s 是 s 的直接子自动 )( 8 tautology?= ? guard t )t ?trans ( s 9 ( ) if event s s?E机的一个状态

25、。10 Repo rt inco mpleteness erro r 4 . 2扩展的层次自动机 11 iftautology ?True 在状态图模型中 , 层间迁移明确指出了迁移的 12 Repo rt inco mpleteness erro r13 else 源状态和目标状态 , 但是在层次自动机中当把状态14 ( ) x fo reach s ?s 图模型中的层间迁移提到高层次状态之间后 , 原来15 ) ) ) ( ( ( t rans s ?= t rans s ?t rans s迁移的源状态和目的状态的信息就有可能丢失 。比 16 ) ( fo reach t ?o ut s

26、s17 ( ) if sr t = ?如 , 图 1 中的层间迁移 o ut 是从 WO R KIN G 状态到18 ( ) x fo reach s ?sD ISCON N EC T ED 子状态 , 但是在图 3 中 , 它被提到 19 ) ( ( ) trans s ?= trans s ? t 状态 WO R KIN G 和 WA I T ING之间,因此丢失了 o ut 20 else21 ( ( ) ) ( ( ) )迁移的目标子状态信息 ; 再如图 1 中的迁移 o n 是由t rans sr t ?= t rans sr t ? t 子状态到 WO R22 ) ) ) ( (

27、( t rans s?= t rans s?o ut s sS TANDB YKIN G的层间迁移，当它23 ( ) Yfo reach A ?s 被提到层次自动机的迁移I 之后 , 丢失了 o n 迁移的 3 )( 24 co mplete detectio n A具体 源 子 状 态 , 也 就 是 不 知 道 I 到 底 是 从 3 设计完备性和一致 性检验算法的难点在于迁移WA I T IN G 状态的哪个子状态迁出的 。 的继承以及冲突的判别和解消 。 把显式指向状态 s 因此 , 在层次自动机中把层间迁移提出后 , 必须 ( ) 的迁移 集合表示为 ins s, 从状态 s 发出的

28、迁移记保留原来迁移的源和目标状态的子状态 。为此 , 在层 ( ) ( ) 为 t ranss。 trans s 可分为两类：一类是在状态图次自动机的迁移标号中增加两个新属性：sr和 t d分中显式的从状态 s 上 发 出 的 迁 移 集 合 , 记 为1别表示迁移的源状态和目标状态集合。比如, 对图 3( ) o ut s s,另一类是直接或间接从父状态继承下来的中的三个迁移 , 迁移 。定 义 如 下符 号 ：设 T为迁移的集 合 , 则( )( )?, t d I S TANDB Y = = sr I 1 1 ( ) t riggers T表示集合 T 中所有迁移的触发事件构 ( )sr

29、 I ( )= ?, t d I = D ISCON N EC T ED 2 2成的集合 , 即( )= S TANDB Y , sr I ( ) ( ) t riggers T = e |? t ? T . e = trigger t 3( ) event s s 表示从 s 发出的所有迁移的触发事件算法 , 可以求出从每个 状态 co mpIeteness detectio n的集合 , 即上迁出的迁移集合 , 如图 5 中标记在状态旁边的集( ) ( ( ) )event s s= t riggers t rans s合 t rans 所示 。设U ML状态图模型的EHA中间表示为EHA

30、(丫)= F , E , 其中 F = A , A , A为顺序自 1 n i丫动机，E为事件的集合，为组合函数。对完备性进行检验的算法为 co mpleteness detectio n ,它的输入是任意层次的顺序自动机 A。该算法遍历A中的i i()()每个状态s , 构造相应的集合trans s 和eve nt s s,然后根据深度优先原则，递归地处理s的下一层次(丫 ()的自动机S。如果状态s是叶子节点 即简单状)态，则根据完备性定义判断其完备性。()算法的最外层循环 第2行，第22行遍历输 图4 U ML状态图模型 入自动机A的每一个状态；对每个状态 s ,检验指向i()该状态的迁移

31、的集合ins s, 如果集合为空，说明没有迁移指向该状态 , 则违反完备性定义 ; 如果状态 s( ) 为叶节点 第 5 行 , 即 s 为简单状态 , 首先计算定义( ) ( ) 在该状态上的所有迁移 , 即 t rans s?o ut s s, 其( ) ( ) 中 t rans s 是从父状态继承下来的迁移 ,o ut s s 是( ) 显式从 s 迁出的迁移 第 6 行 ; 然后计算相应的触( ) (发事件集 合 event s s和 tautology 第 7 行 , 第 8) ( )行 , 如果 event s s? E , 说明状态 s 对某些事件不( 能作 出 响 应 , 违

32、反 了 完 备 性 定 义 第 9 行 , 第 10) 行。如果 tautology ? True , 说明所有从 s 迁出的迁 移的迁移条件不能形成重言式 , 违反了完备性定义( ) 第 11 行 , 第 12 行; 如果状态 s 不是叶节点 , 即 s 图 5 EHA 模型 为组 合 状 态 , 则 首 先 把 它 从 父 状 态 继 承 来 的 迁 移 类似 的 , 设 计 算 法 co nsistency detectio n 以 检()( x ) t rans s向下传播到每个直接子状态s ?s上 验一致性,如下：() x第14、15行，其中为后继函数见定义6;对于算法2 co ns

33、istency detectio n( ) 每个从状态 s 迁出的迁移 t ?o ut s s, 区分两种情 输入 ： 顺序自动 机 A ?F i)( co nsistencydetectio n A ( ) i形 ： 如果 sr t = ?, 说明 t 是显式定义在组合状态1 s ?fo reach Ai ( )x 上的迁移 , 那么 t 要向 s 的直接子状态 s 上传播 if s is not leaf 2 ( ) ( )第 16 , 第 19 行, 否则 t 只向 sr t 所限定的集合() 丫 3 fo reach s ?s()传播 第20行,第21行；处理完迁移的传播后,得)()(

34、4t rans s : = t rans s ?t rans s5 ( ) fo reach t ?o ut s s()到定义在s上的所有迁移集合 第22行。对于组合)(6 if sr t = ?状态s ,按照深度优先策略,递归的向下遍历状态 s 7 ( ) x fo reach s ?s( ) ( )丫的子自动机 A ?s 第 23 行，第 24行。8 ) ( ) ( t rans s ?= t rans s ? t 9 else便于理解起见,通过如下实例来说明算法10 ()()(t rans sr t ?= t rans sr t ? t co mplete ness detectio n

35、中给出的迁移向下传播过 11 ) ) ) ( ( ( t rans s?= t rans s?o ut s s程。12 ) ( fo reach t , t ?t rans s()()13 if t rigger t = t rigger t图4中t 为从状态1迁出的迁移,它要传播到12 14 ( ) A) ( if guard t guard t = True的任意层次的子状态上；而t 是层间迁移,从状态1 15 Repo rt inco nsistency erro r 1 .2.1 . 1 上迁出；迁移t也要传播到1 . 2.1 的任意5 丫 ( ) 16 if s?17 ( ) 丫 f

36、o reach A ?s 子状 态上。图4的EHA模 型如图5所)(18 co n siste ncy detectio n A第1行，第10行是组合状态上迁移的传播；第11行计算状态s上所有迁移的集合；第12行，第15行检验一致性是否满足，即判断触发事件相同的迁移的迁移条件是否同时为真 ; 对于组合状态 , 按照 深度优先的策略 , 递 归的向下遍历子自动机A ?图6原型的处理过程 丫 ( ) s 。值得注意的是 , 对完备性和一致性进行检查实 和一致性进行检验的方法 , 设 计了完备性和一致性 际上是很困难的 , 因为在迁移条件和后效中可能会 的两个 算法 。该算法充分利用了 EHA 的显

37、式树状 引用变量 、函数 、事件参数 、正交 状态等 。因此 , 在最 结构 , 使用深度优先的递归遍历策略对简单状态的 坏情况 下 , 需要可达性分析和对迁移后效的程序代 完备性和一致性进行检查 , 并把组合 状态上的迁移 码的解释 。对迁移条件的静态分析只有在迁移条件 向子状态传播 解决了完备性和一致性分析的难点( 约束成特殊的规范形式 如文献 4 中的 AND/ O R 和关键点 。) table 的形式的情况下才可进行检查 。文中提出的 检验算法只是给出了一个框架 , 不考虑如何通过算 参考文献 : 法来判定逻辑公式 , 因为这超出了文中的范围 。因此 1 HAR EL D.Statechar