{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:19Z","timestamp":1750309519193,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T00:00:00Z","timestamp":1743811200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"German Federal Ministry for Economic Affairs and Energy","award":["20X1908E"],"award-info":[{"award-number":["20X1908E"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,6,30]]},"abstract":"<jats:p>We present a distributed railway interlocking (IXL) method based on trains communicating with switch boxes deployed along the railway network for switching points and monitoring the occupancy states of track elements. The method does not require any centralised IXL components. A distributed architecture is proposed that carefully separates the overall business logic and automated train operation from the safety-critical automated train protection and distributed IXL logic. This architecture is also suitable for autonomous trains traversing the railway network. The safety of the IXL logic is formally proven, using the Isabelle\/HOL proof assistant. Experiments confirm that this proof-based approach is superior to model checking approaches, since the model checking effort grows exponentially with the size of the railway network. In contrast to this, the mathematical safety proof is performed once and for all railway networks fulfilling a realistic well-formedness condition. For a concrete network, only the well-formedness of the network and its initial train placements has to be verified, whereas the safety of the dynamic behaviour is a consequence of the network-independent safety proof.<\/jats:p>","DOI":"10.1145\/3706425","type":"journal-article","created":{"date-parts":[[2024,11,30]],"date-time":"2024-11-30T10:21:08Z","timestamp":1732962068000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Mechanised Safety Verification for a Distributed Autonomous Railway Control System"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5514-7593","authenticated-orcid":false,"given":"Robert","family":"Sachtleben","sequence":"first","affiliation":[{"name":"Verified Systems International GmbH, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7349-8872","authenticated-orcid":false,"given":"Anne","family":"Haxthausen","sequence":"additional","affiliation":[{"name":"DTU Compute, Technical University of Denmark, Lyngby, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3667-9775","authenticated-orcid":false,"given":"Jan","family":"Peleska","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Bremen, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,5]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-05814-1_10"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32872-6_14"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98938-9_2"},{"volume-title":"EN 50128:2011 Railway Applications - Communication, Signalling and Processing Systems - Software for Railway Control and Protection Systems","year":"2011","key":"e_1_3_3_6_2","unstructured":"CENELEC. 2011. EN 50128:2011 Railway Applications - Communication, Signalling and Processing Systems - Software for Railway Control and Protection Systems. European Committee for Electrotechnical Standardization."},{"key":"e_1_3_3_7_2","volume-title":"Proceedings of 11th World Congress on Railway Research (WCRR\u201916)","author":"Fantechi Alessandro","year":"2016","unstructured":"Alessandro Fantechi, Stefania Gnesi, Anne Haxthausen, Jaco van de Pol, Marco Roveri, and Helen Treharne. 2016. SaRDIn - A safe reconfigurable distributed interlocking. In Proceedings of 11th World Congress on Railway Research (WCRR\u201916). Ferrovie dello Stato Italiane, Milano."},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19762-8_19"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00244-2_4"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/PDP.2017.66"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3520480"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-05814-1_14"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_29"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-020-00507-2"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2306.14814"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2203.08917"},{"key":"e_1_3_3_18_2","unstructured":"Verified Systems International GmbH. Web page visited 2023-07-11. RT-Tester. https:\/\/www.verified.de\/products\/rt-tester\/"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.879808"},{"key":"e_1_3_3_21_2","volume-title":"The SPIN Model Checker: Primer and Reference Manual (First ed.)","author":"Holzmann Gerard","year":"2003","unstructured":"Gerard Holzmann. 2003. The SPIN Model Checker: Primer and Reference Manual (First ed.). Addison-Wesley Professional."},{"key":"e_1_3_3_22_2","volume-title":"EULYNX System Definition, Version 4.2","author":"Initiative EULYNX","year":"2023","unstructured":"EULYNX Initiative. 2023. EULYNX System Definition, Version 4.2. https:\/\/eulynx.eu\/storage\/simple-file-list\/General-Documents\/Baseline-set-4-Release-2\/20230627-EULYNX-System-Definition-Eu_Doc_7-v4_2-0_A.pdf"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000140"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/SACI.2016.7507347"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_27"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2011.12.010"},{"key":"e_1_3_3_27_2","unstructured":"Sam Owre and N. Shankar. 2001. Symbolic Analysis Laboratory. http:\/\/sal.csl.sri.com"},{"key":"e_1_3_3_28_2","volume-title":"Railway Signalling Principles","author":"Pachl J\u00f6rn","year":"2021","unstructured":"J\u00f6rn Pachl. 2021. Railway Signalling Principles. Published under a CC BY-NC-ND 4.0 Licence. http:\/\/www.joernpachl.de\/eBook%20RSP.pdf"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_28"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19762-8_22"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-021-00551-6"},{"key":"e_1_3_3_32_2","volume-title":"The RAISE Specification Language","author":"Wagner The RAISE Language Group: Chris George, Peter Haff, Klaus Havelund, Anne E. Haxthausen, Robert Milne, Claus Bendix Nielsen, S\u00f8ren Prehn, and Kim Ritter","year":"1992","unstructured":"The RAISE Language Group: Chris George, Peter Haff, Klaus Havelund, Anne E. Haxthausen, Robert Milne, Claus Bendix Nielsen, S\u00f8ren Prehn, and Kim Ritter Wagner. 1992. The RAISE Specification Language. Prentice Hall Int."},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33951-1_2"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-021-00567-y"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.002"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/SYSOSE.2018.8428771"},{"key":"e_1_3_3_37_2","unstructured":"Uppsala University and Aalborg University. Web page visited 2023-07-11. UPPAAL. http:\/\/www.uppaal.org\/"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.05.010"},{"key":"e_1_3_3_39_2","volume-title":"Isabelle, Isar - A Versatile Environment for Human Readable Formal Proof Documents","author":"Wenzel Markus","year":"2002","unstructured":"Markus Wenzel. 2002. Isabelle, Isar - A Versatile Environment for Human Readable Formal Proof Documents. Ph. D. Dissertation. Technical University Munich, Germany. http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.pdf"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-74781-1_31"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3706425","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3706425","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:04Z","timestamp":1750295884000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3706425"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,5]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6,30]]}},"alternative-id":["10.1145\/3706425"],"URL":"https:\/\/doi.org\/10.1145\/3706425","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2025,4,5]]},"assertion":[{"value":"2023-08-29","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-02","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}