元模型层次的UML动态子图到Coq形式规范的转换

窦　亮　尹　敏　李　超　杨宗源

(华东师范大学计算机科学技术系　上海 201100)



元模型层次的UML动态子图到Coq形式规范的转换

窦亮尹敏*李超杨宗源

(华东师范大学计算机科学技术系上海 201100)

UML动态子图主要包括序列图和状态图等，它们在描述系统的行为方面应用广泛，但是半形式化的语义使它们不能直接进行形式化验证。Coq是目前主流的交互式定理证明器，用形式化的Coq规范来描述UML动态子图模型，可以在此基础上进行对模型的属性进行验证等工作。基于现有工作，提出将UML动态子图模型转换为Coq形式规范的框架，在元模型层次给出状态图和序列图的转换规则，介绍算法和原型工具实现。这种元模型层次的转换方法，保证了转换前后的语法正确性，为进一步分析验证提供了基础。

UML动态子图模型转换元模型Coq Kermeta

0　引　言

UML[1]是面向对象组织(OMG)提出的建模语言，能在各种抽象层次对系统进行描述和建模，被广泛应用在系统的设计阶段。如果在设计阶段就对UML模型进行验证，能尽早地发现系统错误，提高软件质量，减少开销。然而，目前的UML规范缺乏精确的形式语义定义，因此难以进行进一步的分析验证。为了给UML进行精确的语义定义，许多研究工作采用了形式化方法。形式化方法是用于系统规范定义、开发和验证等方面的基于数学的方法，利用适当的数学分析方法，以提高系统的可靠性与安全性。用形式语言来描述UML模型可以弥补UML自身的缺陷，消除开发人员对系统设计理解的不一致性。

Coq[2]是基于归纳构造演算的高阶定理证明器，在跨计算机科学和数学领域的研究中，Coq已经成为一个强有力的工具，它可以作为形式化验证程序的开发环境，也已经成为研究人员对复杂语言的定义进行描述和推理的标准工具。基于定理证明器Coq对各种基础软件的语义进行形式化描述和验证是当前的一个研究热点[3-5]。在之前的工作[6，7]中，我们提出将UML序列图转换为Coq形式规范描述，在Coq定理证明器中证明了语义的相关属性，但是从UML序列图到Coq形式规范的转换过程是手动完成的，这种方式的转换效率较低，且不能保证转换的正确性。

本文提出了一种元模型层面的转换框架，设计了元模型层面的转换规则，提出了针对状态图和序列图这两种UML动态子图到Coq形式规范的转换算法，并在Kermeta[8]中实现了自动转换的原型工具。这种转换不针对某一具体的动态子图模型，而是在元模型层面上完成UML元模型到Coq形式规范的映射，使得转换结果符合目标抽象语法，保持了UML动态子图模型完整的语义成分。

本文的基本内容如下：首先介绍元模型和Kermeta，并给出本文研究的UML状态图和序列图的元模型定义；接着依次介绍UML状态图和序列图转换为Coq形式规范的具体实现，包括转换框架、转换规则和算法几个方面；然后通过实例展示了转换后生成的Coq形式规范；最后介绍相关工作并总结。

1　背景介绍

1.1元模型和Kermeta

OMG组织提出的元对象机制(MOF)是一个四层的元建模框架，在这个体系结构中依次有元元模型层、元模型层、模型层和对象层。每一层都可以看成是上一层的实例，继承了上层模型的元语义；同时又是下一层的抽象，为下一层模型建立了创建模型的元语言。MOF是自描述的，所以不再需要元元元模型。MOF用于定义面向对象元模型，典型的就是UML建模语言，在元模型层面进行模型转换能保证转换前后的模型符合元模型[9]。

Kermeta是一种可执行的元建模语言，可描述模型的结构和行为，支持元模型层面的转换。Kermeta工具集成在Eclipse中，与OMG的EMOF标准兼容。Kermeta语言具有多种特性，包括命令式编程、面向对象编程、面向模型编程、面向方面编程和契约式开发等特性。

