Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release

Linh Hong Vu; Anne Elisabeth Haxthausen; Jan Peleska

doi:10.1007/978-3-319-17581-2_15

Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release

Linh Hong Vu, Anne Elisabeth Haxthausen, Jan Peleska

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

439 Downloads (Pure)

Abstract

In this paper, we present a method and an associated tool suite for formal verification of the new ETCS level 2 based Danish railway interlocking systems. We have made a generic and reconfigurable model of the system behavior and generic high-level safety properties. This model accommodates sequential release – a feature in the new Danish interlocking systems. The generic model and safety properties can be instantiated with interlocking configuration data, resulting in a concrete model in the form of a Kripke structure, and in high-level safety properties expressed as state invariants. Using SMT based bounded model checking (BMC) and inductive reasoning, we are able to verify the properties for model instances corresponding to railway networks of industrial size. Experiments also show that BMC is efficient for finding bugs in the railway interlocking designs.

Original language	English
Title of host publication	Proceedings of the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014)
Editors	Cyrille Artho, Peter Csaba Ölveczky
Publisher	Springer
Publication date	2015
Pages	223-238
ISBN (Print)	978-3-319-17580-5
ISBN (Electronic)	978-3-319-17581-2
DOIs	https://doi.org/10.1007/978-3-319-17581-2_15
Publication status	Published - 2015
Event	Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014) - Luxembourg, Luxembourg Duration: 3 Nov 2014 → 7 Nov 2014 Conference number: 3 http://www.ftscs.org/

Workshop

Workshop	Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014)
Number	3
Country	Luxembourg
City	Luxembourg
Period	03/11/2014 → 07/11/2014
Other	A satellite event of the ICFEM 2014 conference.
Internet address	http://www.ftscs.org/

Series	Communications in Computer and Information Science
Volume	476
ISSN	1865-0929

Keywords

Railway interlocking systems
Formal verification
Bounded model checking
Inductive reasoning
RobustRails
Safety-critical systems

Access to Document

10.1007/978-3-319-17581-2_15

2015mainAccepted author manuscript, 401 KB

Cite this

Vu, L. H., Haxthausen, A. E., & Peleska, J. (2015). Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release. In C. Artho, & P. Csaba Ölveczky (Eds.), Proceedings of the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014) (pp. 223-238). Springer. Communications in Computer and Information Science, Vol.. 476 https://doi.org/10.1007/978-3-319-17581-2_15

Vu, Linh Hong ; Haxthausen, Anne Elisabeth ; Peleska, Jan. / Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release. Proceedings of the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014). editor / Cyrille Artho ; Peter Csaba Ölveczky. Springer, 2015. pp. 223-238 (Communications in Computer and Information Science, Vol. 476).

@inproceedings{b4c9fb8f37e34638b42363d4c7e43344,

title = "Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release",

abstract = "In this paper, we present a method and an associated tool suite for formal verification of the new ETCS level 2 based Danish railway interlocking systems. We have made a generic and reconfigurable model of the system behavior and generic high-level safety properties. This model accommodates sequential release – a feature in the new Danish interlocking systems. The generic model and safety properties can be instantiated with interlocking configuration data, resulting in a concrete model in the form of a Kripke structure, and in high-level safety properties expressed as state invariants. Using SMT based bounded model checking (BMC) and inductive reasoning, we are able to verify the properties for model instances corresponding to railway networks of industrial size. Experiments also show that BMC is efficient for finding bugs in the railway interlocking designs.",

keywords = "Railway interlocking systems, Formal verification, Bounded model checking, Inductive reasoning, RobustRails, Safety-critical systems",

author = "Vu, {Linh Hong} and Haxthausen, {Anne Elisabeth} and Jan Peleska",

year = "2015",

doi = "10.1007/978-3-319-17581-2_15",

language = "English",

isbn = "978-3-319-17580-5",

series = "Communications in Computer and Information Science",

publisher = "Springer",

pages = "223--238",

editor = "Artho, {Cyrille } and {Csaba {\"O}lveczky}, {Peter }",

booktitle = "Proceedings of the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014)",

note = "Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014), FTSCS ; Conference date: 03-11-2014 Through 07-11-2014",

url = "http://www.ftscs.org/",

}

Vu, LH, Haxthausen, AE & Peleska, J 2015, Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release. in C Artho & P Csaba Ölveczky (eds), Proceedings of the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014). Springer, Communications in Computer and Information Science, vol. 476, pp. 223-238, Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014), Luxembourg, Luxembourg, 03/11/2014. https://doi.org/10.1007/978-3-319-17581-2_15

Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release. / Vu, Linh Hong; Haxthausen, Anne Elisabeth; Peleska, Jan.

Proceedings of the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014). ed. / Cyrille Artho; Peter Csaba Ölveczky. Springer, 2015. p. 223-238 (Communications in Computer and Information Science, Vol. 476).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release

AU - Vu, Linh Hong

AU - Haxthausen, Anne Elisabeth

AU - Peleska, Jan

N1 - Conference code: 3

PY - 2015

Y1 - 2015

N2 - In this paper, we present a method and an associated tool suite for formal verification of the new ETCS level 2 based Danish railway interlocking systems. We have made a generic and reconfigurable model of the system behavior and generic high-level safety properties. This model accommodates sequential release – a feature in the new Danish interlocking systems. The generic model and safety properties can be instantiated with interlocking configuration data, resulting in a concrete model in the form of a Kripke structure, and in high-level safety properties expressed as state invariants. Using SMT based bounded model checking (BMC) and inductive reasoning, we are able to verify the properties for model instances corresponding to railway networks of industrial size. Experiments also show that BMC is efficient for finding bugs in the railway interlocking designs.

AB - In this paper, we present a method and an associated tool suite for formal verification of the new ETCS level 2 based Danish railway interlocking systems. We have made a generic and reconfigurable model of the system behavior and generic high-level safety properties. This model accommodates sequential release – a feature in the new Danish interlocking systems. The generic model and safety properties can be instantiated with interlocking configuration data, resulting in a concrete model in the form of a Kripke structure, and in high-level safety properties expressed as state invariants. Using SMT based bounded model checking (BMC) and inductive reasoning, we are able to verify the properties for model instances corresponding to railway networks of industrial size. Experiments also show that BMC is efficient for finding bugs in the railway interlocking designs.

KW - Railway interlocking systems

KW - Formal verification

KW - Bounded model checking

KW - Inductive reasoning

KW - RobustRails

KW - Safety-critical systems

U2 - 10.1007/978-3-319-17581-2_15

DO - 10.1007/978-3-319-17581-2_15

M3 - Article in proceedings

SN - 978-3-319-17580-5

T3 - Communications in Computer and Information Science

SP - 223

EP - 238

BT - Proceedings of the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014)

A2 - Artho, Cyrille

A2 - Csaba Ölveczky, Peter

PB - Springer

T2 - Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014)

Y2 - 3 November 2014 through 7 November 2014

ER -

Vu LH, Haxthausen AE, Peleska J. Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release. In Artho C, Csaba Ölveczky P, editors, Proceedings of the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014). Springer. 2015. p. 223-238. (Communications in Computer and Information Science, Vol. 476). https://doi.org/10.1007/978-3-319-17581-2_15