Formal Modelling and Verification of a Distributed Railway Interlocking System Using UPPAAL

Per Lange  Laursen; Van Anh Thi  Trinh; Anne Elisabeth Haxthausen

doi:10.1007/978-3-030-61467-6_27

Formal Modelling and Verification of a Distributed Railway Interlocking System Using UPPAAL

Per Lange Laursen
, Van Anh Thi Trinh
, Anne Elisabeth Haxthausen

Department of Applied Mathematics and Computer Science

Technical University of Denmark

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

879 Downloads (Orbit)

Abstract

This paper investigates the modelling and model checking of a real-world distributed railway interlocking system algorithm using UPPAAL. Interlocking systems for specific railway networks are verified by instantiating a generic (re-configurable) model with configuration data that describes the network and involved trains. There are three variants of the generic model: (1) The first variant includes the minimum required operations such as reserving a segment for a train, locking a point in a fixed position, and moving a train. (2) A restricted variant that uses a more strict operational order. (3) A variant that extends the first variant with a cancel operation that removes reservations and locks. Verification experiments are carried out on instances of all variants in order to check their correctness and compare their performance. The scalability of the three variants has been investigated with networks of varying sizes. Finally, for a real-world railway network, instances of the three model variants have been successfully verified.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation: Applications
Publisher	Springer
Publication date	2020
Pages	415-433
ISBN (Print)	978-3-030-61467-6
DOIs	https://doi.org/10.1007/978-3-030-61467-6_27
Publication status	Published - 2020
Event	International Symposium On Leveraging Applications of Formal Methods, Verification and Validation 2020 - Virtual event - POSTPONED TO 2021!, Greece Duration: 20 Oct 2020 → 30 Oct 2020 http://www.isola-conference.org/

Conference

Conference	International Symposium On Leveraging Applications of Formal Methods, Verification and Validation 2020
Location	Virtual event - POSTPONED TO 2021!
Country/Territory	Greece
Period	20/10/2020 → 30/10/2020
Other	Postponed to October 2021 due to Covid-19
Internet address	http://www.isola-conference.org/

Series	Lecture Notes in Computer Science
Volume	12478
ISSN	0302-9743

Keywords

Distributed systems
Railway interlocking systems
Formal verification
Model Checking
UPPAAL

Access to Document

10.1007/978-3-030-61467-6_27

FulltextAccepted author manuscript, 585 KB

OpenUrl availability

Check availability in DTU Findit

Cite this

@inproceedings{c4125929bab14a1ca609dd1ae7529a0e,

title = "Formal Modelling and Verification of a Distributed Railway Interlocking System Using UPPAAL",

abstract = "This paper investigates the modelling and model checking of a real-world distributed railway interlocking system algorithm using UPPAAL. Interlocking systems for specific railway networks are verified by instantiating a generic (re-configurable) model with configuration data that describes the network and involved trains. There are three variants of the generic model: (1) The first variant includes the minimum required operations such as reserving a segment for a train, locking a point in a fixed position, and moving a train. (2) A restricted variant that uses a more strict operational order. (3) A variant that extends the first variant with a cancel operation that removes reservations and locks. Verification experiments are carried out on instances of all variants in order to check their correctness and compare their performance. The scalability of the three variants has been investigated with networks of varying sizes. Finally, for a real-world railway network, instances of the three model variants have been successfully verified. ",

keywords = "Distributed systems, Railway interlocking systems, Formal verification, Model Checking, UPPAAL",

author = "Laursen, \{Per Lange\} and Trinh, \{Van Anh Thi\} and Haxthausen, \{Anne Elisabeth\}",

year = "2020",

doi = "10.1007/978-3-030-61467-6\_27",

language = "English",

isbn = "978-3-030-61467-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "415--433",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation: Applications",

note = "International Symposium On Leveraging Applications of Formal Methods, Verification and Validation 2020, ISoLA 2020 ; Conference date: 20-10-2020 Through 30-10-2020",

url = "http://www.isola-conference.org/",

}

Laursen, PL, Trinh, VAT & Haxthausen, AE 2020, Formal Modelling and Verification of a Distributed Railway Interlocking System Using UPPAAL. in Leveraging Applications of Formal Methods, Verification and Validation: Applications. Springer, Lecture Notes in Computer Science, vol. 12478, pp. 415-433, International Symposium On Leveraging Applications of Formal Methods, Verification and Validation 2020, Greece, 20/10/2020. https://doi.org/10.1007/978-3-030-61467-6_27

Formal Modelling and Verification of a Distributed Railway Interlocking System Using UPPAAL. / Laursen, Per Lange ; Trinh, Van Anh Thi ; Haxthausen, Anne Elisabeth.
Leveraging Applications of Formal Methods, Verification and Validation: Applications. Springer, 2020. p. 415-433 (Lecture Notes in Computer Science, Vol. 12478).

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

TY - GEN

T1 - Formal Modelling and Verification of a Distributed Railway Interlocking System Using UPPAAL

AU - Laursen, Per Lange

AU - Trinh, Van Anh Thi

AU - Haxthausen, Anne Elisabeth

PY - 2020

Y1 - 2020

N2 - This paper investigates the modelling and model checking of a real-world distributed railway interlocking system algorithm using UPPAAL. Interlocking systems for specific railway networks are verified by instantiating a generic (re-configurable) model with configuration data that describes the network and involved trains. There are three variants of the generic model: (1) The first variant includes the minimum required operations such as reserving a segment for a train, locking a point in a fixed position, and moving a train. (2) A restricted variant that uses a more strict operational order. (3) A variant that extends the first variant with a cancel operation that removes reservations and locks. Verification experiments are carried out on instances of all variants in order to check their correctness and compare their performance. The scalability of the three variants has been investigated with networks of varying sizes. Finally, for a real-world railway network, instances of the three model variants have been successfully verified.

AB - This paper investigates the modelling and model checking of a real-world distributed railway interlocking system algorithm using UPPAAL. Interlocking systems for specific railway networks are verified by instantiating a generic (re-configurable) model with configuration data that describes the network and involved trains. There are three variants of the generic model: (1) The first variant includes the minimum required operations such as reserving a segment for a train, locking a point in a fixed position, and moving a train. (2) A restricted variant that uses a more strict operational order. (3) A variant that extends the first variant with a cancel operation that removes reservations and locks. Verification experiments are carried out on instances of all variants in order to check their correctness and compare their performance. The scalability of the three variants has been investigated with networks of varying sizes. Finally, for a real-world railway network, instances of the three model variants have been successfully verified.

KW - Distributed systems

KW - Railway interlocking systems

KW - Formal verification

KW - Model Checking

KW - UPPAAL

U2 - 10.1007/978-3-030-61467-6_27

DO - 10.1007/978-3-030-61467-6_27

M3 - Article in proceedings

SN - 978-3-030-61467-6

T3 - Lecture Notes in Computer Science

SP - 415

EP - 433

BT - Leveraging Applications of Formal Methods, Verification and Validation: Applications

PB - Springer

T2 - International Symposium On Leveraging Applications of Formal Methods, Verification and Validation 2020

Y2 - 20 October 2020 through 30 October 2020

ER -

Formal Modelling and Verification of a Distributed Railway Interlocking System Using UPPAAL

Abstract

Conference

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this