Efficient data validation for geographical interlocking systems

Abstract

In this paper, an efficient approach to data validation ofdistributed geographical interlocking systems (IXLs) is presented.In the distributed IXL paradigm, track elements are controlled bylocal computers communicating with other control components overlocal and wide area networks. The overall control logic isdistributed over these track-side computers and remote servercomputers 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 overallsystem. To cope with the configuration-related complexity of suchdistributed IXLs, the software is designed according to the digitaltwin paradigm: physical track elements are associated with softwareobjects implementing supervision and control for the element. Theobjects communicate with each other and with high-level IXL controlcomponents in the cloud over logical channels realised bydistributed communication mechanisms. The objective of this articleis to explain how configuration rules for this type of IXLs can bespecified by temporal logic formulae interpreted on Kripke Structurerepresentations of the IXL configuration. Violations ofconfiguration rules can be specified using formulae from awell-defined subset of LTL. By decomposing the completeconfiguration model into sub-models corresponding to routesthrough the model, the LTL model checking problem can be transformedinto a CTL checking problem for which highly efficient algorithmsexist. Specialised rule violation queries that are hard to expressin LTL can be simplified and checked faster by performing sub-modeltransformations adding auxiliary variables to the states of theunderlying Kripke Structures. Further performance enhancements areachieved by checking each sub-model concurrently. The approachpresented here has been implemented in a model checking tool whichis applied by Siemens Mobility for data validation of geographicalIXLs.