Comparing formal verification approaches of interlocking systems

Anne Elisabeth Haxthausen; Hoang Nga Nguyen; Markus Roggenbach

doi:10.1007/978-3-319-33951-1_12

Comparing formal verification approaches of interlocking systems

Anne Elisabeth Haxthausen
, Hoang Nga Nguyen
, Markus Roggenbach

Department of Applied Mathematics and Computer Science

Coventry University
Swansea University

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

864 Downloads (Orbit)

Abstract

The verification of railway interlocking systems is a challenging task, and therefore several research groups have suggested to improve this task by using formal methods, but they use different modelling and verification approaches. To advance this research, there is a need to compare these approaches. As a first step towards this, in this paper we suggest a way to compare different formal approaches for verifying designs of route-based interlocking systems and we demonstrate it on modelling and verification approaches developed within the research groups at DTU/Bremen and at Surrey/Swansea. The focus is on designs that are specified by so-called control tables. The paper can serve as a starting point for further comparative studies. The DTU/Bremen research has been funded by the RobustRailS project granted by Innovation Fund Denmark. The Surrey/Swansea research has been funded by the SafeCap and the DITTO research projects granted by EPSRC and RSSB. The authors would like to thank Linh Hong Vu for providing the benchmark of scheme plans and the drawings of the track plans.

Original language	English
Title of host publication	Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification : First International Conference, RSSRail 2016 Paris, France, June 28–30, 2016 Proceedings
Number of pages	18
Volume	9707
Publisher	Springer
Publication date	2016
Pages	160-177
ISBN (Print)	978-3-319-33950-4
ISBN (Electronic)	978-3-319-33951-1
DOIs	https://doi.org/10.1007/978-3-319-33951-1_12
Publication status	Published - 2016
Event	The International Conference on Reliability, Safety and Security of Railway Systems: Modelling, Analysis, Verification, and Certification - Espace du Centenaire, Maison de la RATP, Paris, France Duration: 28 Jun 2016 → 30 Jun 2016 Conference number: 1 https://conferences.ncl.ac.uk/rssrail/

Conference

Conference	The International Conference on Reliability, Safety and Security of Railway Systems
Number	1
Location	Espace du Centenaire, Maison de la RATP
Country/Territory	France
City	Paris
Period	28/06/2016 → 30/06/2016
Internet address	https://conferences.ncl.ac.uk/rssrail/

Series	Lecture Notes in Computer Science
ISSN	0302-9743

Keywords

Software Engineering
Logics and Meanings of Programs
Computer Communication Networks
Systems and Data Security
Mathematical Logic and Formal Languages
Artificial Intelligence (incl. Robotics)

Access to Document

10.1007/978-3-319-33951-1_12

2016Accepted author manuscript, 294 KB

OpenUrl availability

Check availability in DTU Findit

Cite this

Haxthausen, A. E., Nguyen, H. N., & Roggenbach, M. (2016). Comparing formal verification approaches of interlocking systems. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: First International Conference, RSSRail 2016 Paris, France, June 28–30, 2016 Proceedings (Vol. 9707, pp. 160-177). Springer. https://doi.org/10.1007/978-3-319-33951-1_12

Haxthausen, Anne Elisabeth ; Nguyen, Hoang Nga ; Roggenbach, Markus. / Comparing formal verification approaches of interlocking systems. Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: First International Conference, RSSRail 2016 Paris, France, June 28–30, 2016 Proceedings. Vol. 9707 Springer, 2016. pp. 160-177 (Lecture Notes in Computer Science).

@inproceedings{1be72ab90cdd4669bcc8fe39be3ebc9d,

title = "Comparing formal verification approaches of interlocking systems",

abstract = "The verification of railway interlocking systems is a challenging task, and therefore several research groups have suggested to improve this task by using formal methods, but they use different modelling and verification approaches. To advance this research, there is a need to compare these approaches. As a first step towards this, in this paper we suggest a way to compare different formal approaches for verifying designs of route-based interlocking systems and we demonstrate it on modelling and verification approaches developed within the research groups at DTU/Bremen and at Surrey/Swansea. The focus is on designs that are specified by so-called control tables. The paper can serve as a starting point for further comparative studies. The DTU/Bremen research has been funded by the RobustRailS project granted by Innovation Fund Denmark. The Surrey/Swansea research has been funded by the SafeCap and the DITTO research projects granted by EPSRC and RSSB. The authors would like to thank Linh Hong Vu for providing the benchmark of scheme plans and the drawings of the track plans.",

keywords = "Software Engineering, Logics and Meanings of Programs, Computer Communication Networks, Systems and Data Security, Mathematical Logic and Formal Languages, Artificial Intelligence (incl. Robotics)",

author = "Haxthausen, \{Anne Elisabeth\} and Nguyen, \{Hoang Nga\} and Markus Roggenbach",

year = "2016",

doi = "10.1007/978-3-319-33951-1\_12",

language = "English",

isbn = "978-3-319-33950-4",

volume = "9707",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "160--177",

booktitle = "Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification",

note = "The International Conference on Reliability, Safety and Security of Railway Systems : Modelling, Analysis, Verification, and Certification, RSSRail 2016 ; Conference date: 28-06-2016 Through 30-06-2016",

url = "https://conferences.ncl.ac.uk/rssrail/",

}

