Information Technology Reference
In-Depth Information
PROMELA constants, the global variables of the processes (used to represent
the states), define the translated processes and generate the initial process.
We illustrate the use of Epsilon to generate verification code in Fig. 13. This
code generates translated processes (transformed xUML objects). We translate
all the possible instances of
ProctypeDef
's (lines 2 to 22). For each instance,
we define the header of the process, with its name and its input parameters
(line 5). The global variables associated to the translated process are initialised
with the correct states in line 9. Then, we generate all the transitions for the
process (lines 12, 13, 14 and 17). The transitions are used to populate the basic
structure (shown previously, in Fig. 6) used to maintain the behaviour of the
xUML models in the PROMELA language (lines 11 to 19).
6Fin lRem rks
In this paper we presented the verification strategy for INESS, devised for
analysing xUML models of railway signalling systems, which is being currently
modelled by our Industry partners. At the core of our strategy is the use of model
transformation to facilitate the implementation and extension of the translation,
as new features (from the action language) used in the xUML models need to
be encoded in the verification tool. The strategy has three different levels of ab-
straction: (a) Track Layout level; (b) xUML level; (c) Verification level. We have
focused our efforts on implementing the automatic transformation from xUML
models down to verification code. This has been explained by exemplifying the
translation of xUML model to PROMELA verification code.
In this paper we have not shown the formal analysis of the xUML models. We
have focused on describing how model transformation can be used to automate
the translation of models. In fact, as we are currently developing a technique
to specify verification properties in terms of xUML and translate them to the
verification model, our only possibility of analysing the models is to encode
verification properties directly in SPIN. When doing that, we have analysed basic
properties of the Micro model, such as no two different routes can be active at
the same time. In terms of SPIN, this can be easily expressed as a temporal
formula stating that (in terms of the Micro model of Section 2.1) objects
R
1
and
state at the same time. During verification, false
results were obtained. Given the simplicity of the Micro Model, which is being
used as a starting example for our translations, this was an expected result.
Currently, we are starting to analyse more complex models obtained from our
partners.
As an immediate future work, we aim to complete our current ongoing work
on defining the specification of properties in terms of xUML and how to trans-
late them to the verification model. We also plan to start tackling the automatic
translation of counter-examples from the Verification level to the xUML abstrac-
tions. SPIN's counter-example result is made of a text file with the execution of
the model until the property under verification had a false result. In this case, we
can use text-to-model transformation from the counter-example file to a speci-
fied meta-model representing the model's execution. Moreover, we are starting
R
2 are never in the
active
