Model Checking a Distributed Interlocking System Using k-induction with RT-Tester

Signe Geisler Pedersen; Anne Elisabeth Haxthausen

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

Model Checking a Distributed Interlocking System Using k-induction with RT-Tester

Signe Geisler Pedersen, Anne Elisabeth Haxthausen

Department of Applied Mathematics and Computer Science

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

163 Downloads (Pure)

Abstract

This paper investigates the use of k-induction with RT-Tester for tackling the challenge of verifying the safety of a distributed railway interlocking system. For a real-world case study, it is described how a generic and reconfigurable model of the system is modelled in a new extension of the RAISE Specification Language (RSL). The generic model is instantiated with concrete data sets and subsequently model checked with respect to safety properties using the k-induction facilities in RT-Tester. The performance metrics of the verification with k-induction are additionally compared with the metrics of verifying the same system model with the SAL model checker.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation: Applications
Publisher	Springer
Publication date	2020
Pages	449-466
ISBN (Print)	978-3-030-61466-9
DOIs	https://doi.org/10.1007/978-3-030-61467-6_29
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

Model checking
RAISE
Railway interlocking systems
Distributed systems
k-induction
RT-Tester

Access to Document

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

FulltextAccepted author manuscript, 280 KB

OpenUrl availability

Full text

Cite this

@inproceedings{e9a850f500434d369ee0b8eedc466b03,

title = "Model Checking a Distributed Interlocking System Using k-induction with RT-Tester",

abstract = "This paper investigates the use of k-induction with RT-Tester for tackling the challenge of verifying the safety of a distributed railway interlocking system. For a real-world case study, it is described how a generic and reconfigurable model of the system is modelled in a new extension of the RAISE Specification Language (RSL). The generic model is instantiated with concrete data sets and subsequently model checked with respect to safety properties using the k-induction facilities in RT-Tester. The performance metrics of the verification with k-induction are additionally compared with the metrics of verifying the same system model with the SAL model checker.",

keywords = "Model checking, RAISE, Railway interlocking systems, Distributed systems, k-induction, RT-Tester",

author = "Pedersen, {Signe Geisler} and Haxthausen, {Anne Elisabeth}",

year = "2020",

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

language = "English",

isbn = "978-3-030-61466-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "449--466",

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/",

}

Pedersen, SG & Haxthausen, AE 2020, Model Checking a Distributed Interlocking System Using k-induction with RT-Tester. in Leveraging Applications of Formal Methods, Verification and Validation: Applications. Springer, Lecture Notes in Computer Science, vol. 12478, pp. 449-466, 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_29

Model Checking a Distributed Interlocking System Using k-induction with RT-Tester. / Pedersen, Signe Geisler; Haxthausen, Anne Elisabeth.
Leveraging Applications of Formal Methods, Verification and Validation: Applications. Springer, 2020. p. 449-466 (Lecture Notes in Computer Science, Vol. 12478).

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

TY - GEN

T1 - Model Checking a Distributed Interlocking System Using k-induction with RT-Tester

AU - Pedersen, Signe Geisler

AU - Haxthausen, Anne Elisabeth

PY - 2020

Y1 - 2020

N2 - This paper investigates the use of k-induction with RT-Tester for tackling the challenge of verifying the safety of a distributed railway interlocking system. For a real-world case study, it is described how a generic and reconfigurable model of the system is modelled in a new extension of the RAISE Specification Language (RSL). The generic model is instantiated with concrete data sets and subsequently model checked with respect to safety properties using the k-induction facilities in RT-Tester. The performance metrics of the verification with k-induction are additionally compared with the metrics of verifying the same system model with the SAL model checker.

AB - This paper investigates the use of k-induction with RT-Tester for tackling the challenge of verifying the safety of a distributed railway interlocking system. For a real-world case study, it is described how a generic and reconfigurable model of the system is modelled in a new extension of the RAISE Specification Language (RSL). The generic model is instantiated with concrete data sets and subsequently model checked with respect to safety properties using the k-induction facilities in RT-Tester. The performance metrics of the verification with k-induction are additionally compared with the metrics of verifying the same system model with the SAL model checker.

KW - Model checking

KW - RAISE

KW - Railway interlocking systems

KW - Distributed systems

KW - k-induction

KW - RT-Tester

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

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

M3 - Article in proceedings

SN - 978-3-030-61466-9

T3 - Lecture Notes in Computer Science

SP - 449

EP - 466

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 -

Model Checking a Distributed Interlocking System Using k-induction with RT-Tester

Abstract

Conference

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this