一种从UML活动图到Event-B模型的转换方法

摘要

本发明是一种从UML活动图到Event‑B模型的转换方法，属于计算机软件工程领域。确定UML活动图的模型元素：发起活动的对象、基本活动和活动流；建立对象集合和活动集合，建立不变式以保证每个活动只属于一个对象，将活动的前置条件和后置条件在event的触发条件guards和动作actions中分别声明，对活动流进行映射，包括顺序流、分叉与汇合、分支与合并三种活动流。本发明方法将UML活动图转换为Event‑B模型，通过Event‑B的建模平台对转换后的模型进行形式化验证，可发现UML模型中存在的问题，同时针对作为形式化语言Event‑B不便于建模的问题，实现了利用UML活动图辅助其建模的方法。

说明书

技术领域

本发明涉及计算机软件工程领域，涉及将UML模型转换为形式化模型的技术，具体 涉及一种从UML活动图到Event-B模型的转换方法。

背景技术

UML即统一建模语言，是一个支持模型化和软件系统开发的图形化语言，UML模型 实际已经成为建模领域的标准，具有更强的通性和更广泛的工具支持。但UML是一种半形式 化语言，没有精确的语意，不同的人理解UML模型容易引起歧义。另外，无法对UML模型进行 形式化验证，从而保证模型的正确性。

为了解决这些问题，目前已有很多工作研究如何将UML模型转换为形式化模型。在 参考文献[1]中，研究人员选用高阶逻辑形式化规范语言PVS对UML的状态图进行了形式化 工作。PVS具有很强描述能力，并且有相应的模型验证工具支持，克服了UML模型缺乏形式化 描述和模型验证工具的不足。参考文献[2]提出了一种由UML的状态图自动转化成Petri网 的模型转化技术，以支持进行安全性的分析和验证。在参考文献[3]中，研究小组则系统地 研究了利用UML转换到Z语言的方法。利用UML建模，构建了系统的类图和状态图，同时，该研 究小组开发了相应的支持工具，支持将系统状态表转换成Z语言，以支持后续的形式化分 析。此外，参考文献[4]研究了将UML模型中的类图和活动图转化到动态故障树(Dynamic FaultTrees，DFT)的方法。文中利用UML的类图对系统进行了建模，然后利用设计开发的剖 析器和合成算法完成了对UML扩展模型的转换。参考文献[5]中对UML视图向B语言进行转换 的机制进行了系统的研究，总结了目前已有的UML中如类图，状态图，顺序图等到B语言的转 换方法，并在此基础上进行了提出了改进思路。最后以某一免疫系统(ImmuneSystem)为实 例，进行了类图和状态图的UML建模，并向B语言进行模型转换，采用模型仿真工具对生成的 B语言模型进行了仿真。

参考文献[1]～[5]如下：

[1].赖明志,尤晋元.从UML状态图到PVS规范的自动转换,验证[J].电子学报, 2002,30(12A):2122-2125.

[2].HeiX,ChangL,MaW,etal.AutomatictransformationfromUML statecharttoPetrinetsforsafetyanalysisandverification[C]//Quality, Reliability,Risk,Maintenance,andSafetyEngineering(ICQR2MSE),2011 InternationalConferenceon.IEEE,2011:948-951.

[3].HawkinsR,ToynI,BateI.Anapproachtodesigningsafetycritical systemsusingtheunifiedmodellinglanguage[J].TUM,2003:3.

[4].PaiGJ,DuganJB.Automaticsynthesisofdynamicfaulttreesfrom UMLsystemmodels[C]//SoftwareReliabilityEngineering,2002.ISSRE 2003.Proceedings.13^thInternationalSymposiumon.IEEE,2002:243-254.

[5].孟静，邹盛荣.基于统一过程的UML_B系统转换技术的研究[D].扬州大学, 2008.

尽管国内外学者针对UML到形式化模型转换方法上进行了大量的研究，但仍存在 一些问题：

1)目前常见的各种模型转化方法虽然都具备各自的优点，但也存在着明显的不 足，比如B语言和Z语言的语义较为复杂，难以理解；Z语言缺乏相应的模型分析工具支持； Petri在面对复杂模型时会出现状态空间爆炸问题等；

2)目前开展的许多研究只针对UML视图中的一种图或两种图提供了相应的模型转 化方法和安全性分析方法，缺乏对UML视图更加系统全面的研究。

