Information Technology Reference
In-Depth Information
UML is the
de facto
language for modelling software systems in industry.
In particular, one of its profiles, Executable UML (xUML) [19], augments a
subset of UML with an action language that adds enough information to enable,
amongst other features, creating objects, establishing references and performing
operations. From the developer's viewpoint, this has the benefit of providing
means to quickly prototype the system at the modelling level, which can then
have its behaviour analysed, for instance by simulation.
INESS experts have been using xUML to model a specification of the proposed
integrated signalling system. The idea is to use the specified xUML models to
check for inconsistencies in the requirements and against core properties of the
system provided by professional railway engineers. Currently, xUML models can
be analysed only via simulation. Due to safety-critical requirements involved
in railway signalling systems, using formal verification to analyse the model is
of vital importance. Therefore, our task in the project, together with partners
from the Universities of Eindhoven, Twente and Southampton is to equip railway
experts with an automatic tool able to analyse the models formally.
Similar to most work found in the literature targeting the automatic verifica-
tion of xUML models (
e.g.
, [28,9,27]), we have focused our research on generating
code that can be used as input to a state-of-the-art model-checking tool. For this
technique to succeed in the context of the INESS project, three challenges have
to be faced:
1. The translation
1
of the xUML model to the input language of the model-
checking tool has to be automatic.
2. The specification of verification properties has to be given in terms of the
xUML model, and the translation of properties to the model-checking tool
has to be automatic and transparent.
3. It must be possible to accurately trace back the results of the analysis from
the model-checking tool (
i.e.
, success or a counter-example) to the abstrac-
tion level of the xUML model.
In order to tackle these challenges, we define a verification strategy that uses
model transformation technology to automatically and transparently generate
code from xUML models, which can then be used as input to model-checking
tools. Model transformation technology provides a major opportunity to auto-
mate all the steps necessary to achieve this task. In particular, for the trans-
formation of models, we use the Epsilon tool-set [11], based on the Eclipse
platform [25]. We take a diverse approach in our verification strategy. We fo-
cus on translating xUML models to different model-checking tools, which may
yield different and potentially better verification results under certain verification
scenarios.
In this paper, we describe the results obtained so far in the INESS project:
-
The verification strategy for the different transformations of xUML to input
languages of different model-checkers.
1
The terms translation and transformation are used interchangeably in this paper.
