Information Technology Reference
In-Depth Information
The Use of Model Transformation
in the INESS Project
Osmar M. dos Santos, Jim Woodcock, Richard F. Paige, and Steve King
University of York
Department of Computer Science
York, UK
{
osantos,jim,paige,king
}
@cs.york.ac.uk
Abstract.
The INESS (INtegrated European Signalling System) Proj-
ect is an effort, funded by the FP7 programme of the European Union, to
provide a common, integrated, railway signalling system within Europe.
It comprises 30 partners, including 6 railway companies. INESS experts
have been using the Executable UML (xUML) language to model the pro-
posed integrated signalling system. Because of the safety-critical aspects
of these systems, one key idea is to use formal verification techniques
to analyse the xUML models for inconsistencies in the requirements and
against core properties provided by professional railway engineers. Our
objective in the project is to equip our INESS partners with an au-
tomated tool to carry out this analysis. Therefore, we have devised a
formal verification strategy that uses model transformation technology
to automatically translate xUML models to the input language of exist-
ing, state-of-the-art, model checking tools. In this paper we describe this
formal verification strategy in more detail: we present initial results on
implementing the automatic generation of PROMELA models that can
be analysed using the SPIN model checker.
1
Introduction
INESS (INtegrated European Signalling System) [8] is an industry-focused
project funded by the FP7 programme of the European Union, comprising 30
partners, including 6 railway companies. The objective is to provide a common
railway signalling system that integrates existing European ones. The motiva-
tion is cost effectiveness: there is increasing competition from other kinds of
transport and from manufacturers outside Europe. The European Commission,
which is committed to revitalise rail transport, sees as the main obstacle to
further development the lack of infrastructure and interoperability between net-
works and systems. Signalling systems are perhaps the most significant part of
the railway infrastructure: they are essential for the performance and the safety
of train operations. Two of the objectives of INESS are to produce a common
core of validated, standardised functional requirements for future interlockings,
and to provide safety-verified test tools and techniques to enable the testing and
commissioning of future signalling applications.
