SysML 状态图合理性验证研究与实现

俞晓锋，王立松

(南京航空航天大学 计算机科学与技术学院，江苏 南京 210016)

SysML(Systems Modeling Language)［1］是UML 在系统工程应用领域的延续和拓展。与其他建模语言一样，SysML 是一种通用标准建模语言。

随着应用系统越发复杂，系统的任意环节均可能会影响到系统的整体运行。例如民航业务系统，作为一个巨大的系统，不能保证其对象在整个生命期内均能安全稳健运行，而一旦出现异常状况会造成巨大的经济损失。用SysML 建模可抽象表示应用系统的对象，本文研究的对象是类模型中某个主动类的实例，通过验证行为模型来模拟出对象在生命期内的运行过程，用这种方式来演练其实现的每一个用例场景。SysML 状态图用于建立类对象在其生命期内的行为模型，尤其是当对象具有依赖于状态的行为。

SysML 和UML 一样，为保持描述的清晰易懂，在给出自身语义说明的同时，采用半形式化的描述方法，使用自然语言表示约束和语义，力求实现形式化与易于理解之间的平衡。因此，SysML 本身缺乏分析和验证的手段，针对这一问题，本文对SysML 状态图进行拓展，使用SCXML(State Chart XML)［2］作为SysML 状态图的形式化描述语言并引用动作规约语言［3］(Action Specification Language，ASL)描述状态图对象的行为动作。其中ASL 是WilKie 等人在2002 年提出的平台无关动作描述语言，其提供了操作平台无关模型元素的方法。通过使用SCXML 和ASL 可建立精确无歧义的行为模型，并在此基础上进行分析验证。

SysML 状态图的体系结构验证无需考虑业务需求的偏好，使用Kripke 结构可表示对象的状态空间。由于SCXML 可表示SysML 状态图体系结构的所有信息，根据Kripke 结构可方便构造出SysML 状态图的对象状态迁移图，通过对象状态迁移图给出性能需求的形式化表示和验证算法［4］。在业务需求验证方面，主要考察对象在生命期内的行为过程是否与用例时序图一致，本文采用事件信号驱动机制来捕获对象的行为轨迹。

1 SysML 状态图体系结构验证

1.1 SysML 状态图语义

为便于描述，本文在遵从对象管理组织SysML 规范［5］的前提下重新定义了一些状态图语义的形式化表示方式，包括顺序自动机、层次自动机、单元以及层次自动机的操作语义。

验证SysML 状态图的体系结构，首先将状态图转化为层次自动机(HA)，其由顺序自动机(SA)组成。

定义2 HA=(F，E)，F 是有穷顺序自动机集合;∀SA1，SA2∈F，ΨSA1∩ΨSA2=Φ，E 是有穷事件集合。

HA 中的全局状态由单元表示，一个单元既可以代表一个基本状态又可代表一个复合状态，每个复合状态由某个简单顺序自动机的基本状态组成。

在SysML 状态图中，每个状态由单元和当前环境组成，环境包括事件环境和变量环境，对于事件环境E，ΘE 表示事件队列的所有可能情况，对于变量环境V;ΘV 表示变量所有可能取值。下面用标记转换系统(LTS)对HA 定义操作语义。

定义4 HA 的操作语义是一个LTS OP=(S，S0，→)，其中S=CellHA×ΘE×ΘV 是状态集合，S0是初始状态集合，→=S×S 是状态迁移集合。

1.2 通过SCXML 构造对象状态迁移图

Kripke 结构是一个4 元组，K=(CellHA，→，L，Cell0)，其中，是初始单元的合集;(Cell1，Cell2)∈→表示存在从Cell1到Cell2的迁移，假设→中的迁移互不相同;L∶CellHA→2AP为每个单元标注一组原子命题。

本文采用邻接表来实现Kripke 结构，实例如图1所示。

图中Vs1，Vs2，Vs3，Vs4∈CellHA，所有邻接于Vsi的顶点Sj链成一条单链表，其中Vsi，Sj∈CellHA，∃i ∈{1，…，num}，此例中num 取4。

根据定义4，给出s∈S 的SCXML 表示，其中e1，…，en∈E，a1…，am∈V)。

图1 用邻接表表示Kripke 结构的实例

从SCXML 可知SysML 状态图的操作语义，结合Kripke 结构，便能构造出对象状态迁移图G。G 是具有SysML 状态图操作语义的Kripke 结构的抽象表示［10－11］。

