Efficient Data Validation for Geographical Interlocking Systems

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedings – Annual report year: 2019Researchpeer-review

Documents

DOI

View graph of relations

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
PublisherSpringer
Publication date2019
Pages142-158
ISBN (Print)9783030187446
DOIs
Publication statusPublished - 2019
EventInternational Conference on Reliability, Safety, and Security of Railway Systems - Lille Grand Palais, Lille , France
Duration: 4 Jun 20196 Jun 2019

Conference

ConferenceInternational Conference on Reliability, Safety, and Security of Railway Systems
LocationLille Grand Palais
CountryFrance
CityLille
Period04/06/201906/06/2019
SeriesLecture Notes in Computer Science
Volume11495
ISSN0302-9743
CitationsWeb of Science® Times Cited: No match on DOI

    Research areas

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

Download statistics

No data available

ID: 180161706