TY - CONF
T1 - The Use of Model Transformation in the INESS Project
AU - Santos, Osmar Marchi dos
AU - Woodcock, Jim
AU - Paige, Richard F.
AU - King, Steve
PY - 2009
Y1 - 2009
N2 - The INESS (INtegrated European Signalling System) Project 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 proposed 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 automated 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 existing, 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.
AB - The INESS (INtegrated European Signalling System) Project 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 proposed 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 automated 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 existing, 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.
UR - http://www.scopus.com/inward/record.url?scp=78650197015&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-17071-3_8
DO - 10.1007/978-3-642-17071-3_8
M3 - Paper
SP - 147
EP - 165
ER -