This paper describes a framework currently under development for modelling, simulation, and verification of relay interlocking systems as used by the Danish railways. The framework is centred around a domain-specific language (DSL) for describing such systems, and provides (1) a graphical editor for creating DSL descriptions, (2) a validator for checking that DSL descriptions are statically well-formed, (3) a graphical simulator for simulating the dynamic behaviour of relay interlocking systems, and (4) verification support for deriving and verifying safety properties of relay interlocking systems. The paper also touches upon how such aframework can be developed using the RAISE Formal Method.
|Title of host publication||Modeling, Development and Verification of Adaptive Systems|
|Editors||Radu Calinescu, Ethan Jackson|
|Place of Publication||Redmond, Washington, USA|
|Publication status||Published - 2010|
|Event||16th Monterey Workshop : Modelling, Development and Verification of Adaptive Systems: the Grand Challenge for Robust Software - Microsoft Research, Redmond, WA, USA|
Duration: 1 Jan 2010 → …
|Conference||16th Monterey Workshop : Modelling, Development and Verification of Adaptive Systems: the Grand Challenge for Robust Software|
|City||Microsoft Research, Redmond, WA, USA|
|Period||01/01/2010 → …|
Bibliographical noteInvited paper.
- software engineering, domain-specific language, formal methods, verification, railway control systems, relay interlocking systems, railways