Compositional Verification of Interlocking Systems for Large Stations

Alessandro Fantechi, Anne Elisabeth Haxthausen, Hugo Daniel dos Santos Macedo

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

275 Downloads (Pure)


Railway interlocking systems are responsible to grant exclusive access to a route, that is a sequence of track elements, through a station or a network. Formal verification that basic safety rules regarding exclusive access to routes are satisfied by an implementation is still a challenge for networks of large size due to the exponential computation time and resources needed. Some recent attempts to address this challenge adopt a compositional approach, targeted to track layouts that are easily decomposable into sub-networks such that a route is almost fully contained in a sub-network: in this way granting the access to a route is essentially a decision local to the sub-network, and the interfaces with the rest of the network easily abstract away less interesting details related to the external world. Following up on previous work, where we defined a compositional verification method that started considering routes that overlap between sub-networks in interlocking systems governing a multi-station line, we attack the verification of large networks, which are typically those in main stations of major cities, and where routes are very intertwined and can hardly be separated into sub-networks that are independent at some degree. At this regard, we study how the division of a complex network into sub-networks, using stub elements to abstract all the routes that are common between sub-networks, may still guarantee compositionality of verification of safety properties.
Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods
Publication date2017
ISBN (Print)9783319661971
Publication statusPublished - 2017
Event15th International Conference on Software Engineering and Formal Methods - Vienna, Austria
Duration: 4 Sep 20178 Sep 2017


Conference15th International Conference on Software Engineering and Formal Methods
SeriesLecture Notes in Computer Science


  • Computer Science
  • Software Engineering
  • Programming Languages, Compilers, Interpreters
  • Programming Techniques
  • Theory of Computation
  • System Performance and Evaluation
  • Artificial Intelligence (incl. Robotics)
  • Railway interlocking
  • Compositional verification
  • Model checking

Fingerprint Dive into the research topics of 'Compositional Verification of Interlocking Systems for Large Stations'. Together they form a unique fingerprint.

Cite this