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 proceedingArticle in proceedingsResearchpeer-review

117 Downloads (Pure)

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 languageEnglish
Title of host publicationReliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification
PublisherSpringer
Publication date2022
Pages3-19
ISBN (Print)978-3-031-05813-4
DOIs
Publication statusPublished - 2022
Event4th International Conference on Reliability, Safety, and Security of Railway Systems - Union Internationale des Chemins de fer, Paris, France
Duration: 1 Jun 20222 Jun 2022
https://rssrail2022.univ-gustave-eiffel.fr/

Conference

Conference4th International Conference on Reliability, Safety, and Security of Railway Systems
LocationUnion Internationale des Chemins de fer
Country/TerritoryFrance
CityParis
Period01/06/202202/06/2022
Internet address
SeriesLecture Notes in Computer Science
Volume13294
ISSN0302-9743

Keywords

  • Compositional verification
  • Model checking railway
  • Railway interlocking systems

Fingerprint

Dive into the research topics of 'Compositional Verification of Railway Interlockings: Comparison of Two Methods'. Together they form a unique fingerprint.

Cite this