Use of Nodel Transformation For The Formal Analysis Of Railway Interlocking Models

T. Xu; O. M. Santos; X. Ge; J. Woodcock

doi:10.2495/CR100741

Use of Nodel Transformation For The Formal Analysis Of Railway Interlocking Models

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Citation (Scopus)

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 language	English
Title of host publication	Computers in Railways XII
Subtitle of host publication	Computer System Design and Operation in the Railway and Other Transit Systems, COMPRAIL 2010
Editors	B. Ning, C. A. Brebbia
Publisher	WIT Press
Pages	815-826
Number of pages	12
Volume	114
ISBN (Print)	9781845644680
DOIs	https://doi.org/10.2495/CR100741
Publication status	Published - 2010
Externally published	Yes
Event	12th International Conference on Computer System Design and Operation in the Railways and other Transit Systems - Beijing, China Duration: 31 Aug 2010 → 2 Sep 2010 Conference number: 12

Publication series

Name	WIT Transactions on the Built Environment
Volume	114
ISSN (Print)	1743-3509

Conference

Conference	12th International Conference on Computer System Design and Operation in the Railways and other Transit Systems
Abbreviated title	COMPRAIL 2010
Country/Territory	China
City	Beijing
Period	31/08/10 → 2/09/10

Access to Document

10.2495/CR100741Licence: CC BY

Cite this

Xu, T., Santos, O. M., Ge, X., & Woodcock, J. (2010). Use of Nodel Transformation For The Formal Analysis Of Railway Interlocking Models. In B. Ning, & C. A. Brebbia (Eds.), Computers in Railways XII: Computer System Design and Operation in the Railway and Other Transit Systems, COMPRAIL 2010 (Vol. 114, pp. 815-826). (WIT Transactions on the Built Environment; Vol. 114). WIT Press. https://doi.org/10.2495/CR100741

@inproceedings{ecd6175431b04c12846be2f4f47f777e,

title = "Use of Nodel Transformation For The Formal Analysis Of Railway Interlocking Models",

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

keywords = "executable UML (xUML), formal analysis, formal languages, model driven engineering (MDE), railway interlocking systems",

author = "T. Xu and Santos, {O. M.} and X. Ge and J. Woodcock",

year = "2010",

doi = "10.2495/CR100741",

language = "English",

isbn = "9781845644680",

volume = "114",

series = "WIT Transactions on the Built Environment",

publisher = "WIT Press",

pages = "815--826",

editor = "B. Ning and Brebbia, {C. A.}",

booktitle = "Computers in Railways XII",

address = "United Kingdom",

note = "12th International Conference on Computer System Design and Operation in the Railways and other Transit Systems, COMPRAIL 2010 ; Conference date: 31-08-2010 Through 02-09-2010",

}

Xu, T, Santos, OM, Ge, X & Woodcock, J 2010, Use of Nodel Transformation For The Formal Analysis Of Railway Interlocking Models. in B Ning & CA Brebbia (eds), Computers in Railways XII: Computer System Design and Operation in the Railway and Other Transit Systems, COMPRAIL 2010. vol. 114, WIT Transactions on the Built Environment, vol. 114, WIT Press, pp. 815-826, 12th International Conference on Computer System Design and Operation in the Railways and other Transit Systems, Beijing, China, 31/08/10. https://doi.org/10.2495/CR100741

Use of Nodel Transformation For The Formal Analysis Of Railway Interlocking Models. / Xu, T.; Santos, O. M.; Ge, X. et al.

Computers in Railways XII: Computer System Design and Operation in the Railway and Other Transit Systems, COMPRAIL 2010. ed. / B. Ning; C. A. Brebbia. Vol. 114 WIT Press, 2010. p. 815-826 (WIT Transactions on the Built Environment; Vol. 114).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Use of Nodel Transformation For The Formal Analysis Of Railway Interlocking Models

AU - Xu, T.

AU - Santos, O. M.

AU - Ge, X.

AU - Woodcock, J.

N1 - Conference code: 12

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

KW - executable UML (xUML)

KW - formal analysis

KW - formal languages

KW - model driven engineering (MDE)

KW - railway interlocking systems

UR - http://www.scopus.com/inward/record.url?scp=78649399877&partnerID=8YFLogxK

U2 - 10.2495/CR100741

DO - 10.2495/CR100741

M3 - Conference contribution

AN - SCOPUS:78649399877

SN - 9781845644680

VL - 114

T3 - WIT Transactions on the Built Environment

SP - 815

EP - 826

BT - Computers in Railways XII

A2 - Ning, B.

A2 - Brebbia, C. A.

PB - WIT Press

T2 - 12th International Conference on Computer System Design and Operation in the Railways and other Transit Systems

Y2 - 31 August 2010 through 2 September 2010

ER -

Xu T, Santos OM, Ge X, Woodcock J. Use of Nodel Transformation For The Formal Analysis Of Railway Interlocking Models. In Ning B, Brebbia CA, editors, Computers in Railways XII: Computer System Design and Operation in the Railway and Other Transit Systems, COMPRAIL 2010. Vol. 114. WIT Press. 2010. p. 815-826. (WIT Transactions on the Built Environment). doi: 10.2495/CR100741

Use of Nodel Transformation For The Formal Analysis Of Railway Interlocking Models

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this