=Paper=
{{Paper
|id=Vol-2019/modevva_2
|storemode=property
|title=Supporting Model Refinement with Equivalence Checking in the Context of Model-driven Engineering with UML-RT
|pdfUrl=https://ceur-ws.org/Vol-2019/modevva_2.pdf
|volume=Vol-2019
|authors=Raquel Oliveira,Juergen Dingel
|dblpUrl=https://dblp.org/rec/conf/models/OliveiraD17
}}
==Supporting Model Refinement with Equivalence Checking in the Context of Model-driven Engineering with UML-RT==
https://ceur-ws.org/Vol-2019/modevva_2.pdf
Supporting Model Refinement with Equivalence
Checking in the Context of Model-Driven
Engineering with UML-RT
Raquel Oliveira Juergen Dingel
IRIT and Univ. Toulouse Queen’s University
Toulouse, France Kingston, Canada
Email: raquel.oliveira@irit.fr Email: dingel@cs.queensu.ca
Abstract—Through model refinement, system developers can a formal specification language, i.e., a language with a clearly
build a system model incrementally and gradually unveil the defined and unambiguous semantics. Formal verification tools
details of the system. While the process of incrementally building provide a rigorous way for analyzing a model by exhaustively
a model can help developers master the complexity of the system,
even small modifications to a model may lead to a loss of initially exploring its state space, which can be used to evaluate the
present desirable behavior and properties. Furthermore, the impact when the model changes.
impact of such changes on the model behavior becomes difficult Despite their acceptance, formal techniques are not trivial to
to detect once the model size increases. We propose a formal use as formal languages are complex to master and to integrate
approach to compare pairs of models in which the second model with semi-formal languages. The challenge is to integrate
is the result of an incremental modification of the first. The results
have shown that the approach helps verify that the modification formal techniques with MDE [9], in order to benefit from the
is behavior preserving, i.e., that it is a refinement in the sense of rigorousness and automation provided by formal verification
the formal methods literature. tools to support the analysis of non-formal models and to make
formal verification amenable to MDE practitioners [29].
I. I NTRODUCTION Although several approaches have been proposed to bridge
Model-Driven Engineering (MDE) designates approaches in this gap using model checking techniques, less attention has
which models are created to describe a system, and from which been paid to the comparison of models related with each other
a concrete implementation can be derived [9]. MDE provides by an abstraction-refinement relation. This paper proposes
a means to handle system complexity with abstraction and an approach based on formal methods to compare U ML -RT
automation. A model is a representation of what is perceived models in order to show behavioral preservation when one
as the relevant characteristics of the system [23], and it can model is the evolution of another one. For this, U ML -RT
be used for a variety of purposes such as understanding, models are automatically translated into a formal specification,
communication, analysis, and code generation. and a well-known refinement pattern is implemented using a
There are limits to the human ability to understand complex- U ML profile. The approach is tool supported and integrated
ity [14]. Gradually adding details to the model is one way to into the Eclipse platform.
master system complexity. MDE development often proceeds
by incrementally adding details into the model. One starts with II. MDE AND F ORMAL M ETHOD C ONTEXT
a very high level model in which, e.g., complex states are This section introduces the main concepts of the MDE
summarized by just one state, and then, once the developers language we use in this work, the refinement technique we
are satisfied with this high-level model (e.g., certain tests are apply, as well as the formal methods background needed to
passed, certain properties are satisfied, etc.), they can unveil understand the approach.
this complex state by adding detail to it. It would be helpful for
developers to be able to check that these kinds of development A. UML-RT
steps are behavior preserving, i.e., that the new model is indeed U ML -RT is a language that integrates constructs suitable for
equivalent in some sense to the previous model, because then modeling complex, event-driven, and potentially distributed
it may not be necessary to run the same tests again and check real-time systems. A U ML -RT model consists of five basic
that properties are preserved. concepts: capsules, ports, protocols, connectors, and state ma-
Although models aim to abstract system complexity, they chines (as illustrated in the example of an ATM in Figure 1).
can become very complex too, making it difficult to inspect Capsules are the central modeling construct of the for-
them manually. Such analysis can be done using formal malism. They are used to represent the major architectural
methods, which are techniques strongly rooted in mathematics elements of real-time systems [27]. Capsules are U ML active
and which rely on formal models. Formal models are written in classes with composite structure that communicate through
C. Equivalence Checking
Equivalence checking is a formal technique that provides a
means to show whether two systems exhibit exactly the same
behavior. It can be used in this case to show the semantic
conformance between an abstract and a refined model. First,
a formal model for each system to be compared is created.
Then, LTSs (labeled transition systems) representing the state
space of the formal models are automatically generated, which
represent all possible evolution of the system. Such LTSs can
Fig. 1. An example of an ATM then be automatically compared using a given equivalence
relation. For instance, strong bisimulation [22] is the most
restrictive relation: two systems are strongly bisimulation
ports typed by protocols. Communication is done by message equivalent whenever they can perform the same actions to
passing. Protocols specify the messages that can be exchanged reach strongly bisimulation equivalent states, i.e., they agree
between capsules. Ports fully isolate a capsule’s implementa- on each step they take.
tion from its environment, all the communication being done There are cases in which some transitions may be skipped in
through connectors that link the capsule ports. Connectors the analysis. These transitions are considered “non observable”
model communication channels, and each connector supports a and hidden by receiving a special label (τ ) in the LTS, allowing
single protocol. Capsules can have an internal behavior, which weaker bisimulation relations to bypass them when checking
is described using state machines. Using the aforementioned equivalence between models. One of the most important
concepts, U ML -RT allows one to create models of real-time features in process algebra is that of abstraction, since it
systems at different levels of detail. provides us with a mechanism to hide actions that are not
observable, or not interesting for any other reason [30]. By
abstraction, some of the actions in a LTS are made invisible
B. Abstraction Patterns or silent (τ -actions). Consequently, any consecutive execution
of hidden (τ ) steps cannot be recognized since they are not
In [28], the author presents a catalog of abstraction patterns
observable [30]. Several bisimulation relations exist that can
for model-based software engineering. These patterns can be
deal with τ transitions. Branching bisimulation [30] is one of
seen as model transformation patterns, and they can be applied
the most commonly used.
in both directions: to obtain a more abstract version of the
The numerous equivalence relations available in the litera-
model as well as to obtain a more refined one (called, in
ture can be used to show equivalence between two systems
this case, refinement patterns). This catalog proposes and
at different levels of abstraction. The choice of the equiva-
groups 13 patterns into three classes: structural, behavioral,
lence relation depends on the abstraction level of the models
and temporal patterns. The first one contains 5 patterns, the
and the verification goals. In case of non-equivalent models,
second one contains 4 patterns, and the last one contains 4
the equivalence checker generates a counter example, i.e., a
patterns.
sequence of steps that leads both systems into a state where
In this paper, we describe an example in which the Summary they are not equivalent. Finally, the results of the analysis can
State behavioral pattern is studied. In this pattern, a certain help to find anomalies in the modeled systems.
detailed-level behavior, described by a state machine, is ab-
stracted into a state at a higher level (Figure 2). Two concepts D. LNT Formal Specification Language
are then introduced: glass state and cross-over transitions. The In order to compare two U ML -RT models using equivalence
former to represent the set of states and transitions that are checking, they should first be described by means of a formal
being abstracted, the latter to represent transitions that cross
in or out of the glass state, and which have corresponding
representatives in the abstract graph. Cross-over S1 S1’
transition
The primary focus of [28] is on the syntactic aspects of
t1 t1’
the transformations. The semantic conformance between a S5 S5’
S2
refinement and its abstraction is not discussed in the paper.
t5 t6’
According to the author, “semantic conformance is the prop- t2
t6 AbsS
erty that an abstraction is phenomenologically consistent with S3
its corresponding refinement”. We move the work described t4
in [28] forward by providing a way to verify the semantic
S4
conformance of the refinement transformations, in the sense
that the relevant structural and behavioral properties of the Glass State
abstraction are retained in the refinement. We verify such
behavioral-preserving refinement using equivalence checking. Fig. 2. The summary state pattern
language. We chose L NT [4] to describe the original models,
because L NT and U ML -RT have similar features, as described
in Section IV-C.
L NT is a language derived from the E-L OTOS [16] standard.
It improves L OTOS [15] and can be translated to L OTOS
automatically. L OTOS was originally devised to support stan-
dardization of OSI (Open Systems Interconnection), but has
been used now more widely to model concurrent systems.
L NT inherits from L OTOS the way a system is represented:
with a data part, based on algebraic abstract data types, and
with a control part, based on process calculus. In L NT, both
parts (data and control) share a common syntax close to
the imperative programming style [10]. In L NT, a system
is described by means of blocks of code called modules. Fig. 3. New ATM model after adding details to the complex states
Modules can contain types, channels, functions, and processes.
A process is an object which denotes a behavior; it can be
parameterized by a list of formal gates (or channels), through Waiting for card validation state once a confirmation is re-
which the process can communicate with other processes. ceived from the functional core capsule. In the FunctionalCore
L NT it is strongly typed, and types such as int, char, side, the original Validating state is also further developed to
boolean, string, etc. are available. Besides, the language include some details of the validation process.
provide constructs such as conditional statements, iteration, For the sake of simplicity, the logic for validating the card,
assignment, sequential composition, etc. The language can the code and the transactions are out of scope of this paper,
also handle concurrency, communication, non-determinism, and we focus on the messages exchanged by the capsules. We
signaling, exceptions, etc. An example of a L NT specification do not consider either the case of invalid cards, codes, and
is illustrated in Figure 6 and it will be detailed in the transactions. In this context, developers may wonder whether
Subsection IV-C. this new version of the model preserves its initial behavior,
i.e., whether it is a refinement of the original model.
III. RUNNING E XAMPLE
To introduce our verification approach, consider a simplified IV. C OMPARING UML-RT M ODELS
ATM whose model is illustrated in Figure 1. It contains two
communicating capsules called UserInterface and Function- Our approach to compare pairs of U ML -RT models is illus-
alCore, each one containing a state machine modeling part trated in Figure 4. The comparison first requires the U ML -RT
of a transaction validation behavior of an ATM: the user models to be expressed in a formal specification language.
interface models some user interactions with the ATM, and With this goal, we wrote an automatic translation from the
the functional core describes a simplified representation of U ML -RT models into L NT formal models using ATL [17]
the validation process of the ATM. The capsules exchange (ATLAS Transformation Language). This step consists of an
messages through a port, which will trigger state transitions M2M (model-to-model) transformation, and both the source
in the corresponding state machine. and the target model should conform to their respective
The state machine of the FunctionalCore is in the state Idle metamodels.
until a card has been inserted in the ATM (which is detected
by the user interface). It triggers the transition to the Validating
Eclipse Platform
state, and back to the Idle state. On the UserInterface side, the
LNT
state machine alternates between the Waiting for validation UML
Metamodel Metamodel
(XText)
state and the Done state, according to the messages received
from the functional core.
UML-RT model 1 ATL M
Suppose that developers now want to add more detail to (Papyrus-RT) program
Formal model 1
(LNT)
(SVL)
this abstract model by explaining what the complex states
Equivalence
Validating and Waiting for validation are, and they produce Checking
(CADP)
a new model (Figure 3). In the UserInterface’s state machine,
the Waiting for card validation state is activated once a card UML-RT model 2 ATL Formal model 2
(Papyrus-RT) (SVL) H
program (LNT)
is inserted in the ATM, staying in this state until the card
has been validated by the functional core. Next, the Wait-
LNT
ing for code validation state becomes active, followed by the UML Metamodel
Metamodel (XText)
Waiting for transaction validation state once the code has
been validated. Once the transaction has been validated, the
state machine transits to the Done state, and returns to the Fig. 4. Equivalence checking of UML-RT models
From the formal models, LTSs are automatically generated TABLE I
(i.e., the graphs M and H in Figure 4), which are compared F ROM STRUCTURAL ELEMENTS OF UML-RT TO LNT
with each other using equivalence checking. Finally, the results U ML -RT L NT
of the comparison can be used to modify the original U ML -RT capsule module
models. For instance, if the models are said non-equivalent, state machine process
an counter-example is generated by the tool. This counter- connector channel
example identifies why the models are not equivalent, which protocol type, channel type
may help to identify anomalies in the U ML -RT models.
A transformation from (part of) U ML -RT into L NT, and a
specification of the L NT metamodel were implemented in the hidden elements and to focus on the remaining parts of the
context of this work. models during the analysis.
The summary state pattern is implemented in this work
A. LNT Metamodel
using the abstraction technique called Omission, introduced
As illustrated in Figure 4, the U ML -RT models are con- in [21]. In this abstraction technique, transitions can be tagged
forming to the U ML metamodel, whereas for the target model, with a special label τ in a state machine, allowing the
no metamodel is currently available for the L NT models to equivalence verification to bypass these transitions during the
be conform with. We specified in XText [7] a subset of the analysis.
L NT language grammar. As a result, we can assure that the
generated L NT specification is conform to its grammar. C. Transforming UML-RT into LNT
The ATL transformations from U ML -RT to L NT cover a
B. Modeling the Glass State subset of both languages. Table I illustrates how the main
In this work we focus on the summary state abstraction structural concepts of U ML -RT are mapped into elements of
pattern [28] (cf. Section II-B). This pattern introduces the the L NT language. A capsule in U ML -RT becomes a module in
concept of glass state, a state containing some states and L NT, and a state machine becomes a process. A state machine
transitions in the refined version of the model. Our approach in U ML -RT describes the behavioral part of the model, and a
allows one to tag some elements in the U ML -RT diagrams process in L NT mainly describes the behavior of the modeled
(states and transitions of the state machine), in order to identify system. Connectors linking U ML -RT capsules are translated
the elements added in the model, and to allow verification that into L NT channels through which processes can communicate.
the remaining part of the detailed model behaves exactly as Since channels in L NT are typed (to indicate which kind of
the abstract version of the model. value is exchanged in the channel), protocols in U ML -RT are
We use U ML stereotypes in order to identify in the detailed translated into regular types and channel types in L NT. Regular
version of the U ML -RT models the states and transitions types allow variables which will receive the messages sent to
which compose the glass state. Stereotype is a U ML concept the channel to be declared.
that permits extending the semantics of U ML to a particular U ML -RT and L NT share some characteristics regarding the
domain. Equations 1 and 2 illustrate the idea. The abstract behavioral modeling of systems. In U ML -RT each capsule
version of the U ML -RT model MU M LRTAbs is translated into evolves independently and concurrently, exchanging messages
a L NT model MLN T using an ATL program P (Equation 1). with each other from time to time through connectors linking
For the detailed version of the model (Equation 2), the the capsules’ ports. On the other hand, L NT was designed
elements of the glass state are first annotated in the model to model asynchronous concurrent systems: systems whose
HU M LRTRef using the hidden stereotype. Then, this annotated components may operate at different speeds, without a global
model HU M LRTAbs is translated into another model HLN T clock to synchronize them [4]. These processes exchange
using the same ATL program P . Finally, the equivalence messages with each other from time to time through channels.
checker is used to verify equivalence between MLN T and In order to translate U ML -RT into L NT, U ML -RT capsules
HLN T . linked by a connector are translated into L NT by processes
whose executions are put in parallel by means of the par-
P
allel composition operator par / end par of L NT. This
MU M LRTAbs −
→ MLN T (1) operator allows one to compose and execute processes in
annotations
HU M LRTRef −−−−−−−−→ HU M LRTAbs −
P
→ HLN T (2) parallel, and to define through which channel the processes
communicate.
Figure 3 illustrates the use of the hidden stereotype to tag For the ATM example, the two capsules UserInterface
the states and transitions which compose the glass state in the and FunctionalCore (linked by a connector) are expressed
detailed version of the ATM model. When the ATL program in L NT by the parallel composition of two processes:
generates the L NT model HLN T from this annotated U ML -RT userinterfacesm and functionalcoresm (Figure 5),
model HU M LRTAbs , these annotated elements will generate corresponding to the state machines of the U ML -RT capsules
special labels in the L NT specification too. This labeling will in Figure 1. These processes exchange values through the
be used afterwards by the equivalence checker to ignore these channel ATMProt_connector, of type ATMProt.
Fig. 5. Example of a parallel composition in LNT
In U ML -RT, messages received through ports can trigger
state transitions, which execute a chain of actions in the model.
A chain of actions of a transition is composed of the exit action
of the source state (if present), the action code of the transition
(if present), and the entry action of the target state (if present).
We translate chains of actions into L NT as if-then-else
statements for each state of the state machine (lines 10-27 of
Figure 6) following the template illustrated in Listing 1. First
the transition chain of actions of the initial pseudo state is en-
coded, followed by an update of a currentState variable, Fig. 6. State machine coding in LNT
which keeps track of the current state of the state machine
(lines 1-3 in Listing 1). Then an unbounded loop envelops the
other transition chain of actions of the state machine (lines the states of the state machine is declared (lines 3-6). Secondly,
4-20). According to the current state of the state machine a process implements the behavior of the state machine (lines
(lines 6-19), a series of if-then-else verifies whether the 8-29). The process is parameterized by one channel called
received message (line 5) triggers a transition in the current connector of type ATMProt (line 8), corresponding to the
state (e.g. lines 6-7), and executes the corresponding chain of connector and the port protocol of the UserInterface U ML -RT
actions (e.g. lines 8-11). capsule through which the state machine receives messages.
For this work, the action code of either the exit of a state, The process contains two variables (line 9), one to receive
the transition, or the entry of a state consists of message- messages that are sent to the connector channel (line 13),
passing actions. For instance, the sending of the message and another one to keep track of the current state of the
cardInserted through the connector connector in line state machine. Finally, the template described in Listing 1 is
10 of Figure 6. More sophisticated action codes with assign- implemented (lines 10-27).
ments or guards are out of scope of this paper and a topic for A U ML -RT state machine receives messages from capsule
future work. ports. This is translated to L NT as a non-deterministic choice
Figure 6 illustrates how the body of a state machine is operator select (lines 13-14 in Figure 6) with one channel
translated to L NT. This L NT specification corresponds to the called connector (since on the example the capsule has only
UserInterface state machine of the detailed version of the ATM one port). This operator allows the process to communicate
example (Figure 3). First, an enumerated type containing all with other processes which synchronize on the same channel,
and to receive messages in the variable ATMProt_var.
We acknowledge that ideally it would be good to prove
Listing 1. Template of transition chain of actions the correctness of the translation. However, this is outside the
1 e x e c u t e a c t i o n code of e x i t t r a n s . of i n i t i a l s t a t e scope of this work. Instead, we rely on extensive testing and
2 execute entry a c t i o n of stateA manual inspection.
3 c u r r e n t S t a t e := stateA
4 s t a r t loop Such formal specification of a U ML -RT model behavior can
5 r e c e i v e message t h r o u g h a c h a n n e l
6 i f currentState = stateA
also have other purposes such as a better understanding of the
7 i f messageReceiv t r i g g e r s t r a n s i t i o n A of stateA semantics of U ML -RT, which is useful for instance to teach
8 execute e x i t a c t i o n of stateA
9 e x e c u t e a c t i o n code of t r a n s i t i o n A
the language.
10 execute entry a c t i o n of t a r g e t stateB
11 c u r r e n t S t a t e := s t a t e B
12 e l s i f messageReceiv t r i g g e r s transB of stateA D. Hiding Elements in the Model
13 execute e x i t a c t i o n of stateA
14 e x e c u t e a c t i o n code of t r a n s B When the U ML -RT model is translated into L NT, its hidden
15 execute entry a c t i o n of t a r g e t stateC
16 c u r r e n t S t a t e := s t a t e C
elements (e.g., Figure 3) are also labeled in the L NT model
17 elsif ... with a tag called hidden. Such information is transmitted to
18 e l s i f currentState = stateB
19 i f messageReceiv . . .
the LTSs automatically generated from the formal models, and
20 end l o o p an S VL [11] (Script Verification Language) program is used to
tag the “hidden”-labeled transitions with the special label τ ,
allowing branching bisimulation equivalence to take this into TABLE II
account when comparing the models. C URRENT STATE OF THE FRAMEWORK
V. T OOL S UPPORT Description #loc Details
L NT XText grammar 243 27 rules
Figure 4 also illustrates the languages and tools used in our
ATL program 565 18 rules, 11 helpers
approach. We used Papyrus-RT1 [24] for creating the U ML -RT
S VL program 8 1 rule
models. Papyrus-RT is a domain-specific modeling language
tool based on Papyrus, an Eclipse-based environment for
U ML. Papyrus-RT provides an implementation of the U ML -RT equivalent but smaller one. In practice, bigger models can be
modeling language, together with editors, code generator for handled, so that one can create more realistic models.
C++, and a run-time system. In this work, the B ISIMULATOR5 [20] and BCG CMP6
The translation of the U ML -RT models into the formal equivalence checkers, and the O CIS7 simulator (Open/Caesar
model was done using an program written in ATL2 [17], a Interactive Simulator) are used, the last one for step-by-step
model transformation language and toolkit developed on top simulation with backtracking. Although L NT is the main input
of the Eclipse platform, which provides ways to produce a set language of C ADP, the tool supports other input languages
of target models from a set of source models. Sharing both a such as S VL8 [11] (Script Verification Language). S VL offers
declarative and an imperative syntax, an ATL transformation means to describe operations over LTSs, which are difficult to
program is composed of rules that define how source model perform by hand on large LTSs. It can be seen as a process
elements are matched and navigated to create and initialize calculus extended with operations on LTSs, e.g., minimiza-
the elements of the target models [8]. tion (also called reduction), abstraction, comparison, deadlock
A grammar of the L NT language was partially defined using detection, as well as orchestration of calls to the C ADP tools.
XText3 [7], a framework for development of programming The creation of the U ML -RT models, the transformation
languages, allowing one to define languages by specifying into the formal model, and the editing of the L NT formal
its grammar. As a result, XText provides an infrastructure model provided by the XText grammar are integrated into the
including parser, linker, typechecker, compiler, and editing Eclipse platform. This provides a means to build a bridge be-
support for Eclipse, providing a fully featured, customizable tween the formal verification tool C ADP and the model-driven
Eclipse-based IDE. Once the grammar of a language has been engineering tool Papyrus-RT, allowing the MDE community
defined with XText, Eclipse can be used as a smart editor to benefit from the analyses provided by formal methods tools.
for the language, providing the developer with many features Table II illustrates the current state of our verification
such as syntax highlighting, content-assist, auto-completion, framework. The XText grammar covers a subset of the L NT
folding, and jump-to-declaration [7]. One of the benefits of language, and the ATL program covers some elements of
our approach is that Eclipse can now be used as an editor for U ML -RT. Finally, the S VL program performs one single
L NT specifications. transformation in the LTS: hiding the transitions tagged with
C ADP4 [13] (Construction and Analysis of Distributed Pro- the hidden label.
cesses) is the formal verification toolbox we used. The choice
of the toolbox was mainly motivated by its maturity, contin- VI. VALIDATION
uous evolution, support, and the numerous tools available. We use this approach to analyze both the abstract and
C ADP is a toolbox for verifying asynchronous concurrent detailed versions of the ATM described in this paper. Both
systems: systems whose components may operate at different models are created in Papyrus-RT, then the glass state is
speeds, without a global clock to synchronize them. Such identified in the detailed model using the hidden stereotype (cf.
components are described by modules, and they communicate Figure 3). The ATL transformations generate one L NT model
through channels. C ADP implements several kinds of analysis: for each version of the ATM, with the information about the
model checking, equivalence checking, reachability analysis, hidden elements in them. Then, the S VL program hides the
on-the-fly verification, simulation, compositional verification, elements that are to be hidden in the generated LTSs. Finally,
distributed verification, static analysis, etc. It contains tools to the LTSs of the models are compared with each other using
create a graph-representation from the formal model (LTS), the equivalence checker of C ADP.
and the reasoning is performed over this graph. The more Specifically, branching bisimulation is used to check
complex the system under evaluation is, the larger its graph whether the abstract version of the model and the detailed
will be. C ADP handle large graphs using different techniques, one (tagged with hidden elements) are equivalent. The verifi-
such as compositional verification [12]. This technique handle cation shows that the two models are branching bisimulation
state-space explosion by creating an equivalent graph for equivalent, which means that the detailed version of the ATM
each component of the model, replacing a state space by an model behaves exactly like its abstract version, in the sense of
1 http://www.eclipse.org/papyrus-rt/ 5 http://cadp.inria.fr/man/bisimulator.html
2 http://www.eclipse.org/atl/ 6 http://cadp.inria.fr/man/bcg cmp.html
3 http://www.eclipse.org/Xtext 7 http://cadp.inria.fr/man/ocis.html
4 http://cadp.inria.fr 8 http://cadp.inria.fr/man/svl.html
TABLE III with the behavior of the system. Finally, TURTLE [3] (Timed
R ESULTS - SOME FIGURES U ML and RT-LOTOS Environment) is a U ML 1.5 profile
Model #loc Details
dedicated to the modeling and formal verification of real-
U ML -RT (abstract) - 3 capsules, 2 state machines,
time systems. Its main strength lies on its formal semantics
6 states, 6 transitions defined in a variation of L OTOS: RT-LOTOS. However, it does
U ML -RT (detailed) - 3 capsules, 2 state machines, not seem that the approach has been applied to equivalence
10 states, 10 transitions verification either.
L NT (abstract) 78 3 modules, 3 processes, 4 types In TTool [2] (the Turtle Toolkit), U ML models may be
L NT (detailed) 98 3 modules, 3 processes, 4 types automatically transformed into a L OTOS specification, in order
to evaluate properties of the system by model checking.
TTool is an open-source toolkit that supports several U ML2
branching bisimulation equivalence relation. In other words, / SysML profiles, including TURTLE and DIPLODOCUS.
the modifications done to the original model did not change Alternatively, CTTool [1] can generate L OTOS specifications
its behavior (disregarding its hidden elements and focusing on that implement a (synchronous) semantics of U ML2 compo-
the observable behavior of the models), the new version is a nent diagrams and state-machines, and analyze this L OTOS
refinement of the previous one, and the pattern used to refine code with C ADP. CTTool provides a number of menus for
the model is the summary state pattern. controlling the C ADP functions. However, the approach mainly
Table III illustrates the size of both the source model and the focuses on distributed components, while our work focuses on
generated target models of the ATM example, and the number real-time systems, and targets the L NT language. Another tool-
of lines of code generated in L NT. supported approach is provided in [31], which also uses ATL
to translate U ML -RT into a formal notation, here, functional
VII. R ELATED W ORK finite state machines. However, the focus of the formal analysis
Several approaches [1]–[3], [5], [6], [18], [19], [25], [26], is on symbolic execution and model checking.
[31] have been proposed to analyze U ML or U ML -RT models In summary, the advantage of our work compared with the
using formal methods. Some approaches [5], [6], [25], [26] previous work is that our approach benefits from equivalence
are partially similar to the one presented in this paper. Other checking to compare U ML -RT models and to verify behavior-
approaches are based on U ML profiles [3], [18], [19], or are preserving refinement between models, with the ultimate goal
supported by different tools [1], [2], [31]. of providing better support to MDE developers. Besides, while
Similar to the Eclipse-based editor for L NT we propose previous work mainly targets the L OTOS language, we cover
in this paper (as a result of the XText grammar for L NT), the L NT language and provide a syntax-highlighting Eclipse
an Eclipse-based editor for L OTOS is proposed in [5]. Even editor for L NT developers.
though L OTOS and L NT share some constructs, since L NT is
derived from E-L OTOS which enhances L OTOS, an editor for VIII. C ONCLUSION
L OTOS would not be entirely suitable for a L NT specification. In this paper we propose an approach to support model
The transformation from U ML -RT to L NT presented in this refinement, i.e., the process of gradually adding details to the
paper is inspired by some of the ideas presented in [6], [25], model in an incremental development. Our approach provides
[26]. In [6] the authors present a translation from U ML -RT to a framework to verify whether this process preserves the model
CSP (Communicating Sequential Processes), a process algebra behavior. With this goal, the initial model and its detailed
formalism which shares some constructs with L NT such as version are first translated into two formal models, and later
the representation of system behavior by processes. This work compared with each other using equivalence checking.
inspired our own translation to L NT in some aspects; however, The contributions of the paper are: (a) the use of equivalence
our work is specific to L NT. On the other hand, in [26] checking to support the verification of behavioral-preserving
(resp [25]), the formal semantics of U ML -RT is defined using refinement in the MDE context; (b) an automatic translation
the OhCircus (resp kiltera) formalism, which helped us from U ML -RT into the L NT formal language, which relieves
to better understand the semantics of U ML -RT before mapping practitioners from having to be familiar with the formal
some of its elements into L NT. language; (c) the implementation of the summary state pattern,
Closer to our work, AVATAR [18] is a SysML environment which is a first step to automatize the verification of the pattern
defined to take into account both security and safety properties catalog proposed in [28]; (d) the integration of Papyrus-RT
in graphical models, and to automatically prove both kinds (an MDE tool) with C ADP (a formal verification tool), making
of properties from the system models. It does not cover, formal methods more accessible to non-experts in the domain;
however, equivalence verification of models. Alternatively, and finally (e) the approach is tool supported.
DIPLODOCUS [19] is a U ML profile intended for the mod- The approach has been validated by the application in
eling and the formal verification of real-time and embedded two case studies: First, in a PingPong model, in which two
applications. However, DIPLODOCUS mainly focuses on im- capsules (Pinger and Ponger) exchange messages with each
plementing architectural elements (e.g., CPUs, bus, memories) other. Secondly, in the ATM example described in this paper,
of the embedded applications, while our concern is mainly in which the summary state pattern has been implemented and
an abstract and a detailed versions of the model are compared [14] P. Hallinger, D. P. Crandall, and D. N. F. Seong. Systems Think-
with each other. Equivalence between the models has been ing/Systems Changing & A Computer Simulation for Learning How to
Make School Ssmarter. Advances in Research and Theories of School
shown, which means that the detailed version of the model is Management and Educational Policy, 1(4):15–24, 2000.
a refinement of the abstract one. [15] ISO/IEC. Lotos — a formal description technique based on the temporal
We plan to improve the readability of the counter exam- ordering of observational behaviour. Draft International Standard 8807,
International Organization for Standardization — Information Process-
ples in case of non-equivalent models, since these counter ing Systems — Open Systems Interconnection, Geneva, July 1987.
examples are expressed as states and transitions of the formal [16] ISO/IEC. Enhancements to LOTOS (E-LOTOS). International Standard
specification, making it hard to identify to which states and 15437:2001, International Organization for Standardization — Informa-
tion Technology, Geneva, Sept. 2001.
transitions they correspond in the original U ML -RT models. [17] F. Jouault and I. Kurtev. Transforming models with atl. In Proceedings
We also plan to investigate the potential use of the simulation of the 2005 International Conference on Satellite Events at the MoDELS,
tools of C ADP to simulate U ML -RT models. Besides, a plugin MoDELS’05, pages 128–138, Berlin, Heidelberg, 2006. Springer-Verlag.
[18] D. Knorreck, L. Apvrille, and P. de Saqui-Sannes. TEPE: A SysML Lan-
could be developed to invoke the C ADP tools directly from guage for Time-constrained Property Modeling and Formal Verification.
Eclipse. C ADP provides both a graphical user interface and a SIGSOFT Softw. Eng. Notes, 36(1):1–8, 2011.
command line interface that can be easily integrated within [19] D. Knorreck, L. Apvrille, and R. Pacalet. Formal system-level design
space exploration. Concurrency and Computation: Practice and Expe-
Eclipse. Finally, a natural improvement would be to enlarge rience, 25(2):250–264, 2013.
the coverage of the U ML -RT language, and to implement [20] R. Mateescu and E. Oudot. Bisimulator 2.0: An on-the-fly equivalence
other patterns of the catalog in [28]. For this, enhancements checker based on boolean equation systems. In Proceedings of the 6th
ACM-IEEE International Conference on Formal Methods and Models
in the L NT grammar and in the ATL transformations would for Codesign MEMOCODE’2008 (Anaheim, CA, USA), pages 73–74.
be necessary. IEEE Computer Society Press, June 2008.
[21] R. Oliveira, S. Dupuy-Chessa, and G. Calvary. Equivalence Checking
ACKNOWLEDGMENT for Comparing User Interfaces. In EICS’15, pages 266–275, New York,
USA, 2015. ACM.
The authors would like to thank Hubert Garavel, researcher [22] D. Park. Concurrency and Automata on Infinite Sequences. In GITCS,
at INRIA Rhône-Alpes, for his support and advice during the pages 167–183. Springer-Verlag, 1981.
[23] J. L. Peterson. Petri Net Theory and the Modeling of Systems. Prentice
development of this work Hall PTR, Upper Saddle River, NJ, USA, 1981.
[24] E. Posse. Papyrusrt: Modelling and code generation (invited presenta-
R EFERENCES tion). In Proceedings of the International Workshop on Open Source
[1] S. Ahumada, L. Apvrille, A. Cansado, E. Madelaine, E. Salageanu, et al. Software for Model Driven Engineering co-located with (MODELS
Specifying Fractal and GCM components with UML. In SCCC’07, 2015), Ottawa, Canada, September 29, 2015., pages 54–63, 2015.
pages 53–62. IEEE, 2007. [25] E. Posse and J. Dingel. An executable formal semantics for UML-RT.
[2] L. Apvrille. TTool, an open-source toolkit for the modeling and Software & Systems Modeling, 15(1):179–217, 2016.
verification of embedded system. http://ttool.telecom-paristech.fr/, 2005. [26] R. Ramos, A. Sampaio, and A. Mota. Rigorous development with UML-
[Online; accessed 22-January-2017]. RT. Master’s thesis, Federal University of Pernambuco, 2005.
[3] L. Apvrille, J.-P. Courtiat, C. Lohr, and P. de Saqui-Sannes. Turtle: A [27] B. Selic. Using UML for modeling complex real-time systems. In
real-time uml profile supported by a formal validation toolkit. IEEE LCTES’98, pages 250–260. Springer, 1998.
transactions on Software Engineering, 30(7):473–487, 2004. [28] B. Selic. A short catalogue of abstraction patterns for model-based
[4] D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, C. McKinty, software engineering. Int. J. Software and Informatics, 5(1-2):313–334,
V. Powazny, F. Lang, W. Serwe, and G. Smeding. Reference Manual 2011.
of the LNT to LOTOS Translator (Version 6.1). INRIA/VASY and [29] B. Selic. What will it take? A view on adoption of model-based methods
INRIA/CONVECS, 131 pages, 2014. in practice. Software and System Modeling, 11(4):513–526, 2012.
[5] G. De Ruvo and A. Santone. An Eclipse-based Editor to Support LOTOS [30] R. J. van Glabbeek and W. P. Weijland. Branching Time and Abstraction
Newcomers. In WETICE’14, pages 372–377, 2014. in Bisimulation Semantics. Journal of the ACM, pages 555–600, 1996.
[6] G. Engels, R. Heckel, J. M. Küster, and L. Groenewegen. Consistency- [31] K. Zurowska and J. Dingel. A customizable execution engine for models
preserving model evolution through transformations. In UML’02, pages of embedded systems. In BM-FA 2009-2014, Revised Selected Papers,
212–226, London, UK, 2002. Springer-Verlag. pages 82–110, 2014.
[7] M. Eysholdt and H. Behrens. Xtext: Implement your language faster
than the quick and dirty way. In Proceedings of the ACM International
Conference Companion on Object Oriented Programming Systems Lan-
guages and Applications Companion, OOPSLA ’10, pages 307–309,
New York, NY, USA, 2010. ACM.
[8] T. E. Foundation. ATL - a model transformation technology. http:
//www.eclipse.org/atl/, 2009. [Online; accessed 20-January-2017].
[9] R. France and B. Rumpe. Model-driven development of complex
software: A research roadmap. In 2007 Future of Software Engineering,
FOSE ’07, pages 37–54, Washington, DC, USA, 2007. IEEE Computer
Society.
[10] H. Garavel. Revisiting sequential composition in process calculi. Journal
of Logical and Algebraic Methods in Programming, 2015.
[11] H. Garavel and F. Lang. SVL: A Scripting Language for Compositional
Verification, pages 377–392. Springer US, Boston, MA, 2002.
[12] H. Garavel, F. Lang, and R. Mateescu. Compositional verification of
asynchronous concurrent systems using cadp. Acta Informatica, pages
1–56, 2015.
[13] H. Garavel, F. Lang, R. Mateescu, and W. Serwe. CADP 2011: A Tool-
box for the Construction and Analysis of Distributed Processes. Interna-
tional Journal on Software Tools for Technology Transfer, 15(2):89–107,
2013.