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

177 Downloads (Pure)

Abstract

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
Publication statusPublished - 2017
Event15th International Conference on Software Engineering and Formal Methods - Vienna, Austria
Duration: 4 Sep 20178 Sep 2017

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

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

Cite this

Fantechi, A., Haxthausen, A. E., & Macedo, H. D. D. S. (2017). Compositional Verification of Interlocking Systems for Large Stations. In Software Engineering and Formal Methods (Vol. 10469, pp. 236-252). Springer. Lecture Notes in Computer Science, Vol.. 10469 https://doi.org/10.1007/978-3-319-66197-1_15
Fantechi, Alessandro ; Haxthausen, Anne Elisabeth ; Macedo, Hugo Daniel dos Santos. / Compositional Verification of Interlocking Systems for Large Stations. Software Engineering and Formal Methods. Vol. 10469 Springer, 2017. pp. 236-252 (Lecture Notes in Computer Science, Vol. 10469).
@inproceedings{37298bb678a64e0a98abd9ce111ec2fc,
title = "Compositional Verification of Interlocking Systems for Large Stations",
abstract = "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.",
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",
author = "Alessandro Fantechi and Haxthausen, {Anne Elisabeth} and Macedo, {Hugo Daniel dos Santos}",
year = "2017",
doi = "10.1007/978-3-319-66197-1_15",
language = "English",
isbn = "9783319661971",
volume = "10469",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "236--252",
booktitle = "Software Engineering and Formal Methods",

}

Fantechi, A, Haxthausen, AE & Macedo, HDDS 2017, Compositional Verification of Interlocking Systems for Large Stations. in Software Engineering and Formal Methods. vol. 10469, Springer, Lecture Notes in Computer Science, vol. 10469, pp. 236-252, 15th International Conference on Software Engineering and Formal Methods, Vienna, Austria, 04/09/2017. https://doi.org/10.1007/978-3-319-66197-1_15

Compositional Verification of Interlocking Systems for Large Stations. / Fantechi, Alessandro; Haxthausen, Anne Elisabeth; Macedo, Hugo Daniel dos Santos.

Software Engineering and Formal Methods. Vol. 10469 Springer, 2017. p. 236-252 (Lecture Notes in Computer Science, Vol. 10469).

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

TY - GEN

T1 - Compositional Verification of Interlocking Systems for Large Stations

AU - Fantechi, Alessandro

AU - Haxthausen, Anne Elisabeth

AU - Macedo, Hugo Daniel dos Santos

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

KW - Computer Science

KW - Software Engineering

KW - Programming Languages, Compilers, Interpreters

KW - Programming Techniques

KW - Theory of Computation

KW - System Performance and Evaluation

KW - Artificial Intelligence (incl. Robotics)

KW - Railway interlocking

KW - Compositional verification

KW - Model checking

U2 - 10.1007/978-3-319-66197-1_15

DO - 10.1007/978-3-319-66197-1_15

M3 - Article in proceedings

SN - 9783319661971

VL - 10469

T3 - Lecture Notes in Computer Science

SP - 236

EP - 252

BT - Software Engineering and Formal Methods

PB - Springer

ER -

Fantechi A, Haxthausen AE, Macedo HDDS. Compositional Verification of Interlocking Systems for Large Stations. In Software Engineering and Formal Methods. Vol. 10469. Springer. 2017. p. 236-252. (Lecture Notes in Computer Science, Vol. 10469). https://doi.org/10.1007/978-3-319-66197-1_15