By the same authors

The Use of Model Transformation in the INESS Project

Research output: Contribution to conferencePaper

Standard

The Use of Model Transformation in the INESS Project. / Santos, Osmar Marchi dos; Woodcock, Jim; Paige, Richard F.; King, Steve.

2009. 147-165.

Research output: Contribution to conferencePaper

Harvard

Santos, OMD, Woodcock, J, Paige, RF & King, S 2009, 'The Use of Model Transformation in the INESS Project' pp. 147-165. https://doi.org/10.1007/978-3-642-17071-3_8

APA

Santos, O. M. D., Woodcock, J., Paige, R. F., & King, S. (2009). The Use of Model Transformation in the INESS Project. 147-165. https://doi.org/10.1007/978-3-642-17071-3_8

Vancouver

Santos OMD, Woodcock J, Paige RF, King S. The Use of Model Transformation in the INESS Project. 2009. https://doi.org/10.1007/978-3-642-17071-3_8

Author

Santos, Osmar Marchi dos ; Woodcock, Jim ; Paige, Richard F. ; King, Steve. / The Use of Model Transformation in the INESS Project.

Bibtex - Download

@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",

}

RIS (suitable for import to EndNote) - Download

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 -