Use Of Model Transformation For The Formal Analysis Of Railway Interlocking Models
Price
Free (open access)
Transaction
Volume
114
Pages
12
Page Range
815 - 826
Published
2010
Size
864 kb
Paper DOI
10.2495/CR100741
Copyright
WIT Press
Author(s)
T. Xu, O. M. Santos, X. Ge & J. Woodcock
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: railway interlocking systems, model driven engineering (MDE), executable UML (xUML), formal languages, formal analysis. 1 Introduction Railway interlocking plays a very important role in establishing high safety for train operations in a railway system, and protecting passengers and equipment from damage. Due to its life-critical application, a rigorous verification phase is
Keywords
railway interlocking systems, model driven engineering (MDE),executable UML (xUML), formal languages, formal analysis