Event-B是一种支持系统级建模和分析的形式化方法。系统级的建模即指Event-B 能够完成同时包含系统软件、硬件和外部交互的建模，而形式化的特点意味着Event-B拥有 严格的数学逻辑基础和精确的语义，是一种无歧义的语言。Event-B由传统的B语言发展而 来，因此与B语言拥有共同的语法基础—一阶谓词逻辑和集合论。而相比于B语言用一个个 抽象机来描述系统，Event-B在建模过程中引入了“事件”的概念，用来更加清晰的描述系统 和外部的交互过程，并克服了B语言在处理并发行为时的不足。Event-B目前的建模环境是 基于Eclipse集成开发环境开发的Rodin建模平台，同时，在该平台下集成了多种模型检测 和验证工具，如ProB[7]工具提供了对Event-B模型进行检验的功能，可以检验模型中是否 存在死锁等性质；AnimB[7]工具提供了动态演示功能，可以对Event-B模型进行动态演示， 观察模型中各个事件发生的顺序，直观的了解建模系统的行为。

Event-B模型中包括两个基本的组成部分，分别是Context和Machine。Context用 于表征模型的静态属性，包括在模型中定义的集合、定理、公理和常量等。其中，在集合里可 以进行新的数据类型的声明，并设定唯一的标识符。相对的，Machine则用于表征系统的动 态行为，包括变量、不变式和事件。变量用于描述在系统运行过程可以发生改变的属性，而 不变式则是对变量的行为进行声明和约束。在模型中，一般用v来表示变量的集合，用I(v) 形式化表示不变式的集合，用E表示事件。在Machine中，变量的值会随着事件的发生而发生 变化，但是变量始终要满足相应不变式的约束。一个事件是由触发条件(Guards)和动作 (Actions)组成，触发条件表示事件发生的必要条件，动作描述当事件发生时，变量集合发 生的变化。Context和Machine之间存在着调用与被调用的关系，Machine中的事件和变量会 调用相应Context中的静态量，如集合，常量等。

发明内容

本发明的目的是提供一种将UML活动图转换为Event-B模型的方法，从而通过 Event-B的建模平台Rodin对转换后的模型进行形式化验证，发现UML模型中存在的问题。

本发明提供的从UML活动图到Event-B模型的转换方法，实现步骤包括：

步骤1，确定UML活动图的模型元素，包括发起活动的对象、基本活动和活动流。

步骤2，在Event-B模型中对UML活动图中参与活动的对象进行声明。

对UML活动图中参与活动的所有对象建立对象集合OBJ_SETS，对象集合中元素为 对象名称，将对象名称作为常量进行声明。

步骤3，在Event-B模型中对UML活动图中的基本活动进行映射。

(3.1)对UML活动图中的所有活动名称，建立活动集合ACTIVITY_SETS，活动集合中 元素为活动名称，将活动名称作为常量进行声明；

(3.2)定义对象变量obj，表示当前活动所处的泳道，声明对象变量obj∈OBJ_ SETS；

(3.3)定义活动变量activity，表示当前进行的活动，声明活动变量activity∈ ACTIVITY_SETS；

(3.4)在Event-B模型的Machine里建立不变式，保证每个活动只属于一个相应的 对象；

(3.5)将UML活动图中的活动的前置条件在Event-B模型中的event的触发条件 guards中进行声明，将UML活动图中的后置条件在动作actions中进行声明。

步骤4，在Event-B模型中对UML活动图中的活动流进行映射；UML活动图中的活动 流包括有顺序流、分叉与汇合、分支与合并。

(4.1)顺序流的映射规则是：声明控制变量sequence，利用控制变量sequence驱动 活动按照顺序流顺序执行，具体是：当活动进入初始状态时，将sequence置为1；对于顺序执 行的第i个活动，在活动的触发条件中增加sequence的值为i的条件，i为正整数，当活动中 的动作执行完成后，追加sequence的值自增1的动作。

(4.2)分叉与汇合的映射规则是：声明用于描述并行动作的动作变量和对象变量， 声明两个控制变量sequence和sequence_2。

使用控制变量sequence和sequence_2在Event-B模型实现并发的逻辑为：

a.当活动流将要进入分叉时，在将要进入分叉的上一个活动中追加动作，将 sequence_2置为1；

b.对于分叉中的一支，继续用sequence作为触发条件，控制活动的顺序执行；对于 分叉中的另一支，用sequence_2作为触发条件，控制活动的顺序执行；

c.在活动流即将汇合时，在汇合后的下一个活动中用两个控制变量sequence和 sequence_2同时作为触发条件，表示进入该活动的条件是分叉中的并发事件都已执行完 毕。

(4.3)分支与合并，分为下面两种情况：

(4.3.1)当活动执行完毕后，将进入一个分支判断，根据判断结果的不同，进入不 同的活动；该情况的映射规则为：声明判定条件变量decision∈BOOL，当判定条件为真时， decision＝True，当判定条件为假时，decision＝False；将判定条件对应的decision的取 值加入对应要进入的活动的触发条件中；

