Information Technology Reference
In-Depth Information
-
A translation of xUML models of railway signalling systems to the PRO-
MELA language, used as input by the SPIN model-checker [6].
-
The implementation of an automated translation of this definition, using the
Epsilon tool-set.
This work forms the basis for automating future translations, defined by us and
our University partners, from xUML to different model-checking input languages.
Our idea is to reuse as much as possible of this work,
e.g.
, transformation rules
and meta-models, in future translations.
This paper is structured as follows. The next section provides background
material on the behaviour of the xUML models we are working with (along
with a very simple example of a railway signalling system), basic features of the
PROMELA language, an overview of the Epsilon tool-set, and related work. In
Section 3, we explain the verification strategy for xUML models. The definition of
a translation of xUML models to PROMELA is described in Section 4. Section 5
details the implementation of this translation using the Epsilon tool-set. Finally,
Section 6 presents closing remarks and future work.
2 Background
2.1 xUML Models of Railway Signalling Systems
The Executable UML (xUML) language augments a subset of UML with an
action language. INESS experts have been using the tool Cassandra [10], a plug-
in for the UML modelling tool Artisan Studio [2], to model railway signalling
systems and simulate their execution. The Cassandra tool defines its own action
language. In our work, we follow Cassandra's action language, since our intention
in the project is to provide experts with the possibility of formally analysing their
current railway signalling system models.
The xUML models used to describe railway signalling systems in INESS are
composed of class diagrams and states machines. Every class diagram has an
associated state machine that describes the behaviour of the class once instan-
tiated (the object). Some characteristics of the classes include the use of integer
attributes and derived attributes, which can have a very complex behaviour.
Amongst other features, the action language is used to send messages between
objects, create objects and set references. To illustrate the xUML models we are
dealing with, we present some parts of a very small interlocking example, which
we call the Micro model, provided by INESS partners.
Fig. 1 shows the class diagram of the Micro model, which is composed of six
different classes. In addition to inheritance and the use of references in the mod-
els, we also have integer attributes, like the
describedinFig.1.Inparticular,
a class called
application
, which does not reference any other classes, is specified
to represent an initial scenario for executing the model.
Fig. 2 depicts the state machine for the
id
class. State machines can only
have initial and normal states. Moreover, they can have concurrent regions (not
shown in this particular example) and can execute actions when entering and
route