1.2状态图和序列图的元模型定义

在Kermeta中实现模型转换，需要指定源/目标元模型，以一个符合源元模型的源模型作为输入。因此，要进行模型转换就需要指定源元模型，下面介绍本文研究的UML状态图和序列图的元模型，分别如图1和图2所示。本文给出的UML状态图和序列图元模型在UML2.0给出的标准元模型上略有删减，并且使用Kermeta自带的Ecore进行构建和绘制。

图1　状态图的元模型

图1是状态图的Ecore元模型。StateModel是该元模型最顶层的类。本文转换后生成的状态图抽象语法定义，支持卫式条件的使用，考虑了状态的进入/退出动作、历史状态记录机制，支持层间转移描述，是较为完整全面的状态图语法定义。

图2　序列图的元模型

图2是序列图的Ecore元模型。SeqModel是元模型最顶层的类。本文转换后生成的序列图抽象语法定义除了考虑消息、生命线、组合片段等元素，还考虑了交互操作符、卫式条件等元素，涵盖了序列图的主要交互操作符片断定义。

2　转换工作

2.1转换框架

模型转换需要保证转换前后模型语法和语义的正确性与完整性，UML图中包含大量的语法和语义信息，直接在模型层面上进行转换很可能会导致转换前后模型信息的丢失。本文在Kermeta中实现的元模型层次的转换工具框架如图3所示，其中UML元模型和模型都属于UML规范范畴，而Coq中对UML的抽象语法定义和UML刻画的实际模型代码符合Coq规范，转换规则是用Kermeta进行编写的。具体地，T1是将UML元模型定义为形式化的Coq抽象语法的过程，通过手工编码实现；T2和T3是模型转换的过程：首先，引入符合元模型的模型，然后，利用转换规则将UML模型转换为Coq形式规范代码，并最终保存为Coq文件，以便在后续的定理证明工作中使用；T4利用了Kermeta的面向方面编程特性，直接将转换规则织入UML元模型中；T5表明UML模型符合UML元模型，即模型是元模型的实例；T6表明转换生成的Coq代码符合Coq中对UML图抽象语法的形式规范定义。

图3　转换框架

该转换框架具有如下的优点：

1. 层次清楚，分离关注，转换规则如果需要变更，只需要修改转换规则层即可；

2. 具备模型无关性，在元模型层面定义转换规则，使得任意符合该元模型的模型都可以使用该转换规则进行转换，和特定模型定义的内容没有关系；

3. 采用了XMI来表示UML模型，使得可以使用不同的建模工具来对目标系统进行建模，方便模型的保存和引入。

2.2状态图的转换规则和算法

从图1中可看出状态图元模型的主要语法单元包括State、Transition、Behavior、Event等。为了将状态图模型转换为Coq形式规范，首先在Coq中为这些元素定义抽象语法如下。这里使用归纳类型定义状态图，关于Coq的使用方法，可以参考文献[10]。

Definition event:= string.

Definition sname:= string.

Definition tname:= string.

Definition action:= string.

Definition seqact:= list action.

Inductive history:Set:=

|none:history

|deep:history

|shallow:history.

Inductive bexp:Type:=

|BTrue:bexp

|BFalse:bexp

|BEq:aexp-> aexp-> bexp

|BLe:aexp-> aexp-> bexp

|BNot:bexp-> bexp

|BAnd:bexp-> bexp-> bexp

|BOr:bexp-> bexp-> bexp

|BImp:bexp-> bexp-> bexp.

(*卫式条件的定义*)

Definition guard:= bexp.

Definition trans:= tname * nat * set sname * event * guard * seqact * set sname * nat * history.

Definition entryexit:= seqact * seqact.

(*状态图的抽象语法定义*)

Inductive sc:Type:=

|basic_sc:sname-> entryexit-> sc

|or_sc:sname-> list sc-> nat-> set trans-> entryexit-> sc

|and_sc:sname-> list sc-> entryexit-> sc.

接着定义元模型层面上的状态图到Coq形式规范的转换规则：