生成对象状态迁移图G 的步骤如下:(1)初始化邻接表。(2)从SCXML 中读取Vsi∈CellHA和变量V 存放到邻接表的顶点域里。(3)从SCXML 中读取Vsi的迁移目标状态存放到邻接于Vsi的单链表里。(4)从SCXML 中读取Vsi的事件E 存放到与Sji对应的链接域里。(5)重复步骤(1)～步骤(3)直到读取完SCXML 中所有的Vsi。(6)对象状态迁移图G 生成完成，算法结束。

1.3 性能需求验证的标准

SysML 状态图是否满足性能需求指主动类对象能否安全地运行完整个生命期［6－9］，即保证对象能够安全地创建、销毁并且在生命期内不存在死锁。根据这个要求，本文定义了G 的3 大安全性条件并给出了相关的推论和证明。

推论1 满足条件1 和条件2 的状态图是符合状态可达的，即状态图中任意一个状态都是可达的。

条件3 tsi=(s1，s2，…，sj)∈{ts1，…，tsn}是对象的其中一条并发迁移序列，则ts1∩…∩tsi∩…∩tsn∉{o}，其中o 为终止状态。该条件表明对象收到销毁信号时，不可能存在该对象产生的某个或多个子对象还未销毁的情况，否则子对象会一直存在于系统中占用资源。保证了对象被安全销毁。

在验证性能需求时，使用G 的安全性作为正确性标准。

1.4 性能需求的验证算法

本文定义了两种异常状态，分别取名为“奇迹”状态和“黑洞”状态。

定义5 “奇迹”状态是一种只有迁移出，没有迁移入的非初始状态。对象处于这种状态时说明它没有被正确创建。

定义6 “黑洞”状态是一种只有迁移入，没有迁移出的非终止状态。对象处于这种状态说明它已经陷入死锁。

由推论1 可知，SysML 状态图不能存在“奇迹”和“黑洞”状态，验证算法:(1)遍历G 的顶点域Vsi，判断该顶点域的单链表是否为空，如果为空并且该顶点域中的状态不是终止状态，则存在“黑洞”状态，标记异常，否则符合安全性的条件1。(2)遍历G 的顶点域Vsi，如果该顶点域的单链表非空，则遍历该单链表，并给单链表中的每个Sji标记上后继标志。(3)在步骤(2)的基础上重新遍历顶点域Vsi，判断顶点域中的状态是否有后继标志，如果没有并且该状态不是初始状态，则存在“奇迹”状态，标记异常，否则符合安全性的条件2。(4)如果终止状态的前继状态只有1 个，则符合安全性的条件3，直接跳到步骤(8)，否则进行步骤(5)～步骤(7)。(5)遍历G 的顶点域Vsi，判断顶点域中的状态类型，如果为FORK 伪状态，则给该单链表中的每个Sji标记上活动标志，如果为JOIN 伪状态，则清除顶点域中状态的活动标记。(6)如果顶点域Vsi中的状态具有活动标志，则给该单链表中的每个Sji标记上活动标志。(7)在步骤(5)和步骤(6)的基础上重新遍历G的顶点域Vsi，判断顶点域中的状态类型，如果为终止状态并且具有活动标记，说明不符合安全性的条件3，标记异常，否则符合安全性的条件3。(8)如果条件1 ～条件3 都满足，则该SysML 状态图的性能需求是合理的。

2 SysML 状态图业务需求验证

2.1 业务需求验证标准

一个用例从黑盒的、外部的角度描述了系统对象的一次生命过程。用它可推断对象对请求或激励做出何种响应。全体用例和它们的相关场景，可以完全刻画对象所需的功能性行为，使得绝大多数业务需求得以体现。用例时序图是用户希望系统所能产生的行为交互过程，它在建模过程中被用来当成系统的标准黑箱视图。一个用例场景对应一个用例时序图。本文采用Moore 状态机原型，在状态图模型描述某个主动类对象的行为过程中，当对象接收到外部激励信号时所表现的行为由对象所在状态的入口动作决定，它由ASL 进行描述，此时对象可能会在自导信号的作用下转移到新的状态也有可能停留在原状态等待新的外部激励，对象在这两种情况下产生收发信号事件的序列。通过判断信号事件序列是否符合预期定义的事件序列来验证状态图的业务需求。

2.2 业务需求验证设计方法

每个对象维持一个信号事件队列，根据这个特点设计信号事件驱动机制来执行状态图，设计的信号事件驱动结构如图2 所示。

