Efficient data validation for geographical interlocking systems

• Published in: Formal aspects of computing 2021-12, Vol.33 (6), p.925-955
• Main Authors: Peleska, Jan, Krafczyk, Niklas, Haxthausen, Anne E., Pinger, Ralf
• Format: Article
• Language: English
• Subjects: Algorithms; Cloud computing; Communication; Computer Science; Configurations; Fault tolerance; Geographical distribution; Locking; Math Applications in Computer Science; Original Article; Redundancy; Servers; Software; Temporal logic; Theory of Computation; Wide area networks
• ISSN: 0934-5043; 1433-299X
• DOI: 10.1007/s00165-021-00551-6

In this paper, an efficient approach to data validation of distributed geographical interlocking systems (IXLs) is presented. In the distributed IXL paradigm, track elements are controlled by local computers communicating with other control components over local and wide area networks. The overall control logic is distributed over these track-side computers and remote server computers that may even reside in one or more cloud server farms. Redundancy is introduced to ensure fail-safe behaviour, fault-tolerance, and to increase the availability of the overall system. To cope with the configuration-related complexity of such distributed IXLs, the software is designed according to the digital twin paradigm: physical track elements are associated with software objects implementing supervision and control for the element. The objects communicate with each other and with high-level IXL control components in the cloud over logical channels realised by distributed communication mechanisms. The objective of this article is to explain how configuration rules for this type of IXLs can be specified by temporal logic formulae interpreted on Kripke Structure representations of the IXL configuration. Violations of configuration rules can be specified using formulae 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 Mobility for data validation of geographical IXLs.