Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems

Anne Elisabeth Haxthausen; Andreas A. Kjær; Marie Le Bliguet

doi:10.1007/978-3-642-21437-0_11

Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems

Anne Elisabeth Haxthausen, Andreas A. Kjær, Marie Le Bliguet

Technical University of Denmark

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

Abstract

This paper describes a tool for formal modelling relay interlocking systems and explains how it has been stepwise, formally developed using the RAISE method. The developed tool takes the circuit diagrams of a relay interlocking system as input and gives as result a state transition system modelling the dynamic behaviour of the interlocking system, i.e. the dynamic behaviour of the circuits depicted in the diagrams. The resulting state transition system (model) is expressed in the SAL language such that the SAL model checker can be used to model check required properties of this model of the interlocking system. The tool has been applied to the circuit diagrams of Stenstrup station in Denmark and the resulting formal model has then been model checked to satisfy a number of required safety properties.

Original language	English
Title of host publication	FM 2011: Formal Methods : 17th International Symposium on Formal Methods Limerick, Ireland, June 20-24, 2011 Proceedings
Publisher	Springer
Publication date	2011
Pages	118-132
ISBN (Print)	978-3-642-21436-3
ISBN (Electronic)	978-3-642-21437-0
DOIs	https://doi.org/10.1007/978-3-642-21437-0_11
Publication status	Published - 2011
Event	17th International Symposium on Formal Methods (FM 2011) - Limerick, Ireland Duration: 20 Jun 2011 → 24 Jun 2011 Conference number: 17

Conference

Conference	17th International Symposium on Formal Methods (FM 2011)
Number	17
Country/Territory	Ireland
City	Limerick
Period	20/06/2011 → 24/06/2011

Series	Lecture Notes in Computer Science
Number	6664
ISSN	0302-9743

Access to Document

10.1007/978-3-642-21437-0_11

http://sites.lero.ie/fm2011

OpenUrl availability

Full text

Cite this

@inproceedings{58064f795c9f421394ba3446a1821d46,

title = "Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems",

abstract = "This paper describes a tool for formal modelling relay interlocking systems and explains how it has been stepwise, formally developed using the RAISE method. The developed tool takes the circuit diagrams of a relay interlocking system as input and gives as result a state transition system modelling the dynamic behaviour of the interlocking system, i.e. the dynamic behaviour of the circuits depicted in the diagrams. The resulting state transition system (model) is expressed in the SAL language such that the SAL model checker can be used to model check required properties of this model of the interlocking system. The tool has been applied to the circuit diagrams of Stenstrup station in Denmark and the resulting formal model has then been model checked to satisfy a number of required safety properties.",

author = "Haxthausen, {Anne Elisabeth} and Kj{\ae}r, {Andreas A.} and {Le Bliguet}, Marie",

year = "2011",

doi = "10.1007/978-3-642-21437-0_11",

language = "English",

isbn = "978-3-642-21436-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

number = "6664",

pages = "118--132",

booktitle = "FM 2011: Formal Methods",

note = "17th International Symposium on Formal Methods (FM 2011), FM 2011 ; Conference date: 20-06-2011 Through 24-06-2011",

}

Haxthausen, AE, Kjær, AA & Le Bliguet, M 2011, Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems. in FM 2011: Formal Methods: 17th International Symposium on Formal Methods Limerick, Ireland, June 20-24, 2011 Proceedings. Springer, Lecture Notes in Computer Science, no. 6664, pp. 118-132, 17th International Symposium on Formal Methods (FM 2011), Limerick, Ireland, 20/06/2011. https://doi.org/10.1007/978-3-642-21437-0_11

Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems. / Haxthausen, Anne Elisabeth; Kjær, Andreas A.; Le Bliguet, Marie.
FM 2011: Formal Methods: 17th International Symposium on Formal Methods Limerick, Ireland, June 20-24, 2011 Proceedings. Springer, 2011. p. 118-132 (Lecture Notes in Computer Science; No. 6664).

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

TY - GEN

T1 - Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems

AU - Haxthausen, Anne Elisabeth

AU - Kjær, Andreas A.

AU - Le Bliguet, Marie

N1 - Conference code: 17

PY - 2011

Y1 - 2011

N2 - This paper describes a tool for formal modelling relay interlocking systems and explains how it has been stepwise, formally developed using the RAISE method. The developed tool takes the circuit diagrams of a relay interlocking system as input and gives as result a state transition system modelling the dynamic behaviour of the interlocking system, i.e. the dynamic behaviour of the circuits depicted in the diagrams. The resulting state transition system (model) is expressed in the SAL language such that the SAL model checker can be used to model check required properties of this model of the interlocking system. The tool has been applied to the circuit diagrams of Stenstrup station in Denmark and the resulting formal model has then been model checked to satisfy a number of required safety properties.

AB - This paper describes a tool for formal modelling relay interlocking systems and explains how it has been stepwise, formally developed using the RAISE method. The developed tool takes the circuit diagrams of a relay interlocking system as input and gives as result a state transition system modelling the dynamic behaviour of the interlocking system, i.e. the dynamic behaviour of the circuits depicted in the diagrams. The resulting state transition system (model) is expressed in the SAL language such that the SAL model checker can be used to model check required properties of this model of the interlocking system. The tool has been applied to the circuit diagrams of Stenstrup station in Denmark and the resulting formal model has then been model checked to satisfy a number of required safety properties.

U2 - 10.1007/978-3-642-21437-0_11

DO - 10.1007/978-3-642-21437-0_11

M3 - Article in proceedings

SN - 978-3-642-21436-3

T3 - Lecture Notes in Computer Science

SP - 118

EP - 132

BT - FM 2011: Formal Methods

PB - Springer

T2 - 17th International Symposium on Formal Methods (FM 2011)

Y2 - 20 June 2011 through 24 June 2011

ER -

Haxthausen AE, Kjær AA, Le Bliguet M. Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems. In FM 2011: Formal Methods: 17th International Symposium on Formal Methods Limerick, Ireland, June 20-24, 2011 Proceedings. Springer. 2011. p. 118-132. (Lecture Notes in Computer Science; No. 6664). doi: 10.1007/978-3-642-21437-0_11

Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this