Modeling is an important aspect of UML formal verification that directly affects the quality and efficiency of the verification. Formal models are the foundation of formal verification. As UML diagrams only have semi-formal semantics, they cannot be used for formal verification directly. Recent studies present model transformation from semi-formal UML models to formal models to solve the issues. In this paper, a metamodeling level transformation tool from UML sequence diagrams to formal Coq codes is presented. Using Kermeta (a metamodeling language) and predefined transformation rules that directly added to the metamodel of UML sequence diagrams, models of UML sequence diagrams are transformed into XMI, an intermediate format, and finally to formal Coq codes. This paper is part of our formal verification work for UML sequence diagrams, and the automatically generated Coq codes can be used for further formal verification using the theorem proof assistant Coq in our related works. This paper perfects the whole verification work and provides useful support to improve the integration density of formal verification in the formalization process of UML sequence diagrams.
Unified Modeling Language (UML) [
Despite the wide use of UML, a number of problems have been identified
due to its semi-formal semantics. For example, a developer’s understanding of
UML models may differ from the designer’s understanding, tools for analyzing
UML models may be limited to syntactic analysis [
UML sequence diagrams have been widely used in the early stage of software development process. Different objects or processes are represented by parallel vertical lines in a sequence diagram. Objects or processes communicate with each other via messages that are represented by horizontal arrows. UML sequence diagrams play an important role in helping developers understand the runtime behaviours of system. Thus, it is important to verify the models when using UML sequence diagrams in the design stage.
A great deal of UFV works have been done, most of them focus on two
aspects: the transformation rules from models of UML diagrams to formal models,
and the verification process based on the formal models. In previous work [
Metamodeling is the process to define a modeling language completely and
precisely. The abstract syntax of modeling language is described by a metamodel,
which is also defined in a metamodeling language. A metamodeling language
is a superior language to describe modeling languages and it is also defined
with a metamodel. The metamodel of a metamodeling language is called
metametamodel, which is self-descibing [
The rest of the paper is structured as follows. Firstly, the related work is reviewed in Section 2. Section 3 recalls the model transformation in Kermeta and briefly introduces Coq. Transformation rules and a case study are showed in Section 4. Finally, we conclude in Section 5. 2
A variety of formalization work has been proposed for UML diagrams over the
years. A formal framework is provided to support visual simulation of UML
models that composed of class, object, state, sequence and collaboration
diagrams, and an integrated semantics of these models is presented in [
Our work not only presents transformation rules at metamodeling level, but also implement a transformation process from UML sequence diagrams to Coq codes automatically in Kermeta. The generated codes can be used for further formal verification. 3 3.1
Metamodeling and Model Transformation in Kermeta
Kermeta is an executable metamodeling language which supports describing
both structures and behaviours of metamodels. Kermeta is integrated with Eclipse,
and distributed as Eclipse plug-in. It is fully compatible with the OMG Essential
Meta-Object Facility (EMOF) [
As Kermeta relies on EMF for model storage, regular EMF metamodels, Ecore files, can be used. These metamodels can be created and edited using the generic model editor provided with the EMF. Operations can be added to any class in metamodels using the action language provided by Kermeta. In addition, once the source metamodel is created, source model that confirms to the source metamodel can be generated manually using the model editor.
Model transformation in Kermeta takes one source model as input, and produces one target model as output. Both source model and target model should conform to specific metamodel or abstract syntax, and transformation rules should be defined to drive the transformation. That is, given the source model, source and target metamodel (or abstract syntax), and transformation rules, target model can be generated automatically.
In order to write a model transformation in Kermeta, the source and target metamodels (or abstract syntax) should be defined at first. In our work, UML sequence diagrams is the source modeling language and Coq is the target modeling language. Metamodel of UML sequence diagrams and abstract syntax of Coq are explained in the following sections. 3.2
Lifeline, Message and InteractionFragment are contained by Interaction. Lifeline, message and fragment are the basic elements of UML sequence diagrams. A lifeline represents a specific object. Lifelines communicate with each other through messages, each message triggers two events: send event and receive event. A fragment is an instance of Event and CombinedFragment that inherit from the abstract class InteractionFragment. Fragments describe the behaviour information of UML sequence diagrams. Events are the basic behavioral constructs of UML sequence diagrams and can be combined to form larger behavioral constructs called CombinedFragment. A combined fragment consists of an interaction operator, one or more operands which are comprised of events or combined fragments, and an optional guard condition. A combined fragment covers a set of lifeline and decides the execution mode and condition of fragments (events or combined fragments). 3.3 Coq is a theorem proof assistant. The Calculus of Inductive Constructions (CIC) is the underlying core language of Coq. CIC is based on the calculus of constructions extended by inductive definitions as they are known from the constructive type theory.
The Coq abstract syntax represents UML sequence diagrams as an inductive type as below, which enables reasoning by case analysis and induction. Inductive Seq : Set := |Skip : Seq |E : Event -> Seq |Alt : Seq -> Seq -> Seq |Opt : Seq-> Seq |Strict : Seq -> Seq -> Seq |Loop : nat -> Seq -> Seq |Par : Seq -> Seq -> Seq.
Seq is defined inductively as events and operators in the Coq abstract syntax. Skip represents an empty graph. An E represents an event. Event is the basic element, it consists of its type and a message, it is defined as :
Definition Event := Type * Message.
Type ∈ {?,!}, ! represents sending, and ? represents receiving. Message is defined as a triple :
Definition Message := mName * Lifeline * Lifeline. mName represents the name of the message, a message has two lifelines, the first one represents a lifeline sends the message, the second one represents a lifeline receives the message. Furthermore, operators are considered in our work, they decide the execution mode between fragments. We only consider five interaction operators: alt, opt, par, loop and strict. Among the operators, opt is unary and other operators are binary. What calls for special attention is that, two events always occur accompanying a message, these two events are considered as a special combined fragment with strict execution mode.
Models of UML sequence diagrams should be transformed to events and operators definitions that confirm to the abstract syntax. This is discussed in the following section. 4
In the preceding sections, we have described the core concepts of our transformation tool, a more detailed description of the transformation process in our tool is shown in Fig.2.
Step1(Manually): Design model of the target system in modeling tools, and load the model into our tool.
Step2(Automatically): Transform the model of UML sequence diagrams to Coq codes with the transformation rules, all these rules are added to classes of UML sequence diagrams metamodel using our tool. This process is also implemented automatically.
Step3(Automatically): Output of model transformation are provided to Coq as input. Further formal verification is based on this output. Once the source metamodel and the target abstract syntax are defined, models of target system can be transformed to Coq codes confirms to the abstract syntax. The transformation has two steps. In the first step, all the events of source model are transformed to events definition in Coq. In the second step, behaviour elements of source model, i.e. events and combined fragments, are transformed to operators definition in Coq. Before transformation rules of events are given, transformation rule of message is defined in Rule 1.
Rule 1. In UML sequence diagrams, a message is transmitted from one lifeline to another lifeline, this message should be mapped to message variable definition in Coq.
According to Rule 1, we can obtain the Coq codes of the message in Fig.3:
Definition m_m1: Message :=("m1","L1","L2").
Once the transformation rules of message is defined, Rule 2 for events transformation is given as below.
Rule 2. In UML sequence diagrams, when a message named m1 is transmitted, two related events occur, one is send event: sm1, another is receive event: rm1, these two events should be mapped to event variable definition and initialization in Coq.
According to Rule 2, we can obtain the Coq input codes of the events in Fig.3:
Definition sm1: Event := (!,m_m1).
Definition rm1: Event := (?,m_m1).
According to the two definitions above, we can obtain the ultimate Coq input codes of the events in Fig.3 :
Definition sm1: Event := (!,("m1","L1","L2"))
Definition rm1: Event := (?,("m1","L1","L2"))
Execution modes between fragments describe the structure information of UML sequence diagrams. In the second step, we define the transformation rules of behaviour information. We start with the transformation rule of events.
Rule 3. In UML sequence diagrams, two events, send event and receive event, always accompanies a message, the execution mode between them is strict. Two events of this message are considered as a special combined fragment with strict execution mode and should be mapped to operators definition and initialization in Coq.
According to Rule 3, we can obtain the operators codes of the two events in Fig.3:
strict(E sm1)(E rm1)
Rule 4. In UML sequence diagram, a combined fragment is comprised of one operator and fragments, fragments ∈ {Event,CombinedF ragment}, and we specify that any two adjacent fragments without operators are in strict execution mode. Combined fragments in sequence diagrams should be transformed to operators definition in Coq.
According to the Rule 4, we can obtain the Coq codes of the combined fragment in Fig.4:
Alt(Strict (E sm1)(E rm1))(Strict (E sm2)(E rm2)) // sm2 and rm2 is defined in the same way as sm1 and rm1 Using action language and aspect-orientation mechanism in Kermeta, transformation rules can be added to corresponding class in the metamodel of UML sequence diagrams. procedure main() //import a sequence diagram model seq :SeqModel = loadModel(seq.xmi); //call the method toCoq to perform transformation coqCode : String = seq.toCoq(); //save the transformation result saveModel(coqCode); end main //toCoq is added to the top level class SeqModel procedure toCoq():String result :String; foreach m in message
result = result + m.message2Coq(); foreach f in fragment
result = result + f.fragment2Coq(); return result; end toCoq //message2Coq is added to class Message procedure message2Coq():String mName = self.name; sLineName = getSendLineName(); rLineName = getRecLineName(); sendEvent=write2Coq(!, mName, sLineName, rLineName ); recEvent = write2Coq(?, mName, sLineName, rLineName ); return sendEvent + recEvent; end message2Coq // fragment2Coq is added to class InteractionFragment procedure fragment2Coq():String //(1)when fragment is event 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) when fragment is combinedFragment else if(self.isInstanceOf(CombinedFragment))then if(self.operand == opt)then
result = result + CombinetoCoq (operand, self.name); else leftOp = self; rightOp = nextFragment; result = result + CombinetoCoq(operand, leftOp, rightOp); //transform every subfragment in combinedfragment foreach f in self.operand.fragment
result = result + f.fragment2Coq(); return result; end fragment2Coq Operation event2Coq transforms a send or receive event to Coq codes,and operation Combine2Coq transforms a combined fragment with unary or binary operators to Coq codes. 4.3
In this section, a simple example is presented to illustrate our transformation. Fig.5 shows a scene that a user sends his account id and password to the Automatic Teller Machine (ATM)and get a reply from it. If logged in successfully, the user can check balance or withdraw money.
After reading the XMI file of Fig.5 and parse it, our transformation tool automatically extract the useful information and transform it to formal Coq codes that confirms to the abstract syntax we have defined: Definition sid :Event :=(!,("id","User","ATM") Definition rid :Event :=(?,("id","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 :=(!,("withdraw","User","ATM") Definition rwithdraw :Event :=(?,("withdraw","User","ATM") Definition scheck :Event :=(!,("check","User","ATM") Definition rcheck :Event :=(?,("check","User","ATM") Definition sloginFail :Event :=(!,("loginFail","ATM","User") Definition rloginFail :Event :=(?,("loginFail","ATM","User") Definition ExampleSeq :Seq :=
Strict (Strict (Strict (E sid)(E rid))(Strict (E spwd)(E rpwd))) (Alt(Strict(Strict (E sloginsucc)(E rloginsucc))(Opt (Strict (Strict (E swithdraw)(E rwithdraw))(Strict (E scheck)(E rcheck))))) (Strict (E sloginfail)(E rloginfail))). 5
Modeling is an important step in the UML diagrams formalization, it lays the foundation for further formal verification. In this paper, we focus on the model transformation for UML sequence diagrams and implement a metamodeling transformation tool in Kermeta. Firstly, metamodel of UML squence diagrams and exact definition of Coq abstract syntax are given. Then, using predefined transformation rules that directly added to the classes in UML sequence diagrams metamodel, models of UML sequence diagrams are automatically transformed to Coq codes so that further verification could be done. Finally, we present a case study to show the result of model transformation. The result can be as the input codes for formal verification in Coq theorem prover.
We consider model concepts of sequence diagrams but not the whole, we can further define and extend our transformation rules. Another future direction is to extend the transformation to implement the transformation of UML state diagrams. In addition, our transformation tool is integrated with Kermeta, but separated with the verification process, we hope to combine them together and package them as a new exe or web-based tool in future.
This work is supported by National Natural Science Foundation of China (No.61070226).