Abstract
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.
Original language | English |
---|---|
Title of host publication | Modeling, Development and Verification of Adaptive Systems |
Editors | Radu Calinescu, Ethan Jackson |
Place of Publication | Redmond, Washington, USA |
Publisher | Microsoft Research |
Publication date | 2010 |
Pages | 101-111 |
Publication status | Published - 2010 |
Event | 16th Monterey Workshop : Modelling, Development and Verification of Adaptive Systems: the Grand Challenge for Robust Software - Microsoft Research, Redmond, United States Duration: 31 Mar 2010 → 2 Apr 2010 Conference number: 16 |
Conference
Conference | 16th Monterey Workshop : Modelling, Development and Verification of Adaptive Systems |
---|---|
Number | 16 |
Location | Microsoft Research |
Country/Territory | United States |
City | Redmond |
Period | 31/03/2010 → 02/04/2010 |
Bibliographical note
Invited paper.Keywords
- software engineering, domain-specific language, formal methods, verification, railway control systems, relay interlocking systems, railways