Efficient Data Validation for Geographical Interlocking Systems

Jan Peleska*, Niklas Krafczyk, Anne Elisabeth Haxthausen, Ralf Pinger

*Corresponding author for this work

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

174 Downloads (Pure)


In this paper, an efficient approach to data validation of geographical interlocking systems (IXLs) is presented. It is explained how configuration rules for IXLs can be specified by temporal logic formulas interpreted on Kripke structure representations of the IXL configuration. Violations of configuration rules can be specified using formulas from a well-defined subset of LTL. By decomposing the complete configuration model into sub-models corresponding to routes through the model, the LTL model checking problem can be transformed into a CTL checking problem for which highly efficient algorithms exist. Specialised rule violation queries that are hard to express in LTL can be simplified and checked faster by performing sub-model transformations adding auxiliary variables to the states of the underlying Kripke structures. Further performance enhancements are achieved by checking each sub-model concurrently. The approach presented here has been implemented in a model checking tool which is applied by Siemens for data validation of geographical IXLs.
Original languageEnglish
Title of host publicationProceedings of 2019 International Conference on Reliability, Safety, and Security of Railway Systems
Publication date2019
ISBN (Print)9783030187446
Publication statusPublished - 2019
EventInternational Conference on Reliability, Safety, and Security of Railway Systems - Lille Grand Palais, Lille , France
Duration: 4 Jun 20196 Jun 2019


ConferenceInternational Conference on Reliability, Safety, and Security of Railway Systems
LocationLille Grand Palais
SeriesLecture Notes in Computer Science


  • Data validation
  • Interlocking systems
  • LTL
  • CTL
  • Model checking

Fingerprint Dive into the research topics of 'Efficient Data Validation for Geographical Interlocking Systems'. Together they form a unique fingerprint.

Cite this