Conference paper · Book chapter
Model Checking a Distributed Interlocking System Using k-induction with RT-Tester
In
Lecture Notes in Computer Science
—
2020, pp. 449-466
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.
| Language: | English |
|---|---|
| Publisher: | Springer |
| Year: | 2020 |
| Pages: | 449-466 |
| Proceedings: | International Symposium On Leveraging Applications of Formal Methods, Verification and Validation 2020 |
| Series: | Lecture Notes in Computer Science |
| ISBN: | 3030614662 , 3030614670 , 9783030614669 and 9783030614676 |
| ISSN: | 03029743 and 16113349 |
| Types: | Conference paper and Book chapter |
| DOI: | 10.1007/978-3-030-61467-6_29 |
| ORCIDs: | Pedersen, Signe Geisler and Haxthausen, Anne Elisabeth |
