Conference paper · Book chapter
Efficient Data Validation for Geographical Interlocking Systems
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.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2019 |
Pages: | 142-158 |
Proceedings: | International Conference on Reliability, Safety, and Security of Railway Systems |
Series: | Lecture Notes in Computer Science |
Journal subtitle: | Third International Conference, Rssrail 2019, Lille, France, June 4–6, 2019, Proceedings |
ISBN: | 3030187438 , 3030187446 , 9783030187439 and 9783030187446 |
ISSN: | 03029743 and 16113349 |
Types: | Conference paper and Book chapter |
DOI: | 10.1007/978-3-030-18744-6_9 |
ORCIDs: | Haxthausen, Anne Elisabeth and 0000-0002-4076-3331 |