Use of model transformation for the formal analysis of railway interlocking models

T. Xu*, O. M. Santos, X. Ge, J. Woodcock

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Model transformation is at the heart of Model-Driven Engineering (MDE). In MDE, the system model is specified using a modelling language, such as UML (Unified Modelling Language) or a DSL (Domain-Specific Language). Once a model is specified, executable code for a computing platform can be automatically generated by means of model transformation (code generation). Besides the support for incremental model development, MDE also enables the formal verification of system properties. In the context of safety-critical systems, such as railway interlockings, the system model (e.g., specified in terms of UML) can be translated to a formal (mathematical) language more amendable to rigorous analysis. This paper presents a model transformation that takes a railway interlocking model (specified in Executable UML (xUML)) as input and outputs a formal model that can be mathematically analysed. This can potentially bridge the gap between well-known modelling languages (such as xUML) and formal languages, which facilitates the systematic development of safety-critical systems in terms of MDE. A small xUML railway interlocking model is used to illustrate the proposed method.

Original languageEnglish
Title of host publicationComputers in Railways XII, COMPRAIL 2010
Pages815-826
Number of pages12
DOIs
Publication statusPublished - 2010
Event12th International Conference on Computer System Design and Operation in the Railways and other Transit Systems, COMPRAIL 2010 - Beijing, China
Duration: 31 Aug 20102 Sep 2010

Publication series

NameWIT Transactions on the Built Environment
Volume114
ISSN (Print)1743-3509

Conference

Conference12th International Conference on Computer System Design and Operation in the Railways and other Transit Systems, COMPRAIL 2010
Country/TerritoryChina
CityBeijing
Period31/08/102/09/10

Keywords

  • executable UML (xUML)
  • formal analysis
  • formal languages
  • model driven engineering (MDE)
  • railway interlocking systems

Cite this