Stepwise development and model checking of a distributed interlocking system using RAISE

S. Geisler*, A. E. Haxthausen

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

This paper considers the challenge of designing and verifying control protocols for geographically distributed railway interlocking systems. It describes how this challenge can be tackled by stepwise development and model checking of state transition system models in a new extension of the RAISE Specification Language. Railway interlocking systems are reconfigurable systems which can be configured by supplying data describing the network to be controlled and other details. Therefore, such systems are natural candidates for being modelled by generic state transition systems, which abstract away from the concrete configuration at the time of modelling, and can later be instantiated with concrete data. For a real-world case study, a generic state transition system is developed in steps, starting with an abstract model of the essential system behaviour and incrementally adding details and restrictions. The stepwise development method allows different variants of the control protocol to be explored. The generic models are instantiated with concrete configuration data, after which desired properties, in particular safety properties, of the system models are verified using model checking.

Original languageEnglish
JournalFormal Aspects of Computing
Pages (from-to)1-39
ISSN0934-5043
DOIs
Publication statusPublished - 1 Jan 2020

Keywords

  • Distributed systems
  • Model checking
  • Railway interlocking systems
  • RAISE
  • Stepwise development

Fingerprint Dive into the research topics of 'Stepwise development and model checking of a distributed interlocking system using RAISE'. Together they form a unique fingerprint.

Cite this