Haxthausen, AE, Nguyen, HN & Roggenbach, M 2016, Comparing formal verification approaches of interlocking systems. in Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: First International Conference, RSSRail 2016 Paris, France, June 28–30, 2016 Proceedings. vol. 9707, Springer, Lecture Notes in Computer Science, pp. 160-177, The International Conference on Reliability, Safety and Security of Railway Systems, Paris, France, 28/06/2016. https://doi.org/10.1007/978-3-319-33951-1_12

Comparing formal verification approaches of interlocking systems. / Haxthausen, Anne Elisabeth; Nguyen, Hoang Nga; Roggenbach, Markus.
Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: First International Conference, RSSRail 2016 Paris, France, June 28–30, 2016 Proceedings. Vol. 9707 Springer, 2016. p. 160-177 (Lecture Notes in Computer Science).

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

TY - GEN

T1 - Comparing formal verification approaches of interlocking systems

AU - Haxthausen, Anne Elisabeth

AU - Nguyen, Hoang Nga

AU - Roggenbach, Markus

N1 - Conference code: 1

PY - 2016

Y1 - 2016

N2 - The verification of railway interlocking systems is a challenging task, and therefore several research groups have suggested to improve this task by using formal methods, but they use different modelling and verification approaches. To advance this research, there is a need to compare these approaches. As a first step towards this, in this paper we suggest a way to compare different formal approaches for verifying designs of route-based interlocking systems and we demonstrate it on modelling and verification approaches developed within the research groups at DTU/Bremen and at Surrey/Swansea. The focus is on designs that are specified by so-called control tables. The paper can serve as a starting point for further comparative studies. The DTU/Bremen research has been funded by the RobustRailS project granted by Innovation Fund Denmark. The Surrey/Swansea research has been funded by the SafeCap and the DITTO research projects granted by EPSRC and RSSB. The authors would like to thank Linh Hong Vu for providing the benchmark of scheme plans and the drawings of the track plans.

AB - The verification of railway interlocking systems is a challenging task, and therefore several research groups have suggested to improve this task by using formal methods, but they use different modelling and verification approaches. To advance this research, there is a need to compare these approaches. As a first step towards this, in this paper we suggest a way to compare different formal approaches for verifying designs of route-based interlocking systems and we demonstrate it on modelling and verification approaches developed within the research groups at DTU/Bremen and at Surrey/Swansea. The focus is on designs that are specified by so-called control tables. The paper can serve as a starting point for further comparative studies. The DTU/Bremen research has been funded by the RobustRailS project granted by Innovation Fund Denmark. The Surrey/Swansea research has been funded by the SafeCap and the DITTO research projects granted by EPSRC and RSSB. The authors would like to thank Linh Hong Vu for providing the benchmark of scheme plans and the drawings of the track plans.

KW - Software Engineering

KW - Logics and Meanings of Programs

KW - Computer Communication Networks

KW - Systems and Data Security

KW - Mathematical Logic and Formal Languages

KW - Artificial Intelligence (incl. Robotics)

U2 - 10.1007/978-3-319-33951-1_12

DO - 10.1007/978-3-319-33951-1_12

M3 - Article in proceedings

SN - 978-3-319-33950-4

VL - 9707

T3 - Lecture Notes in Computer Science

SP - 160

EP - 177

BT - Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification

PB - Springer

T2 - The International Conference on Reliability, Safety and Security of Railway Systems

Y2 - 28 June 2016 through 30 June 2016

ER -

Haxthausen AE, Nguyen HN, Roggenbach M. Comparing formal verification approaches of interlocking systems. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: First International Conference, RSSRail 2016 Paris, France, June 28–30, 2016 Proceedings. Vol. 9707. Springer. 2016. p. 160-177. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-33951-1_12

Comparing formal verification approaches of interlocking systems

Abstract

Conference

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this