Efficient data validation for geographical interlocking systems

Autor: Jan Peleska, Niklas Krafczyk, Anne E. Haxthausen, Ralf Pinger
Rok vydání: 2021
Předmět:
Zdroj: Peleska, J, Krafczyk, N, Haxthausen, A E & Pinger, R 2021, ' Efficient data validation for geographical interlocking systems ', Formal Aspects of Computing . https://doi.org/10.1007/s00165-021-00551-6
ISSN: 1433-299X
0934-5043
DOI: 10.1007/s00165-021-00551-6
Popis: 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.
Databáze: OpenAIRE
Externí odkaz: