Compositional Verification of Railway Interlockings: Comparison of Two Methods

Alessandro Fantechi; Gloria Gori; Anne E. Haxthausen; Christophe Limbrée

doi:10.1007/978-3-031-05814-1_1

Compositional Verification of Railway Interlockings: Comparison of Two Methods

Alessandro Fantechi, Gloria Gori, Anne E. Haxthausen, Christophe Limbrée

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

143 Downloads (Orbit)

Abstract

Formal verification of safety of interlocking systems and of their configuration on a specific track layout is conceptually an easy task for model checking. Systems that control large railway networks, however, are challenging due to state space explosion problems. A possible way out is to adopt a compositional approach that allows safety of a large system to be deduced from the formal verification of parts in which the system has been properly decomposed. Two different approaches have been proposed in this regard, differing for the decomposition assumptions and for the adopted compositional verification techniques. In this paper we compare the two approaches, discussing the differences, but also showing how the different concepts behind them are essentially equivalent, hence producing comparable benefits.

Original language	English
Title of host publication	Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification
Publisher	Springer
Publication date	2022
Pages	3-19
ISBN (Print)	978-3-031-05813-4
DOIs	https://doi.org/10.1007/978-3-031-05814-1_1
Publication status	Published - 2022
Event	4^th International Conference on Reliability, Safety, and Security of Railway Systems - Union Internationale des Chemins de fer, Paris, France Duration: 1 Jun 2022 → 2 Jun 2022 https://rssrail2022.univ-gustave-eiffel.fr/

Conference

Conference	4^th International Conference on Reliability, Safety, and Security of Railway Systems
Location	Union Internationale des Chemins de fer
Country/Territory	France
City	Paris
Period	01/06/2022 → 02/06/2022
Internet address	https://rssrail2022.univ-gustave-eiffel.fr/

Series	Lecture Notes in Computer Science
Volume	13294
ISSN	0302-9743

Keywords

Compositional verification
Model checking railway
Railway interlocking systems

Access to Document

10.1007/978-3-031-05814-1_1

FulltextAccepted author manuscript, 475 KB

OpenUrl availability

Full text

Cite this

@inproceedings{3ab467c2f344418d9b2ee317d80bd878,

title = "Compositional Verification of Railway Interlockings: Comparison of Two Methods",

abstract = "Formal verification of safety of interlocking systems and of their configuration on a specific track layout is conceptually an easy task for model checking. Systems that control large railway networks, however, are challenging due to state space explosion problems. A possible way out is to adopt a compositional approach that allows safety of a large system to be deduced from the formal verification of parts in which the system has been properly decomposed. Two different approaches have been proposed in this regard, differing for the decomposition assumptions and for the adopted compositional verification techniques. In this paper we compare the two approaches, discussing the differences, but also showing how the different concepts behind them are essentially equivalent, hence producing comparable benefits.",

keywords = "Compositional verification, Model checking railway, Railway interlocking systems",

author = "Alessandro Fantechi and Gloria Gori and Haxthausen, {Anne E.} and Christophe Limbr{\'e}e",

year = "2022",

doi = "10.1007/978-3-031-05814-1_1",

language = "English",

isbn = "978-3-031-05813-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "3--19",

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

note = "4<sup>th</sup> International Conference on Reliability, Safety, and Security of Railway Systems, RSSRail 2022 ; Conference date: 01-06-2022 Through 02-06-2022",

url = "https://rssrail2022.univ-gustave-eiffel.fr/",

}

Fantechi, A, Gori, G, Haxthausen, AE & Limbrée, C 2022, Compositional Verification of Railway Interlockings: Comparison of Two Methods. in Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. Springer, Lecture Notes in Computer Science, vol. 13294, pp. 3-19, 4^th International Conference on Reliability, Safety, and Security of Railway Systems, Paris, France, 01/06/2022. https://doi.org/10.1007/978-3-031-05814-1_1

Compositional Verification of Railway Interlockings: Comparison of Two Methods. / Fantechi, Alessandro; Gori, Gloria; Haxthausen, Anne E. et al.
Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. Springer, 2022. p. 3-19 (Lecture Notes in Computer Science, Vol. 13294).

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

TY - GEN

T1 - Compositional Verification of Railway Interlockings: Comparison of Two Methods

AU - Fantechi, Alessandro

AU - Gori, Gloria

AU - Haxthausen, Anne E.

AU - Limbrée, Christophe

PY - 2022

Y1 - 2022

N2 - Formal verification of safety of interlocking systems and of their configuration on a specific track layout is conceptually an easy task for model checking. Systems that control large railway networks, however, are challenging due to state space explosion problems. A possible way out is to adopt a compositional approach that allows safety of a large system to be deduced from the formal verification of parts in which the system has been properly decomposed. Two different approaches have been proposed in this regard, differing for the decomposition assumptions and for the adopted compositional verification techniques. In this paper we compare the two approaches, discussing the differences, but also showing how the different concepts behind them are essentially equivalent, hence producing comparable benefits.

AB - Formal verification of safety of interlocking systems and of their configuration on a specific track layout is conceptually an easy task for model checking. Systems that control large railway networks, however, are challenging due to state space explosion problems. A possible way out is to adopt a compositional approach that allows safety of a large system to be deduced from the formal verification of parts in which the system has been properly decomposed. Two different approaches have been proposed in this regard, differing for the decomposition assumptions and for the adopted compositional verification techniques. In this paper we compare the two approaches, discussing the differences, but also showing how the different concepts behind them are essentially equivalent, hence producing comparable benefits.

KW - Compositional verification

KW - Model checking railway

KW - Railway interlocking systems

U2 - 10.1007/978-3-031-05814-1_1

DO - 10.1007/978-3-031-05814-1_1

M3 - Article in proceedings

SN - 978-3-031-05813-4

T3 - Lecture Notes in Computer Science

SP - 3

EP - 19

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

PB - Springer

T2 - 4<sup>th</sup> International Conference on Reliability, Safety, and Security of Railway Systems

Y2 - 1 June 2022 through 2 June 2022

ER -