Executable and well-de ned models are a cornerstone of model driven engineering. We are currently working on a transformation chain from UML models to formal veri cation tools. In the context of the UML language, the fUML and Alf speci cations o er a standardized way for the semantics of the basic model elements and a textual speci cation language. Open source modeling tools started to adapt these speci cations. However, their support is of varying degree. This paper summarizes our experiences with the open source tools regarding fUML and Alf support, and di erent model transformation technologies in order to analyse them with formal veri cation tools.
Model driven engineering (MDE) is changing software and systems development
in di erent application domains. In MDE, models are the primary artifacts from
which other artifacts (code, deployment descriptions, etc.) are generated [
The Uni ed Modeling Language (UML) is a general purpose, widely used
modeling language used for describing the di erent aspects of software systems.
It o ers several modeling notations to express not only the structure but the
behavior of the modeled system (e.g. with state machines, activities). But UML
is criticized because of the lack of a precise de nition of the language [
Some commercial MDE tools already o er an executable variant of UML. Some of these are using fUML (e.g. No Magic's Cameo Simulation Toolkit for MagicDraw) or are using other approaches (e.g. xtUML in the BridgePoint modelling tool of Mentor Graphics). These tools are able to execute, debug and transform UML behavioral models.
Fortunately, more and more open source tools have started to include some kind of executable UML functionality, and support for fUML or Alf. However, due to the nature of open source, these developments are sometimes overlapping and redundant, some projects are not active any more, and their technology readiness level and documentation is uneven. Thus, if someone wants to engage in a UML-based MDE project the following questions naturally arise. 1. What open source tools are available for fUML and Alf? 2. What are their maturity level? 3. How can the di erent tools be connected to solve a complex problem?
We are currently working on a tool chain to provide veri cation of UML behavioral models in the communication domain by transforming them to the input of formal model checkers and back-annotating the results. The goal of the veri cation is to prove the deadlock freedom of protocols. When developing the initial prototypes, we tried to base our work on open source components for fUML or Alf. This paper primarily aims at summarizing our experience of using these open source components for model analysis purposes.
Section 2 introduces our modeling and analysis approach, then collects the fUML and Alf tools we are aware of. Section 3 details the avalilable transformation technologies, and presents our Eclipse-based transformation prototype implementation. Section 4 summarizes our experiences and some open issues with the speci cations and the tooling. 2
The goal of our project is to provide formal analysis for behavioral UML models
by transforming these models to the input languages of formal veri cation tools
(e.g. model checkers). We aim to use a combination of UML diagrams as input
to capture static and dynamic aspects. In order to facilitate the adaptation of
the tool chain to di erent back-end tools, we intend to use intermediate models
between the source engineering model and the target veri er model, which is
proposed in numerous model analysis approaches [
The goal of the fUML speci cation of the OMG is to give a precise semantic
definition for a subset of UML. This subset includes parts of the classes, behaviors,
activities and actions packages of UML Superstructure, but does not include
state machines or sequence diagrams. The standardization including
composite structures (such as components, ports...) is ongoing [
fUML Ref. Impl. L
fUMoliz lfAlf Ref. Impl. 0.4.0 APapyrus Alf Editor
contains the de nition of (1) an abstract syntax for the subset of UML Infrastructure/Superstructure, (2) an execution model for the operational semantics, (3) Java language semantic de nitions for the behavior of the elements, (4) a model library (functions for primitive types, channels), and (5) axiomatic semantics for a base UML.
The Action Language for Foundational UML (Alf) is a standardized textual language for specifying executable behavior. It can be used to extend a graphical UML model (e.g. to de ne actions or guards). However, it can also express structural model elements, thus an entire UML model can be described in a textual language. The speci cation consists of (1) an EBNF grammar for the Alf language, and (2) a modeling library for primitive types, functions and collections. UML state machines are not in fUML, thus Alf does not cover it; but Annex A of the speci cation gives an example for such a mapping.
Table 1 summarizes the tools with fUML or Alf support we are aware of. The
following is a short description of the fUML and Alf tools in Table 1.
fUML Reference Implementation [
Moka [
Moliz [
High Level UML Sequence Diag.
Error Trace fUML Simulation
Model Checking State Machine 1 ActivitySDiagram 2
AlfSModel 3
Formal Model
Alf Reference Implementation [
A model transformation (MT) de nes a mapping from a source language to a target language. Model transformations are speci ed in a language which is executed by a transformation engine on a source model to create a target model. A complex MT can be split into multiple steps to form a transformation chain.
Figure 2 shows a simple iterator example of the transformation of Step 2 and 3 described in Figure 1 with concrete syntax in the top row and model representation in the bottom row. Activity diagrams de ne guards and actions by Alf code, but the control ow is de ned by explicit transition arrows and composite nodes. First, the activity diagram is translated to full Alf code, where the actions are mapped to statements and the ow is de ned by structures (while statements). Then the Alf code is mapped to an Uppaal formal model where the statements are represented by atomic state transitions, and the control is managed by explicit edges with guard expressions.
We show how this MT problem can be solved using di erent MT approaches using the Alf-to-Uppaal transformation. We also highlight the di erences and the bene ts of the techniques from the following aspects: source model processing, target model construction, trace handling and debugging possibilities. Transformation program A rst approach to implement a MT is to create a problem speci c transformation program written in a general-purpose imperative programming language like Java. It is easy to start development without relying on any third-party MT tool. However, such MT programs are error-prone and hard to maintain resulting in a long development process.
Figure 3c shows the skeleton of an example Java transformation code, where both the source and target models are handled as arbitrary Java (EMF) objects. The source model is traversed by complex control structures, where navigation is available only through direct references (see Mark 1)in Figure 3a). The transformation code is responsible for nding the required relations in the model, i.e. possible state transitions in between Alf statements. Objects of the target EMF model are created via factory methods, attributes and references are de ned by setter methods as in common Java objects (Mark 2)). Traceability management is ad hoc, and usually implemented with temporally maps (Mark 3)). (a) Transformation program illustration
(b) Model transformation program run (c) Example Transformation program implemented in java
(d) Example model ATL transformation rules Model Transformation Tool There are several dedicated MT languages to specify transformation rules. Those rules are automatically executed by transformation engines on the source model to produce the output model. The transformation development process is scaling well with respect to the number of rules, However, there are also some constructs that are di cult to formulate in the transformation language, hard to integrate with other tools or transformation steps implemented in imperative code, and it has little debugging support.
The ATLAS Transformation Language (ATL) [
Model Queries and Functional Programs Declarative graph query frameworks
like EMF-IncQuery[
Functional approaches proved their usefulness in the implementation of data transformations. Their main advantages are 1) compact representation 2) easy extendability and 3) composability. Template based code generation and model transformation widely uses functional approaches. The Xtend language adds functional elements to Java language like lambda expressions while keeps the imperative elements. The right column of Figure 4c shows the skeletons of the transformer functions: the rst transforms a while statement, the second maps a relation condition.
Our experiences shows that a functional Xtend code using EMF-IncQuery queries is e cient for implementing model transformations. It can be used similarly to MT tools and it eliminates known navigation issues of Xtend. This approach allows the developer to 1) freely mix the two techniques (query the model from the template code, or use pure functions in a pattern), 2) directly call and debug templates and queries or 3) reuse rules by other transformations. Query Based Views as Model Transformations IncQuery patterns can be used to de ne views to represent relations of the source model in a target model. Those query based view models are automatically and incrementally maintained. Views can be used as visualisation, or as model transformation. The visualiser aids the developer to correct bugs. A trace model is automatically derived.
Figure 4d shows four example for the use of query based views, and Figure 4b illustrate it with the running example, where the matches and their images are marked with Mark 1)- Mark 4). Mark 1) de nes that each match of a Statement should be mapped to a new l Location in the Uppaal model. The trace of the mapping can be used in other rules, for example Mark 2) collects the subsequent statements from the control graph of the Alf model with the nextState pattern and creates an e edge between the images of the statements. Pattern Mark 3) gets the rst statement of the cycle body and names it to StartLoop and the edge where the loop enters called incoming. Similarly Mark 4) selects the exiting statement rst statement where the loop exits called FinishLoop, the edge is named outgoing. The model creation rules then maps the Alf loop conditions to Uppaal guard expressions and inserts it to the incoming and outgoing edges positively and negatively.
While query based views provide a restricted subclass of model transformations, this loss of generality is balanced by the fact that this class of model transformations is (source-)incremental by its nature, i.e. changes in the source model are propagated to the target model incrementally.
Summary From the above transformation approaches we choose the third one in our prototype implementation. EMF-IncQuery was used for the e cient and scalable queries of model elements. Xtend was used to map the source to the target model according to the de ned EMF-IncQuery patterns. The lessons learnt during the development are summarized in the next section. 4
This section summarizes our experiences during the development of the previously presented transformation.
Experience with fUML and Alf: { No list of tools: Although it seems trivial, but even collecting the available tools required considerable e ort. This paper provides a snapshot, but it will become outdated. As fUML and Alf is still not yet widespread, OMG could promote them by listing the tools on its website along the speci cations. { Few examples: There are few example fUML models or Alf code available.
Moreover, version and tool incompatibility further hinders the reuse of examples (e.g. a model exported in XMI could not always be loaded in an other tool, the UML speci cation changed in recent years, etc.). { Reference implementations: The fUML and Alf reference implementations are ful lling their purpose, they help to understand the speci cations. Advanced functions are not in their scope, but they provide a good starting point for tool developers. { Semantic information: Semantic information that could help the veri cation is not present in the Alf model (e.g. current compound state in a hierarchical or parallel activity). It can be added to the transformation tool as annotations. { Alf grammar: The current version of Alf grammar uses complex structures of language elements to ensure unambiguity of the language. This structure is e ectively handled by matching graph patterns during the transformation. Open issues with the tools: { In the released version of Papyrus, Alf code cannot be speci ed for the behavioral elements, thus we attached them as simple text in comment blocks. { We had to create our own (limited) Alf metamodel for the transformations as the available ones were incomplete in the pre-Luna versions of the Eclipsebased tools. { The tools would need a functionality to restrict the available elements (e.g.
an Alf language element should not be used in a certain application domain). Maturity of the tools: { Proven: the Eclipse platform and its core services (e.g. EMF, Xtext) provided a solid base for tool development. { Incubation: Although still in incubation phase, it was relatively easy to use EMF-IncQuery due to its easy-to-use tooling and examples. (Note, we consulted also with local developers of the tool). { Prototype: The fUML engines (Moka, Moliz) are working and there are some examples and documentation available. However, they are still in prototypes phase (e.g. in a simple scenario we were able to produce NullReferenceException in Moka). { Alpha: The Alf editor in Papyrus is still in active development (e.g. most of the code is in the sandbox repository, it supports only a limited part of Alf). 5
Support for the executable extensions of UML started to appear in open source modeling tools. This paper summarized these tools and our experiences with them, obtained during the development of a prototype transformation chain. Our ndings showed that advancement in the tooling is promising, but there is still a long road ahead. As a summary, the questions raised in the introduction can be answered as follows:
Acknowledgments. This work was partially supported by Ericsson Hungary.