Automated generation of formal safety conditions from railway interlocking tables

Research output: Contribution to journalJournal articleResearchpeer-review

1045 Downloads (Orbit)

Abstract

This paper describes a tool for extracting formal safety conditions from interlocking tables for railway interlocking systems. The tool has been applied to generate safety conditions for the interlocking system at Stenstrup station in Denmark, and the SAL model checker tool has been used to check that these conditions were satisfied by a model of the relay circuits implementing the interlocking system at Stenstrup station.
Original languageEnglish
JournalInternational Journal on Software Tools for Technology Transfer
Volume16
Issue number6
Pages (from-to)713-726
ISSN1433-2779
DOIs
Publication statusPublished - 2014

Keywords

  • RAILROADS
  • Automatic train control
  • HASH(0x456fba0)
  • Railways
  • Interlocking systems
  • Formal methods
  • Safety
  • Verification
  • Model checking
  • Interlocking tables
  • Signal control tables

Fingerprint

Dive into the research topics of 'Automated generation of formal safety conditions from railway interlocking tables'. Together they form a unique fingerprint.

Cite this