{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:37Z","timestamp":1773827497305,"version":"3.50.1"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,8,10]],"date-time":"2021-08-10T00:00:00Z","timestamp":1628553600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Deutche Forchungsgemeinschaft","award":["407708394"],"award-info":[{"award-number":["407708394"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In this paper, an efficient approach to data validation of\ndistributed geographical interlocking systems (IXLs) is presented.\nIn the distributed IXL paradigm, track elements are controlled by\nlocal computers communicating with other control components over\nlocal and wide area networks. The overall control logic is\ndistributed over these track-side computers and remote server\ncomputers that may even reside in one or more cloud server farms.\nRedundancy is introduced to ensure fail-safe behaviour,\nfault-tolerance, and to increase the availability of the overall\nsystem. To cope with the configuration-related complexity of such\ndistributed IXLs, the software is designed according to the digital\ntwin paradigm: physical track elements are associated with software\nobjects implementing supervision and control for the element. The\nobjects communicate with each other and with high-level IXL control\ncomponents in the cloud over logical channels realised by\ndistributed communication mechanisms. The objective of this article\nis to explain  how configuration rules for this type of IXLs can be\nspecified by temporal logic formulae interpreted on Kripke Structure\nrepresentations of the IXL configuration. Violations of\nconfiguration rules can be specified using formulae from a\nwell-defined subset of LTL. By decomposing the complete\nconfiguration model into sub-models corresponding to routes\nthrough the model, the LTL model checking problem can be transformed\ninto a CTL checking problem for which highly efficient algorithms\nexist. Specialised rule violation queries that are hard to express\nin LTL can be simplified and checked faster by performing sub-model\ntransformations adding auxiliary variables to the states of the\nunderlying Kripke Structures. Further performance enhancements are\nachieved by checking each sub-model concurrently. The approach\npresented here has been implemented in a model checking tool which\nis applied by Siemens Mobility for data validation of geographical\nIXLs.<\/jats:p>","DOI":"10.1007\/s00165-021-00551-6","type":"journal-article","created":{"date-parts":[[2021,8,10]],"date-time":"2021-08-10T03:50:26Z","timestamp":1628567426000},"page":"925-955","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Efficient data validation for geographical interlocking systems"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3667-9775","authenticated-orcid":false,"given":"Jan","family":"Peleska","sequence":"first","affiliation":[{"name":"Department of Mathematics and Computer Science, University of Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Niklas","family":"Krafczyk","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, University of Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7349-8872","authenticated-orcid":false,"given":"Anne E.","family":"Haxthausen","sequence":"additional","affiliation":[{"name":"DTU Compute, Technical University of Denmark, Kongens Lyngby, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralf","family":"Pinger","sequence":"additional","affiliation":[{"name":"Siemens Mobility GmbH, Brunswick, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Behm P Benoit P Faivre A Meynadier J-M (1999) M\u00e9t\u00e9or: A successful application of B in a large project. In: Wing JM Woodcock J Davies J (eds) FM'99\u2014Formal methods world congress on formal methods in the development of computing systems. Toulouse France September 20\u201324 1999 Proceedings Volume I volume 1708 of lecture notes in computer science. Springer pp 369\u2013387","DOI":"10.1007\/3-540-48119-2_22"},{"key":"e_1_2_1_2_2_2","unstructured":"Badeau F Doche-Petit M (2012) Formal data validation with event-B. arXiv:1210.7039 [cs] October"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Biere A Heljanko K Junttila T Latvala T Schuppan V (2006) Linear encodings of bounded LTL model checking. Log Methods Comput Sci 2(5) November. arXiv: cs\/0611029","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"e_1_2_1_2_4_2","unstructured":"Bj\u00f8rner D (2003) New results and current trends in formal techniques for the development of software for transportation systems. In: Proceedings of the symposium on formal methods for railway operation and control systems (FORMS'2003) Budapest\/Hungary. L'Harmattan Hongrie May 15\u201316"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Basile D ter Beek MH Fantechi A Gnesi SM Piattino FA Trentini D Ferrari A (2018) On the industrial uptake of formal methods in the railway domain. In: Furia CA Winter K (eds) Integrated formal methods lecture notes in computer science. Springer International Publishing pp 20\u201329","DOI":"10.1007\/978-3-319-98938-9_2"},{"key":"e_1_2_1_2_6_2","unstructured":"CENELEC (2011) EN 50128:2011 railway applications\u2014communication signalling and processing systems\u2014software for railway control and protection systems"},{"key":"e_1_2_1_2_7_2","volume-title":"Model checking","author":"Clarke EM","year":"1999","unstructured":"ClarkeEMGrumbergOPeledDAModel checking1999CambridgeThe MIT Press1423.68002"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s40534-016-0119-1"},{"key":"e_1_2_1_2_9_2","volume-title":"Introduction to algorithms","author":"Cormen TH","year":"2009","unstructured":"CormenTHLeisersonCERivestRLSteinCIntroduction to algorithms20093The MIT Press1187.68679","edition":"3"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Fantechi A (2012) Distributing the challenge of model checking interlocking control tables. In: Margaria T Steffen B (eds) Leveraging applications of formal methods verification and validation. Applications and case studies volume 7610 of lecture notes in computer science. Springer Berlin pp 276\u2013289","DOI":"10.1007\/978-3-642-34032-1_26"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Fantechi A Fokkink W Morzenti A (2012) Some trends in formal methods applications to railway signaling. In: Formal methods for industrial critical systems. Wiley pp 61\u201384","DOI":"10.1002\/9781118459898.ch4"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Fredj M Leger S Feliachi A Ordioni J (2017) OVADO. In: Fantechi A Lecomte T Romanovsky A (eds) Reliability safety and security of railway systems. Modelling analysis verification and certification lecture notes in computer science. Springer International Publishing pp 87\u201398","DOI":"10.1007\/978-3-319-68499-4_6"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Ferrari A Magnani G Grasso D Fantechi A (2011) Model checking interlocking control tables. In: Schnieder E Tarnai G (eds) Proceedings of formal methods for automation and safety in railway and automotive systems (FORMS\/FORMAT 2010) Braunschweig Germany. Springer","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"e_1_2_1_2_14_2","first-page":"277","volume-title":"Formal methods\u201322nd international symposium, FM 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 15\u201317, 2018, Proceedings","author":"Geisler S","year":"2018","unstructured":"GeislerSHaxthausenAEHavelundKPeleskaJRoscoeBde VinkEPStepwise development and model checking of a distributed interlocking system\u2013using RAISEFormal methods\u201322nd international symposium, FM 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 15\u201317, 2018, Proceedings2018Springer277293"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.05.010"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Haxthausen AE \u00d8stergaard PH (2016) On the use of static checking in the verification of interlocking systems. In: Leveraging applications of formal methods verification and validation: discussion dissemination applications Part II volume 9953 of lecture notes in computer science. Springer International Publishing AG pp 266\u2013278","DOI":"10.1007\/978-3-319-47169-3_19"},{"key":"e_1_2_1_2_17_2","first-page":"205","volume-title":"SEFM workshops","author":"Haxthausen AE","year":"2013","unstructured":"HaxthausenAEPeleskaJPingerRCounsellSN\u00fa\u00f1ezMApplied bounded model checking for interlocking system designsSEFM workshops2013Springer205220"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Hansen D Schneider D Leuschel M (2016) Using B and ProB for data validation projects. In: Butler M Schewe K-D Mashkoor A Biro M (eds) Abstract state machines alloy B TLA VDM and Z lecture notes in computer science. Springer International Publishing pp 167\u2013182","DOI":"10.1007\/978-3-319-33600-8_10"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0304-7"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Keming W Zheng W Chuandong Z (2019) Formal modeling and data validation of general railway interlocking system. WIT Trans Built Environ 181","DOI":"10.2495\/CR180471"},{"key":"e_1_2_1_2_21_2","unstructured":"Lecomte T Burdy L Leuschel M (2012) Formally checking large data sets in the railways. CoRR abs\/1210.6815"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Laroussinie F Meyer A Petonnet E (2010) Counting LTL. In: Markey N Wijsen J (eds) TIME 2010\u201417th international symposium on temporal representation and reasoning Paris France 6\u20138 September 2010. IEEE Computer Society pp 51\u201358","DOI":"10.1109\/TIME.2010.20"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/978-3-642-39611-3_20","volume-title":"Hardware and software: verification and testing","author":"Moller F","year":"2013","unstructured":"MollerFNguyenHNRoggenbachMSchneiderSTreharneHBiereANahirAVosTDefining and model checking abstractions of complex railway models using CSP\u2016BHardware and software: verification and testing2013BerlinSpringer19320810.1007\/978-3-642-39611-3_20"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_2_1_2_25_2","unstructured":"Pachl J (2002) Railway operation and control. VTD Rail Publishing January"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1007\/978-3-030-61467-6_28","volume-title":"Leveraging applications of formal methods, verification and validation:applications\u20139th international symposium on leveraging applications of formal methods, ISoLA 2020, Rhodes, Greece, October 20\u201330, 2020, Proceedings, Part III","author":"Peleska J","year":"2020","unstructured":"PeleskaJMargariaTSteffenBNew distribution paradigms for railway interlockingLeveraging applications of formal methods, verification and validation:applications\u20139th international symposium on leveraging applications of formal methods, ISoLA 2020, Rhodes, Greece, October 20\u201330, 2020, Proceedings, Part III2020Springer43444810.1007\/978-3-030-61467-6_28"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Peleska J Krafczyk N Haxthausen AE Pinger R (2019) Efficient data validation for geographical interlocking systems. In: Dutilleul SC Lecomte T Romanovsky AB (eds) Reliability safety and security of railway systems. Modelling analysis verification and certification\u2014third international conference RSSRail 2019 Lille France June 4\u20136 2019 Proceedings volume 11495 of lecture notes in computer science. Springer pp 142\u2013158","DOI":"10.1007\/978-3-030-18744-6_9"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211865"},{"key":"e_1_2_1_2_29_2","unstructured":"Steffens S Siemens Mobility GmbH (2018) Safety@COTS multicore distributed smart safe system DS3. In: Innovationstag ETCS stellwerk smartrail 4.0. Presentation Slides pp 35\u201347"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Winter K (2012) Symbolic model checking for interlocking systems. In: Railway safety reliability and security: technologies and system engineering. IGI Global pp 298\u2013315","DOI":"10.4018\/978-1-4666-1643-1.ch013"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00551-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-021-00551-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00551-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00551-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,21]],"date-time":"2022-04-21T20:46:26Z","timestamp":1650573986000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-021-00551-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":30,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["10.1007\/s00165-021-00551-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-021-00551-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12]]},"assertion":[{"value":"30 August 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 March 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 May 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 August 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}