(1) 状态名、事件名和转移名在Coq中都用字符串来表示，分别对应sname、event和tname；

(2) 状态的入口出口动作被映射成包含2个动作(action)列表的二元组；

(3) 状态图中的每个状态都被映射为Coq抽象语法中定义的或状态(or_sc)、基本状态(basic_sc)和与状态(and_sc)中的一种。例如：or_sc是包括状态名、子状态列表、活跃状态序号、子转移列表、入口出口动作的五元组；

(4) 每个卫式条件(guard)都被映射为逻辑谓词bexp规定类型中的一种；

(5) 每一个动作序列被映射为动作列表；

(6) 每个转移都被映射为一个包含转移名、源状态序号、源状态决定因子、触发事件、卫式条件、行为、目标状态决定因子、目标状态序号和历史纪录机制的九元组。为了处理转移可能发生在不同层次的状态之间的情况，用源目标决定因子和目标决定因子两个元素进行指示。即，如果发生层间转移，则源、目标状态序号用来记录最高层的源、目标状态的序号，而决定因子用来记录子层状态的状态名。

根据转换规则，设计UML状态图到Coq形式规范的生成算法：首先，引入符合状态图元模型的状态图模型；其次，对模型进行分析，获取模型中的状态和转移信息，并存储在对应的集合中；最后，按照转换规则，将提取出来的状态、转移、卫式条件等信息转换为Coq形式规范代码。算法描述如下：

算法1

TransList 状态转移信息的集合，初始为空

StateList 状态集合，初始为空。包括简单状态、或状态、与状态，以及历史纪录状态信息

//下述方法织入到元模型最顶层类StateModel上

operation toCoq():String

//通过下面2个方法获取模型的信息，存储在相应集合

//最顶层的region调用getTransList方法

self.packagedElment.asType(StateMachine).region.one.getTransList();

//最顶层的Vertex调用getTransList方法

self.packagedElment.asType(StateMachine).region.one.subVertex.one.asType(Vertex).getStateList(TransList);

//将相应集合中的状态和卫式条件进行编号

setStateID(StateList);

setGuardID(TransList);

re1 = Guard2Coq(TransiList.guard);

re2 = State2Coq();

re3 = Trans2Coq();

//返回转换结果

return re1 + re2 + re3;

end

toCoq ()方法是整个算法的主线，该算法通过调用其他方法实现信息获取、进行调整和转换。对于模型信息的获取，是通过getTransList()和getStateList()两个方法实现的。getTransList()方法被织入到Region类上，而并没有织入到Transition类上，主要是为避免重复获取同一个trans的信息，所以从最顶层的region开始自顶向下地获取所有trans的信息。getStateList()方法需要用到getTransList()获得的信息，故放在getTransList()后执行。这两个方法的伪代码如下：

aspect class Region{

operation getTransList()

//(1)处理最顶层的region中的每个transition元素

foreach trans in transition

//当目标状态为历史状态时

if(self.target.isHistory(self.target)) then

trans.tState = trans.parent;

trans.history = trans.target.kind.name;

//层间转移，则要添加源或目的决定因子sr和tr

if(not isPeer(trans.sState,trans.tState)) then

trans:= changeTrans(trans) ;

TransList = TransList ∪{trans.name × trans.source × trans.sr × trans.event × trans.guard × trans.action × trans.tState × trans.tr × trans.history };

//(2)递归处理其他层的region中的transition元素

foreach vertex in self.SubVertex

if(e.isInstanceOf(State)&&e.getType!=”basic_sc”)then

foreach trans in vertex.region.transition

trans.getTransList();

end }

//getStateList方法被织入到Vertex类上

