Compositional Verification of Interlocking Systems for Large Stations

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2017

Documents

DOI

View graph of relations

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
Volume10469
PublisherSpringer
Publication date2017
Pages236-252
ISBN (print)9783319661971
DOIs
StatePublished - 2017
Event15th International Conference on Software Engineering and Formal Methods - Vienna, Austria

Conference

Conference15th International Conference on Software Engineering and Formal Methods
CountryAustria
CityVienna
Period04/09/201708/09/2017
SeriesLecture Notes in Computer Science
Volume10469
ISSN0302-9743
CitationsWeb of Science® Times Cited: No match on DOI

    Keywords

  • 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
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

Download statistics

No data available

ID: 134976350