Information Technology Reference
In-Depth Information
3 The Verification Strategy
The verification strategy of INESS consists of defining a methodology for the ver-
ification of railway signalling system models specified in xUML. Fig. 5 illustrates
this methodology, where three different levels of abstraction are presented:
1. Track Layout level: We use a Domain-Specific Language (DSL) for describing
the scenario (diagram) of railway signaling systems for verification. In the
INESS Project, the xUML language is used to specify different European rail-
way signalling systems and how they integrate together. This culminates in
the definition of a set of components that can be combined in different ways.
In this sense, the Track Layout level provides an abstraction, understood by
railway engineers, that facilitates the definition of analysis scenarios. A com-
ponent at this level provides a direct mapping to an xUML component (at
the xUML level). Moreover, we are currently looking into method to specify
verification properties at this level.
2. xUML level: This represents the xUML level used to model the integrated
railway signalling system. An important element is the xUML Library of
railway signalling components that can be put together in order to define an
analysis scenario. We focus our work on providing a verification method at
this abstraction level. Given a transformed xUML model of the desired Track
Layout, we provide transformation rules to generate a model in the target
language (used as input to a model-checking tool) integrating the model
and the encoded verification property. Although we have initial results in
translating the xUML to PROMELA (see Section 4), we are still working on
a way to express verification properties in terms of the xUML model.
3. Verification level: This level represents the target verification model, already
encoded with the desired verification properties. Once the model has been
translated, the task is to generate the verification code, which is actually
used by the model checker for the automated formal verification. After ver-
ification, it is necessary to translate the results back from the verification
level to the xUML level, so that users can view the same abstraction level
(transparency, with respect to the verification, is obtained).
Starting from the top level, the verification strategy should work with the def-
inition of a Track Layout scenario. This is mapped to an xUML model. The
xUML model is then translated to the input language of a model checking tool
(Target Model), being analysed (Verification Code and Results) and have its re-
sults transformed back to the abstractions found in the Track Layout (Counter
Examples chain from Verification to Track Layout levels).
Note that, in our current work, we have not focused on the Track Layout
level, since it provides a direct and straightforward mapping of one-to-one to the
xUML level. In other words, the Track Layout level only facilitates transparency
of verification, since railway engineers do not have to even understand the xUML
model in order to use the verification facilities. However, one of our industrial
partners has already successfully defined a Track Layout level and mapped it