aspect class Vertex{

operation getStateList(TransList)

// self是当前的最顶层状态

if(self.isInstanceOf(State))then

entryExit = getEntryExit();

//(1)获取基本状态信息

if(self.getType()==”basic_sc”)then

type = “basic _sc”;

StateList= StateList ∪ {self.name × entryExit × type};

//(2)获取或状态信息

else if(s.getType()==”or_sc”)then

subTrans = getSubTrans(TransList);

subStates = getSubStates();

type = “or_sc”;

StateList= StateList ∪ {self.Name × subStates × 0 × subTrans × entryExit × type};

//递归调用getStateList将当前状态的每个子状态加入StateList

foreach s in self.subStates

if(not isHistory(s1))then s.getStateList(transList);

//(3)与状态转换与或状态的处理类似，省略

else if(self.getType()==”and_sc”)then ……

StateList = StateList ∪ {self.Name × subStates × entryExit × type}；

end }

其中，getType()通过判断状态中region的数目来确定状态的类型；chageTrans(trans)用来改变trans的源/目标状态，以及设置源/目标决定因子；isHistory()用来判断状态是否是历史类型的伪状态；getTransList()和getSubStateList()分别用来获得子状态和子转移；Trans2Coq()与State2Coq()的算法相似，限于篇幅未给出算法；Guard2Coq()为bexp中使用的操作符建立了相应的解释器，由解释器将卫式条件转换为相应的Coq代码。

2.3序列图转换规则和算法

序列图的抽象语法定义主要处理的语法单元包括LifeLine、 Event、 Message、Fragment等。首先在Coq中为这些元素定义抽象语法，也使用归纳类型来定义序列图：

Inductive kind:Set:= | Send:kind | Receive:kind.

Notation ″!″:= Send

Notation ″?″:= Receive

Definition signal:= string.

Definition lifeline:= string.

Definition event:= kind * signal * lifeline * lifeline.

Inductive id:Set:= Id:nat-> id.

(*卫式条件的定义*)

Inductive cnd:Type:= | Bvar:id-> cnd | Btrue:cnd

|Bfalse:cnd | Bnot:cnd-> cnd | Band:cnd-> cnd-> cnd

|Bor:cnd-> cnd-> cnd | Bimp:cnd-> cnd-> cnd.

(*序列图的抽象语法定义*)

Inductive seqDiag:Set:=

|Dtau:seqDiag

|De:event-> seqDiag

|Dpar:seqDiag-> seqDiag-> seqDiag

|Dalt:cnd-> seqDiag-> seqDiag-> seqDiag

|Dopt:cnd-> seqDiag-> seqDiag

|Dstrict:seqDiag-> seqDiag-> seqDiag

|Dloop:nat-> cnd-> seqDiag-> seqDiag.

其中Event中的事件类型分为发送事件和接受事件，分别用‘?’和‘!’表示。序列图被表示成一个归纳类型，可以为空(Dtau)，可以通过事件(De)构成，也可以是通过交互操作符构成。这里只考虑五种交互操作符Dalt、Dopt、Dstrict、Dloop和Dpar。

元模型层面上的序列图到Coq形式规范的转换规则主要包括：

(1) 消息名和生命线名在Coq中都用字符串来表示，分别对应signal和lifeline类型；

(2) 序列图中的每个事件被映射成Coq抽象语法中定义的类型、消息名、接受/发送生命线组成的四元组；

(3) 消息的约束条件被映射为cnd中规定的类型中的一种，并且约束条件中的变量被映射为自然数类型的id；

(4) 利用前面3条规则，将序列图映射为由抽象语法中事件，约束条件和五种交互操作符递归构造的Coq规范。

序列图模型到Coq形式规范转换的算法，与状态图的转换相似，由于要处理的语法单元相对较少，因此去掉了存储模型中元素的步骤。算法如下：

算法2

//下述方法织入到元模型最顶层类SeqModel上

operation toCoq():String

result:String;

//将依赖于消息的发送和接受事件，转换为coq代码

foreach m in message

result = result + m.message2Coq();

//将每个fragment转换为Coq代码。

foreach f in fragment

result = result + f.fragment2Coq();

return result;

end

//下述方法织入到Message类上

operation message2Coq():String

mName = self.name;

//获得发送和接受消息的生命线(lifeline)

sLineName = getSendLineName();

rLineName = getRecLineName();

//发送事件

sendEvent=write2Coq(“!”,mName,sLineName,rLineName );

