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

85 Downloads (Pure)

Abstract

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

Keywords

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

Cite this

Peleska, J., Krafczyk, N., Haxthausen, A. E., & Pinger, R. (2019). Efficient Data Validation for Geographical Interlocking Systems. In Proceedings of 2019 International Conference on Reliability, Safety, and Security of Railway Systems (pp. 142-158). Springer. Lecture Notes in Computer Science, Vol.. 11495 https://doi.org/10.1007/978-3-030-18744-6_9
Peleska, Jan ; Krafczyk, Niklas ; Haxthausen, Anne Elisabeth ; Pinger, Ralf. / Efficient Data Validation for Geographical Interlocking Systems. Proceedings of 2019 International Conference on Reliability, Safety, and Security of Railway Systems. Springer, 2019. pp. 142-158 (Lecture Notes in Computer Science, Vol. 11495).
@inproceedings{d12ef4ff1b304e95b5324bf46433d4a6,
title = "Efficient Data Validation for Geographical Interlocking Systems",
abstract = "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.",
keywords = "Data validation, Interlocking systems, LTL, CTL, Model checking",
author = "Jan Peleska and Niklas Krafczyk and Haxthausen, {Anne Elisabeth} and Ralf Pinger",
year = "2019",
doi = "10.1007/978-3-030-18744-6_9",
language = "English",
isbn = "9783030187446",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "142--158",
booktitle = "Proceedings of 2019 International Conference on Reliability, Safety, and Security of Railway Systems",

}

Peleska, J, Krafczyk, N, Haxthausen, AE & Pinger, R 2019, Efficient Data Validation for Geographical Interlocking Systems. in Proceedings of 2019 International Conference on Reliability, Safety, and Security of Railway Systems. Springer, Lecture Notes in Computer Science, vol. 11495, pp. 142-158, International Conference on Reliability, Safety, and Security of Railway Systems, Lille , France, 04/06/2019. https://doi.org/10.1007/978-3-030-18744-6_9

Efficient Data Validation for Geographical Interlocking Systems. / Peleska, Jan; Krafczyk, Niklas; Haxthausen, Anne Elisabeth; Pinger, Ralf.

Proceedings of 2019 International Conference on Reliability, Safety, and Security of Railway Systems. Springer, 2019. p. 142-158 (Lecture Notes in Computer Science, Vol. 11495).

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

TY - GEN

T1 - Efficient Data Validation for Geographical Interlocking Systems

AU - Peleska, Jan

AU - Krafczyk, Niklas

AU - Haxthausen, Anne Elisabeth

AU - Pinger, Ralf

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

KW - Data validation

KW - Interlocking systems

KW - LTL

KW - CTL

KW - Model checking

U2 - 10.1007/978-3-030-18744-6_9

DO - 10.1007/978-3-030-18744-6_9

M3 - Article in proceedings

SN - 9783030187446

T3 - Lecture Notes in Computer Science

SP - 142

EP - 158

BT - Proceedings of 2019 International Conference on Reliability, Safety, and Security of Railway Systems

PB - Springer

ER -

Peleska J, Krafczyk N, Haxthausen AE, Pinger R. Efficient Data Validation for Geographical Interlocking Systems. In Proceedings of 2019 International Conference on Reliability, Safety, and Security of Railway Systems. Springer. 2019. p. 142-158. (Lecture Notes in Computer Science, Vol. 11495). https://doi.org/10.1007/978-3-030-18744-6_9