(4.3.2)当活动1执行完毕后，将进入一个分支判断，如果判断条件为真，继续执行 活动2，如果判断条件为假，则返回活动1重新执行，直到判断条件为真后才离开活动1；该情 况的映射规则为：按照(4.3.1)中声明判定条件变量decision，当判定条件为真时， decision＝True，当判定条件为假时，decision＝False；增加辅助事件Loop_Branch，其中 的动作为将控制变量sequence的值减1，在事件的触发条件中加入decision＝False，通过 辅助事件Loop_Branch使活动流在判定条件为假时自动回到活动1中重新执行。

本发明的优点和积极效果在于：本发明提供的从UML活动图到Event-B模型的转换 方法，实现了将UML活动图转换到Event-B模型，从而可以利用Event-B模型对UML模型进行 形式化验证，发现UML模型中存在的问题。针对作为形式化语言的Event-B不便于建模的问 题，本发明实现了利用UML活动图辅助其建模的方法。

附图说明

图1是本发明的从UML活动图到Event-B模型的转换方法的整体流程示意图；

图2是典型的顺序流的示意图；

图3是典型的分叉与汇合活动流的示意图；

图4是第一种类型的分支与合并活动流的示意图；

图5是第二种类型的分支与合并活动流的示意图。

具体实施方式

下面将结合附图和实施例对本发明作进一步的详细说明。

活动图是UML建模语言中一种常用视图，用于对系统的动态行为进行建模。活动图 描述了系统中活动的顺序，展现了从一个活动到另一个活动的控制流。一个活动图中包含 的基本元素有：活动的对象，动作状态，活动的控制流。其中活动的对象表示活动的发起者， 即该活动是由系统中的哪个对象进行的。活动的对象明确地位于活动图中的“泳道”，并且 每个活动只能明确地属于某一条泳道。动作状态是指不可中断的瞬时动作。活动的控制流 是指动作状态的执行顺序。

本发明提供的从UML活动图到Event-B模型的转换方法，包括实现步骤1～步骤4。

步骤1，确定UML活动图的模型元素。

要将UML活动图转化为Event-B模型，首先需要分析UML活动图中具有的模型元素， 确定需要进行转化的元素。根据分析，活动图中基本的模型元素如表1所示。

表1UML活动图中基本的模型元素

而后，根据表中的模型元素，将其分别转换到Event-B模型中。其中，考虑到活动图 中的活动流(控制流)的形式很多，活动之间存在着顺序执行、并发执行、判断分支、循环等 各种基本活动流的组合，因此需要对每种基本活动流分别考虑映射规则。

步骤2，在Event-B模型中对UML活动图中参与活动的对象进行声明。

建立一个对象集合表示UML活动图中参与活动的所有对象，将对象名称作为常量 进行声明，并且将对象名称作为对象集合里的元素。Event-B的声明形式如下：

该例中，Obj1、Obj2、Obj3均为对象名称，放入集合OBJ_SETS中。

步骤3，在Event-B模型中对UML活动图中的基本活动进行映射。

将UML活动图中的基本活动映射到Event-B模型中包括步骤3.1～步骤3.5。

(3.1)对UML活动图中的所有活动名称，建立活动集合ACTIVITY_SETS，把图中所有 出现的活动名称作为常量进行声明，并且作为将活动名称作为集合里的元素。Event-B的声 明形式如下：

其中，Actvity1、Actvity2、Actvity3均为活动名称，放入集合ACTIVITY_SETS中。

(3.2)定义对象变量obj，表示当前活动所处的泳道(活动的执行对象)；同时，声明 对象变量obj∈OBJ_SETS，表示对象变量的值只能取自对象集合。

(3.3)定义活动变量activity，表示当前进行的活动；同时声明活动变量activity ∈ACTIVITY_SETS，表示活动变量的值只能取自活动集合。

(3.4)活动图中不允许活动跨泳道。为了对此进行约束，可以通过在Event-B的 Machine里建立不变式，保证每个活动只属于一个相应的对象。例如，假设活动图中活动1和 活动2是由对象1发起的，活动3和活动4是由对象2发起的，则相应的不变式如下：

inv1：

inv2：

(3.5)用Pre-condition表示此活动的前置条件，在相应事件的触发条件guards中 声明；用Post-condition表示此活动的后置条件，在事件的动作actions中声明。

综上，一个基本活动的Event-B模型如下：

上面示例中，act1、act2表示两个行为，obj表示对象变量，activity表示活动变 量。

步骤4，在Event-B模型中对UML活动图中的活动流进行映射。

由于UML活动图中活动流的形式很多，因此下面根据活动流的基本形式，分别说明 转换规则。