//接受事件

recEvent = write2Coq(“?”,mName,sLineName,rLineName );

return sendEvent + recEvent;

end

//下述方法织入到InteractionFragment类上

operation fragment2Coq():String

//(1)当fragment为事件类型时，将发送接受事件转换

if(self.isInstanceOf(OcreenceSpecification))then

if(self.type ==”send”)then

result = result + event2Coq(self.name,“send”);

else if(self.type ==”receive”)then

result = result + event2Coq(self.name,“receive”);

//(2)当fragment为组合片段类型时

else if(self.isInstanceOf(CombinedFragment))then

//当交互操作符为单元操作符opt时

if(self.operand == “opt”)then

result = result + CombinetoCoq (operand,self.name);

//当为其他四种二元操作符时

else

leftOp = self;

//右操作符为下一个fragment

rightOp = nextFragment;

result = result + Combine2Coq(operand,leftOp,rightOp);

//对组合片段的子片段进行转换

foreach f in self.operand.fragment

result = result + f.fragment2Coq();

return result;

end

算法中event2Coq()实现将某个发送或接受事件类型的组合片段转换为Coq代码；Combine2Coq则实现将包含单元或者二元操作符的组合片段转换为Coq代码。

3　实例研究

根据转换框架和算法，我们实现了UML动态子图到Coq代码转换的原型工具，实现了转换过程的自动化。本章以用户在自动取款机(ATM)取款的情景为例，绘制了图4和图5所示的序列图模型和状态图模型，用来对原型工具进行测试。

图4　序列图模型实例

图4是用户在ATM上取款的简化的交互场景的序列图。用户首先插入银行卡，然后输入密码，由ATM机根据输入的信息进行身份验证，发送验证成功(loginSucc)或验证失败(loginFail)的消息；如果登录成功，且帐户余额大于零，用户可以选择进行一次取款操作。原型工具执行后自动转换生成如下的Coq形式规范代码：

Definition C1:cnd:= BEq(AId checkPwd)(ANum 1).

Definition C2:cnd:= BGt(AId balance)(ANum 0).

Definition sInsertCard:event:= (!,″InsertCard″,″User″,″ATM″).

Definition rInsertCard:event:= (?,″InsertCard″,″User″,″ATM″).

Definition spwd:event:= (!,″pwd″,″User″,″ATM″).

Definition rpwd:event:= (?,″pwd″,″User″,″ATM″).

Definition sloginSucc:event:= (!,″loginSucc″,″ATM″,″User″).

Definition rloginSucc:event:= (?,″loginSucc″,″ATM″,″User″).

Definition swithdraw:event:= (!,″cmd″,″User″,″ATM″).

Definition rwithdraw:event:= (?,″cmd″,″User″,″ATM″).

Definition sloginFail:event:= (!,″loginFail″,″ATM″,″User″).

Definition rloginFail:event:= (?,″loginFail″,″ATM″,″User″).

Definition ExampleSeq:SeqDiag:= Dstrict

(Dstrict (Dstrict (De sInsertCard)(De rInsertCard))

(Dstrict (De spwd)(De rpwd)))

(Dalt C1 (Dstrict(Dstrict (De sloginSucc)(De rloginSucc))

(Dopt C2 (Dstrict (De scmd)(De rcmd))))

(Dstrict (De sloginFail)(De rloginFail))).

图5　状态图模型实例

图5是用户在ATM上取款时，ATM服务器状态变化情况的状态图。Execute和Log是并行运行的或状态，分别表示系统处于给用户提供服务的执行状态，以及系统在进行日志记录操作的状态。原型工具执行后转换为如下Coq形式规范代码：

Definition g0:guard:= BGt (AId balance) (ANum 0).

Definition g1:guard:= BEq (AId checkPwd) (ANum 1).

Definition g2:guard:= BNot (BEq (AId checkPwd) (ANum 1)).

Definition t4:trans:=

(″t4″,1,nil,″withdraw″,g0,nil,nil,0,shallow).

Definition t1:trans:=

