Information Technology Reference
In-Depth Information
Fig. 5.
Illustration of the verification strategy
to the xUML level, where the model can be simulated - as opposed to formally
verified, as we aim to achieve in our work.
We use model transformation technology to implement every transition be-
tween levels of the strategy. At its most basic form, model transformation consists
of defining transformation rules that are executed in order to translate a model
A (conforming to a given meta-model) to a new model B (which conforms to
another meta-model). In the verification strategy, two different types of model
transformation techniques found in Epsilon are used: model-to-model (ETL) and
model-to-text (EGL).
For translating an xUML model to a target input language, we firstly define
a meta-model for the target language. Secondly, we specify transformation rules
for populating the target model (using the elements of the xUML model), which
must conform to the meta-model of the target language. We show how this
is done in terms of the PROMELA language in Section 5. The same should
happen when translating the counter-examples from the verification level back
to the xUML level. Although, in this case we can potentially reuse the already
defined meta-models for verification and xUML.
4 Translation of xUML into PROMELA
In this section we describe how the xUML constructs are translated to PRO-
MELA. The translation is divided in two different parts. The first describes the
translation of the class diagrams and state machines that compose the objects.
Then, in Subsection 4.2 we show the translation of the initial scenario of the
system, where objects are created and references between these objects are set.
4.1 Class Diagrams, State Machines and Objects
In the xUML model every class diagram has an associated state machine, al-
though only objects (the basic computation units) are used in the execution
