Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations

Hugo Daniel Macedo; Assensandro Fantechi; Anne Elisabeth Haxthausen

doi:10.1007/978-3-319-57288-8_11

Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations

Hugo Daniel Macedo, Assensandro Fantechi, Anne Elisabeth Haxthausen

Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

10 Citations (Scopus)

Abstract

In the railway domain safety is guaranteed by an interlocking system which translates operational decisions into commands leading to field operations. Such a system is safety critical and demands thorough formal verification during its development process. Within this context, our work has focused on the extension of a compositional model checking approach to formally verify interlocking system models for lines with multiple stations. The idea of the approach is to decompose a model of the interlocking system by applying cuts at the network modelling level. The paper introduces an alternative cut (the linear cut) to a previously proposed cut (border cut). Powered with the linear cut, the model checking approach is then applied to the verification of an interlocking system controlling a real-world multiple station line.

Original language	English
Title of host publication	NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings : NFM 2017
Editors	Clark Barrett, Misty Davies, Temesghen Kahsai
Number of pages	17
Volume	10227
Publisher	Springer
Publication date	9 Apr 2017
Pages	146-162
ISBN (Print)	978-3-319-57287-1
ISBN (Electronic)	978-3-319-57288-8
DOIs	https://doi.org/10.1007/978-3-319-57288-8_11
Publication status	Published - 9 Apr 2017
Event	9th NASA Formal Methods Symposium - NASA Ames Research Center, Moffett Field, United States Duration: 16 May 2017 → 18 May 2017 https://ti.arc.nasa.gov/events/nfm-2017/

Conference

Conference	9th NASA Formal Methods Symposium
Location	NASA Ames Research Center
Country/Territory	United States
City	Moffett Field
Period	16/05/2017 → 18/05/2017
Internet address	https://ti.arc.nasa.gov/events/nfm-2017/

Series	Lecture Notes in Computer Science
Number	10227
ISSN	0302-9743

Keywords

Compositional verification
Model checking
Railway interlocking

Access to Document

10.1007/978-3-319-57288-8_11

Library access?

Check availability with the Royal Danish Library

Cite this

Macedo, Hugo Daniel ; Fantechi, Assensandro ; Haxthausen, Anne Elisabeth. / Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations. NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings: NFM 2017. editor / Clark Barrett ; Misty Davies ; Temesghen Kahsai. Vol. 10227 Springer, 2017. pp. 146-162 (Lecture Notes in Computer Science; No. 10227).

@inproceedings{021204302d994e3c9db54f78266f195d,

title = "Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations",

abstract = "In the railway domain safety is guaranteed by an interlocking system which translates operational decisions into commands leading to field operations. Such a system is safety critical and demands thorough formal verification during its development process. Within this context, our work has focused on the extension of a compositional model checking approach to formally verify interlocking system models for lines with multiple stations. The idea of the approach is to decompose a model of the interlocking system by applying cuts at the network modelling level. The paper introduces an alternative cut (the linear cut) to a previously proposed cut (border cut). Powered with the linear cut, the model checking approach is then applied to the verification of an interlocking system controlling a real-world multiple station line.",

keywords = "Compositional verification, Model checking, Railway interlocking",

author = "Macedo, \{Hugo Daniel\} and Assensandro Fantechi and Haxthausen, \{Anne Elisabeth\}",

year = "2017",

month = apr,

day = "9",

doi = "10.1007/978-3-319-57288-8\_11",

language = "English",

isbn = "978-3-319-57287-1",

volume = "10227",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

number = "10227",

pages = "146--162",

editor = "Clark Barrett and Misty Davies and Temesghen Kahsai",

booktitle = "NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings",

address = "Netherlands",

note = "9th NASA Formal Methods Symposium ; Conference date: 16-05-2017 Through 18-05-2017",

url = "https://ti.arc.nasa.gov/events/nfm-2017/",

}

Macedo, HD, Fantechi, A & Haxthausen, AE 2017, Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations. in C Barrett, M Davies & T Kahsai (eds), NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings: NFM 2017. vol. 10227, Springer, Lecture Notes in Computer Science, no. 10227, pp. 146-162, 9th NASA Formal Methods Symposium , Moffett Field, California, United States, 16/05/2017. https://doi.org/10.1007/978-3-319-57288-8_11

Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations. / Macedo, Hugo Daniel; Fantechi, Assensandro; Haxthausen, Anne Elisabeth.
NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings: NFM 2017. ed. / Clark Barrett; Misty Davies; Temesghen Kahsai. Vol. 10227 Springer, 2017. p. 146-162 (Lecture Notes in Computer Science; No. 10227).

Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations

AU - Macedo, Hugo Daniel

AU - Fantechi, Assensandro

AU - Haxthausen, Anne Elisabeth

PY - 2017/4/9

Y1 - 2017/4/9

N2 - In the railway domain safety is guaranteed by an interlocking system which translates operational decisions into commands leading to field operations. Such a system is safety critical and demands thorough formal verification during its development process. Within this context, our work has focused on the extension of a compositional model checking approach to formally verify interlocking system models for lines with multiple stations. The idea of the approach is to decompose a model of the interlocking system by applying cuts at the network modelling level. The paper introduces an alternative cut (the linear cut) to a previously proposed cut (border cut). Powered with the linear cut, the model checking approach is then applied to the verification of an interlocking system controlling a real-world multiple station line.

AB - In the railway domain safety is guaranteed by an interlocking system which translates operational decisions into commands leading to field operations. Such a system is safety critical and demands thorough formal verification during its development process. Within this context, our work has focused on the extension of a compositional model checking approach to formally verify interlocking system models for lines with multiple stations. The idea of the approach is to decompose a model of the interlocking system by applying cuts at the network modelling level. The paper introduces an alternative cut (the linear cut) to a previously proposed cut (border cut). Powered with the linear cut, the model checking approach is then applied to the verification of an interlocking system controlling a real-world multiple station line.

KW - Compositional verification

KW - Model checking

KW - Railway interlocking

UR - https://www.scopus.com/pages/publications/85018709363

U2 - 10.1007/978-3-319-57288-8_11

DO - 10.1007/978-3-319-57288-8_11

M3 - Article in proceedings

SN - 978-3-319-57287-1

VL - 10227

T3 - Lecture Notes in Computer Science

SP - 146

EP - 162

BT - NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings

A2 - Barrett, Clark

A2 - Davies, Misty

A2 - Kahsai, Temesghen

PB - Springer

T2 - 9th NASA Formal Methods Symposium

Y2 - 16 May 2017 through 18 May 2017

ER -

Macedo HD, Fantechi A, Haxthausen AE. Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations. In Barrett C, Davies M, Kahsai T, editors, NASA Formal Methods - 9th International Symposium, NFM 2017 Moffett Field, Proceedings: NFM 2017. Vol. 10227. Springer. 2017. p. 146-162. (Lecture Notes in Computer Science; No. 10227). doi: 10.1007/978-3-319-57288-8_11

Compositional Model Checking of Interlocking Systems for Lines with Multiple Stations

Abstract

Conference

Keywords

Access to Document

Library access?

Other files and links

Fingerprint

Cite this