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

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

65 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 languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation: Applications
PublisherSpringer
Publication date2020
Pages449-466
ISBN (Print)978-3-030-61466-9
DOIs
Publication statusPublished - 2020
EventInternational Symposium On Leveraging Applications of Formal Methods, Verification and Validation 2020 - Virtual event - POSTPONED TO 2021!, Greece
Duration: 20 Oct 202030 Oct 2020
http://www.isola-conference.org/

Conference

ConferenceInternational Symposium On Leveraging Applications of Formal Methods, Verification and Validation 2020
LocationVirtual event - POSTPONED TO 2021!
Country/TerritoryGreece
Period20/10/202030/10/2020
OtherPostponed to October 2021 due to Covid-19
Internet address
SeriesLecture Notes in Computer Science
Volume12478
ISSN0302-9743

Keywords

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

Fingerprint

Dive into the research topics of 'Model Checking a Distributed Interlocking System Using k-induction with RT-Tester'. Together they form a unique fingerprint.

Cite this