(″t1″,0,nil,″insertCard″,BTrue,nil,nil,1,none).

Definition t2:trans:= (″t2″,0,(″Indentify″::″InputPwd″::nil),

″pwd″,g1,″loginSucc″::nil,nil,1,none).

Definition t3:trans:=

(″t3″,1,nil,″pwd″,g2,″loginFail″::nil,nil,1,none).

Definition t5:trans:=

(″t5″,0,nil,″insertCard″,BTrue,nil,nil,1,none).

Definition n0:sc:= basic_sc ″CardIn″ (nil,nil).

Definition n1:sc:= basic_sc ″InputPwd″ (nil,nil).

Definition n2:sc:= or_sc ″Indentify″ (n0::n1::nil) 0

(t1::t3::nil) (nil,″exlogin″::nil).

Definition n3:sc:= basic_sc ″Accept″ (″command″::nil,nil).

Definition n4:sc:=

or_sc ″Execute″ (n2::n3::nil) 0 (t4::t2::nil) (nil,nil).

Definition n5:sc:= basic_sc ″Wait″ (nil,nil).

Definition n6:sc:= basic_sc ″Write″ (nil,nil).

Definition n7:sc:=

or_sc ″Log″ (n5::n6::nil) 0 (t5::nil) (nil,nil).

Definition n8:sc:= and_sc ″ATMServer″ (n4::n7::nil) (nil,nil).

这些自动生成的Coq形式规范代码，可以在定理证明器Coq中直接打开，进行下一步的分析和验证，使之前的研究工作[6，7]更加完善。本文完整源代码和实例可在文献[10]中下载。

4　相关工作

国内外将形式化方法应用于UML的研究一直是热点。较多的工作致力于类图的形式化和验证，如文献[12]等。对于UML的典型动态子图——序列图和状态图，也有许多形式语义研究工作，可参见综述文献[13，14]。本节主要讨论将UML动态子图转换为形式规范的相关工作。

文献[15，16]都将UML状态图转换为了B语言规范，但是文献[15]中没有将状态内部的动作考虑在内，且只对简单的状态图进行了分析。在文献[16]中为了表示状态图中的事件和转移，加入了自己定义的新标签，这就使得转换得到的B语言规范不符合标准的B语言抽象语法。本文的状态图语法定义全面完整，并且生成的Coq规范也符合目标抽象语法。文献[17]实现了UML状态图到Petri网的转换，但是整个转换都在模型层面进行，不能保证转换前后语法的一致性。

文献[18]基于B方法对用例图模型与序列图模型进行形式化转换，提出了转换规则，但没有实现自动转换工具。文献[19] 采用了和本文相似的元模型层面的转换框架，将序列图和状态图转换为广义随机Petri网，但是也只考虑了基本元素的转换，对序列图没有考虑组合片段的情况，对状态图没有考虑历史伪状态的转换。本文则在全面考虑各种元素的转换规则的基础上，实现了自动化的转换工具，由于利用了Kermeta的面向方面编程特性，规则的修改和扩展也很容易。

5　结　语

本文提出了一种元模型层次的UML动态子图到Coq形式规范的转换框架。首先给出了状态图和序列图形式化Coq抽象语法，然后提出元模型层面转换规则，并最终实现从UML动态子图到Coq形式规范转换的原型工具。本文的工作，使得从UML动态子图到Coq规范的自动转换成为现实，保证了转换前后语法的正确性，得到了符合目标抽象语法的Coq形式规范，为分析验证工作提供了便利。下一步的工作是完善现有工作中UML状态图和序列图的特性，为实际应用提供更全面的支持。

[1] Rumbaugh J,Jacobson I,Booch G.Unified Modeling Language Reference Manual[M].The Pearson Higher Education,2004.

[2] Paulin-Mohring C.Introduction to the Coq proof-assistant for practical software verification[C]//Tools for Practical Software Verification.Springer Berlin Heidelberg,2012:45-95.

[3] Leroy X.Formal verification of a realistic compiler[J].Communications of the ACM,2009,52(7):107-115.