图2 信号事件驱动框架

事件消费类中的事件处理函数为状态的入口动作，事件类中产生的信号包括外部信号事件和自导信号，状态解析引擎将状态图转换为由SCXML 和ASL表示的精确描述的PIM 代码。如果状态验证没有完成，整个驱动引擎将一直处于循环状态，将驱动引擎生命期内对象所产生的信号事件序列与预期的用例时序图作对比，就可以判断出状态图是否满足业务需求。

对象在执行过程中所产生的Event 序列，如果与预期定义的用例时序图中的事件交互顺序不一致，则表明对象业务需求未得到满足。

3 实验验证

文中验证了一个列车管理域模型，该域的类模型如图3 所示。

图3 列车管理的类图

由类图可知，一个列车运行的一个路段(Hop)包括多个加速曲线(AccelerationCurve)。

对AccelerationCurve 的对象建立如图4 所示的状态图。

图4 AccelerationCurve 对象的状态图

分别为MaintainingAccelerationCurve 状态和A ccelerationCurveComplete 状态添加用入口动作，下面给出用ASL 描述的MaintainingAccelerationCurve 状态的入口动作，整个入口动作用于判断AccelerationCurve对象是否到达了加速曲线终点。

AccelerationCurveComplete 状态中的入口动作描述了列车如何从一个加速曲线过度到另个一个加速曲线。

运行信号事件驱动框架，在状态解析部分验证了状态图的体系结构，SCXML 表示的体系结构满足条件1 ～条件3，AccelerationCurve 对象的性能需求合理。

用ASL 来表示外部激励信号，该信号模拟了Hop对象对AccelerationCurve 对象的激励。

在输入事件触发按钮响应的对话框中输入用ASL描述的测试例程:generate performCurve()to theAccelerationCurve。如图5 所示。

图5 状态图业务需求验证

点击确定后得到对象在生命期内的行为过程，执行结果如图6 所示。

图6 AccelerationCurve 对象的执行结果

从执行信息里可了解到该对象在其生命期内的信号事件序列，它表示对象在经过速度调节之后到达了路段的终点，并向Hop 对象发送了完成信号。将其与预期的用例时序图做比较，就可以判断出状态图是否表现出了应有的业务需求。

4 结束语

本文给出了一种验证SysML 状态图合理性的实现方案。用SCXML 和ASL 精确无歧义描述SysML 状态图，通过信号事件驱动机制完成体系结构和业务需求的验证。

将SysML 状态图作为行为模型并不完全［7－9］，而且在体系结构验证部分没有考虑并发工作流和时序逻辑［10］方面的内容。本文以后的一个研究方向是:对SysML 状态图进行时间拓展，给出拓展后的SysML 状态图到时间自动机的过程，使用时间计算树逻辑［11］表示时序约束，并验证时序约束的一致性。

［1］ 蒋彩云，王维平，李群.SysML:一种新的系统建模语言［J］.系统仿真学报，2006，18(6):1483－1487，1492.

［2］ JIM B G.State chart XML(SCXML):state machine notation for control abstraction［S］.USA:Voice Browser，2013.

［3］ CHRIS R，PAUL F.Model driven architecture with executable UML［M］.北京:机械工业出版社，2006.

［4］ 陆公正.基于UML 状态图的工作流建模与验证［D］.苏州:苏州大学，2006.

［5］ VERBEEK H M W.Diagnosing workflow process using woflan［J］.Computer Journal，2001，44(4):246－279.

［6］ KWON G.Rewrite rules and operational semantics for model checking UML statecharts［C］.Berlin:Lecture Notes In Computer Science，Springer，2000.

［7］ GNESI S，MAZZANTI F.A model checking verification environment for UML statecharts［C］.Udine:XLIII Annual Italian Conference AICA，IEEE Computer Society，2005.

［8］ ESHUIS R.Symbolic model checking of UML activity diagrams［J］.ACM Transactions on Software Engineering and Methodology，2006(15):1－38.

［9］ 李广元，唐稚松.基于线性时序逻辑的实时系统模型检查［J］.软件学报，2002，13(2):193－202.

［10］ALUR R，HENZINGER T A.Logics and models of real time:a survey［M］.Berlin:Springer－Verlag，1992.

［11］杜杰，江国华.基于模型检测的UML 状态图和顺序图一致性检测［J］.电子科技，2012，25(2):100－104.