Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release

Linh Hong Vu; Anne Elisabeth Haxthausen; Jan Peleska

Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release

Linh Hong Vu, Anne Elisabeth Haxthausen, Jan Peleska

Department of Applied Mathematics and Computer Science

University of Bremen

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

1040 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	Preliminary Proceedings of the Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014)
Editors	Cyrille Artho, Peter Csaba Ölveczky
Publication date	2014
Pages	58-73
Publication status	Published - 2014
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/Territory	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/

Bibliographical note

Revised versions of accepted regular papers will appear in the post-proceedings of FTSCS 2014 that will be published as a volume in Springer’s Communications in Computer and Information Science (CCIS) series.

Keywords

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

Access to Document

MainAccepted author manuscript, 369 KB

http://csaba.olveczky.se/ftscs14-preproceedings.pdf

OpenUrl availability

Full text

Cite this

@inproceedings{8e8948815ba343159fcc7e5cbfd66d54,

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, Robust Rails, Safety-critical systems",

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

note = "Revised versions of accepted regular papers will appear in the post-proceedings of FTSCS 2014 that will be published as a volume in Springer{\textquoteright}s Communications in Computer and Information Science (CCIS) series.; Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014), FTSCS ; Conference date: 03-11-2014 Through 07-11-2014",

year = "2014",

language = "English",

pages = "58--73",

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

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

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

}

Vu, LH, Haxthausen, AE & Peleska, J 2014, Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release. in C Artho & PC Ölveczky (eds), Preliminary Proceedings of the Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014). pp. 58-73, Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014), Luxembourg, Luxembourg, 03/11/2014. <http://csaba.olveczky.se/ftscs14-preproceedings.pdf>

Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release. / Vu, Linh Hong; Haxthausen, Anne Elisabeth; Peleska, Jan.
Preliminary Proceedings of the Third International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014). ed. / Cyrille Artho; Peter Csaba Ölveczky. 2014. p. 58-73.

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 - 2014

Y1 - 2014

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 - Robust Rails

KW - Safety-critical systems

M3 - Article in proceedings

SP - 58

EP - 73

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

A2 - Artho, Cyrille

A2 - Ölveczky, Peter Csaba

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

Y2 - 3 November 2014 through 7 November 2014

ER -

Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release

Abstract

Workshop

Bibliographical note

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this