Decomposing the Verification of Interlocking Systems

Anne E. Haxthausen*, Alessandro Fantechi, Gloria Gori

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review


This paper considers model checking the safety for members of a product line of railway interlocking systems, where an actual interlocking system is modelled as an instance of a generic model configured over the network under its control. For models over large networks it is a well-known problem that model checking may fail due to state space explosion. The RobustRailS tools that combine inductive reasoning with SMT solving using Jan Peleska’s powerful RT-Tester tool suite have pushed considerably the limits of the size of networks that can be handled. To further push these limits, we have proposed a compositional method that can be combined with RobustRailS to reduce the size of networks to be model checked: the idea is to divide the network of the system to be verified into two sub-networks and then model check the model instances for these sub-networks instead of that for the full network. In this paper we propose a strategy for applying such network divisions repeatedly to achieve a fine granularity decomposition of a given network into a number of small sub-networks. Under certain conditions, these sub-networks all belong to a library of pre-verified elementary networks, so model checking of the sub-networks is no longer needed.
Original languageEnglish
Title of host publicationApplicable Formal Methods for Safe Industrial Products
Publication date2023
ISBN (Print)978-3-031-40131-2
ISBN (Electronic)978-3-031-40132-9
Publication statusPublished - 2023
SeriesLecture Notes in Computer Science


  • Compositional Verification
  • Formal Methods
  • Interlocking Systems
  • Model Checking


Dive into the research topics of 'Decomposing the Verification of Interlocking Systems'. Together they form a unique fingerprint.

Cite this