(4.1)顺序流。一个典型的顺序流如图2所示。

为了表达这种活动之间依次顺序发生的关系，本发明考虑添加一个辅助变量来控 制活动的发生顺序。该变量并不对应UML活动图中的任何图形元素，而是用来驱动活动按照 预定次序依次发生。定义该辅助变量为控制变量sequence，声明sequence∈N1，将其作为活 动发生的触发条件，同时约束活动发生的顺序。N1表示表示正整数集合。

控制变量sequence的赋值逻辑为：当活动进入初始状态时，将sequence变量置为 1；进入活动1的触发条件中追加一条：sequence＝1；当活动1执行完成后，在活动1的动作中 追加一条：sequence＝sequence+1，表示离开本活动准备进入下一活动；而活动2的触发条 件中追加一条sequence＝2，表示可以进入本活动，以此类推，驱动活动按照顺序流顺序发 生。按此逻辑，图2对应的Event-B模型表示如下：

该示例中，定义活动1—Actvity1和活动2—Actvity2中，前置条件中加入 sequence值，在动作中追加sequence的值自增1。

(4.2)分叉与汇合。分叉与汇合也是活动流的一种，它是UML活动图中用来表达并 发的方法。一个典型分叉与汇合如图3所示。

由于在此类活动流中会存在活动并发执行的情况，如果只使用原来的一个动作变 量activity已经无法表达并发执行的两个动作。因此，考虑追加新的动作变量activity_2， 新的对象变量obj_2，以及新的控制变量sequence_2，来描述正在进行的并发活动。同时用 不变式声明对象变量obj_2∈OBJ_SETS，action_2∈ACTIVITY_SETS，sequence_2∈N1，初始 化为1。

利用控制变量sequence和sequence_2在Event-B模型实现并发的基本逻辑为：

a.当活动流将要进入分叉(并发)时，在将要进入分叉的上一个活动中追加一个 Action，将sequence_2置为1；

b.对于分叉中的一支，继续用控制变量sequence作为触发条件，控制活动的顺序 执行；对于分叉中的另一支sequence_2作为触发条件进行控制；

c.在活动流即将汇合(离开并发)时，在汇合后的下一个活动中用两个控制变量 sequence和sequence_2同时作为触发条件，表示进入该活动的条件是分叉中的并发事件都 已执行完毕。

根据上述设计逻辑，图3所对应的Event-B模型为：

如上所示，示例中，存在控制变量sequence和sequence_2，活动2和活动3并发执 行，则在活动1中增加将sequence_2置为1的动作。在一个分支中，继续使用控制变量 sequence进行顺序控制。sequence和sequence_2控制活动顺序执行的赋值逻辑都是按照 (4.1)中的原则设置的。

(4.3)分支与合并。分支与合并即活动图中的判断流，根据具体情况的不同，分支 与合并又可以细分为三种类型。下面分别给出这三种类型的活动流和向Event-B模型转换 的规则。

(4.3.1)第一种类型的分支与合并活动流的基本结构如图4所示，当活动1执行完 毕后，将进入一个分支判断，根据判断结果的不同，会进入不同的活动。如果分支判断条件 为真，则继续执行活动3；如果分支判断条件为假，则继续执行活动2。

针对这种分支与合并活动流，考虑可以将判断条件加入活动2和活动3的触发条件 中，实现这种活动流向Event-B模型的映射。因此，追加一个判定条件变量decision∈BOOL， BOOL为布尔值。当判定条件为真时，decision＝True；当判定条件为假时，decision＝ False。图4对应的Event-B模型为：

通过判定条件变量decision来控制判断逻辑的执行。

(4.3.2)第二种类型的分支与合并活动流的基本结构如图5所示，这种类型的活动 流可以看作是一种循环。当活动1执行完毕后，将进入一个分支判断，根据判断结果的不同， 会进入不同的活动。如果分支判断条件为真，则继续执行活动2；如果分支判断条件为假，则 返回活动1重新执行，直到分支判断条件为真后才离开活动1。

对于这种类型的活动流，考虑加入一个辅助事件“Loop_Branch”，该辅助事件同样 也不对应于活动图中的任何图形元素，它的作用是当分支判断条件为假时，将辅助变量置 为sequence：＝sequence-1，使活动流能够自动回到活动1中重新执行。图5对应的Event-B 模型如下：

除了利用(4.3.1)的判定条件变量decision外，还额外定义辅助事件“Loop_ Branch”，当decision＝False时，将sequence的值减1。

综上，上述转换方法将UML活动图中的模型元素和基本的活动流类型全部映射到 了Event-B模型中。按照上述的映射规则，可以将UML活动图转换为相应的Event-B模型。