The Use of Model Transformation in the INESS Project

Osmar Marchi dos Santos; Jim Woodcock; Richard F. Paige; Steve King

doi:10.1007/978-3-642-17071-3_8

The Use of Model Transformation in the INESS Project

Osmar Marchi dos Santos, Jim Woodcock, Richard F. Paige, Steve King

Computer Science

Research output: Contribution to conference › Paper › peer-review

Abstract

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.

Original language	Undefined/Unknown
Pages	147-165
DOIs	https://doi.org/10.1007/978-3-642-17071-3_8
Publication status	Published - 2009

Access to Document

10.1007/978-3-642-17071-3_8

http://dx.doi.org/10.1007/978-3-642-17071-3_8

Cite this

@conference{ceb689e8cd1e410eaebbf23132fa2358,

title = "The Use of Model Transformation in the INESS Project",

abstract = "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.",

author = "Santos, {Osmar Marchi dos} and Jim Woodcock and Paige, {Richard F.} and Steve King",

year = "2009",

doi = "10.1007/978-3-642-17071-3_8",

language = "Undefined/Unknown",

pages = "147--165",

}

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 -

The Use of Model Transformation in the INESS Project

Abstract

Access to Document

Other files and links

Cite this