The Use of Model Transformation in the INESS Project - Formal Methods for Components and Objects - page 151

INESS experts have been using the Cassandra tool to analyse the xUML mod-
els via simulation. We have taken the behaviour implemented by this tool as the
operational semantics for the execution of the model. Cassandra imposes some
important constraints. Firstly, (a) even though after -transitions are possible in
the model, there is no notion of progressive increase of time during simula-
tion. During simulation, if two transitions are enabled (and one of them is an
after -transition), the system can choose (nondeterministically) which one to ex-
ecute. Secondly, (b) an enabled change -transition will always be executed, even
if other transitions are enabled. This means that, if the system still has an active
change -transition, it will be processed before any attempt to handle other events,
like an arriving signal. Thirdly, (c) the same signal arriving in a state machine
can generate different transitions (if they are enabled) in different concurrent
regions.
Continuing, Fig. 3 shows an example scenario for the Micro model specified in
the xUML action language. The same scenario is represented by an example of
a Track Layout diagram in Fig. 4. The Track Layout is a closer abstraction for
railway engineers. It effectively has an one-to-one correspondence to the xUML
model. Later, in Section 4 we describe the verification strategy used in the proj-
ect, which relates different levels of abstraction (from Track Layout down to
verification code).

create T1 from track by track; 1

create T2 from track by track;

2

create T3 from track by track;

3

create S1 from signal by signal;

4

create P1 from point by point;

5

create R1 from route by route; 6

create R2 from route by route;

7

link R1 via route with T1 via tracks;

8

link R1 via route with T3 via tracks;

9

link R1 via route with P1 via left_points;

10

link R1 via route with S1 via entry_signal; 11

link R2 via route with T1 via tracks;

12

link R2 via route with T2 via tracks;

13

link R2 via route with P1 via right_points;

14

link R2 via route with S1 via entry_signal;

15

Fig. 3. Micro model - scenario in the xUML action grammar

For specifying the xUML models of railway signalling systems, we have been
using a modified version of the Papyrus UML modelling tool [21], an open-source
tool based on Eclipse. The use of a homogeneous platform, in this case Eclipse,
for modelling and developing the transformation (with Epsilon), makes it easier
to provide one integrated tool. A key element of this modified version is that
we have integrated it with another Eclipse plugin, called EMFText [23], which
enables us to define an action grammar and automatically parse this grammar
from code to a model. This approach facilitates the translation between models,
since the xUML action grammar can be viewed as a model with well-defined
constraints, which is also part of the UML model. Section 5 provides more details
about our current xUML action grammar.