[4] Chlipala A.A verified compiler for an impure functional language[C]//Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,2010,45(1):93-106.

[6] Zuo Y,Dou L,Xu L,et al.Mechanized semantics of UML sequence diagrams[C]//Proceedings of the IASTED International Conference on Engineering and Applied Science,2012:188-195.

[7] Dou L,Lu L,Yang Z,et al.Towards mechanized semantics of UML sequence diagrams and refinement relation[C]//Proceedings of the 24th IASTED International Conference on Modelling and Simulation,2013:262-269.

[8] Kermeta[EB/OL].[2015-3-1].http://www.kermeta.org/.

[9] Cetinkaya D,Verbraeck A.Metamodeling and model transformations in modeling and simulation[C]//Proceedings of the Winter Simulation Conference.Winter Simulation Conference,2011:3048-3058.

[10] Bertot Y,Castéran P.交互式定理证明与程序开发:Coq 归纳构造演算的艺术[M].顾明等译.清华大学出版社,2010.

[11] 元模型层次的UML动态子图到Coq形式规范的转换工具源代码及案例[EB/OL].[2015-3-1].https://github.com/lisa-dou/UML2Coq.

[12] Lano K,Clark D,Androutsopoulos K.UML to B:Formal verification of object-oriented models[C]//Integrated Formal Methods.Springer Berlin Heidelberg,2004:187-206.

[13] Micskei Z,Waeselynck H.The many meanings of UML2 Sequence Diagrams:a survey[J].Software & Systems Modeling,2011,10(4):489-514.

[14] Lund M S,Refsdal A,Stφlen K.Semantics of UML Models for Dynamic Behavior[M]//Model-Based Engineering of Embedded Real-Time Systems.Springer Berlin Heidelberg,2010:77-103.

[15] Ledang H,Souquières J.Contributions for modelling UML state-charts in B[C]//In Integrated Formal Methods,Springer Berlin Heidelberg,2002:109-127.

[16] Idani A,Ledru Y.Dynamic graphical UML views from formal B specifications[J].Information and Software Technology,2006,48(3):154-169.

[17] Pais R,Gomes L,Barros J P.From UML state machines to Petri nets:History attribute translation strategies[C]//IECON 2011-37th Annual Conference on IEEE Industrial Electronics Society.IEEE,2011:3776-3781.

[18] 夏志翔,徐中伟,陈祖希,等.UML模型形式化B方法转换的实现[J].计算机应用与软件,2011,28(11):15-20.

[19] Bernardi S,Donatelli S,Merseguer J.From UML sequence diagrams and statecharts to analysable petri net models[C]//Proceedings of the 3rd international workshop on Software and performance.ACM,2002:35-45.

A METAMODELLING LEVEL TRANSFORMATION FROM UML DYNAMIC SUB-DIAGRAMS TO COQ

Dou LiangYin Min*Li ChaoYang Zongyuan

(DepartmentofComputerScienceandTechnology,EastChinaNormalUniversity,Shanghai201100,China)

UML dynamic sub-diagrams mainly comprise the sequence diagram and the state machine diagram,they are widely applied in describing system behaviours.However,it is hard to perform direct formal verification due to the semi-formal semantics of UML.Coq is a mainstream interactive theorem prover,using formal Coq specification to describe UML dynamic sub-diagrams model can carry out verification on model’s attributes on that basis.According to our previous work,the paper presents a framework to transform UML dynamic sub-diagrams model to Coq formal specifications,and the transformation rules of UML sequence diagram and state machine diagram are offered at meta-modelling level.The algorithm and the implementation of prototype tool are also introduced.This metamodelling level transformation framework ensures the correctness of semantics before and after transformation,and lays the basis for further analysis and verification.

UMLDynamic diagramsModel transformationMetamodellingCoqKermeta

2015-04-03。国家自然科学基金项目(61070226)。窦亮，讲师，主研领域：形式化方法，定理证明和软件工程。尹敏，讲师。李超，硕士生。杨宗源，教授。

TP311

A

10.3969/j.issn.1000-386x.2016.08.002