{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T21:13:30Z","timestamp":1792185210056,"version":"4.4.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,1,12]],"date-time":"2023-01-12T00:00:00Z","timestamp":1673481600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2023,3,31]]},"abstract":"<jats:p>Model checking techniques have often been applied to the verification of railway interlocking systems, responsible for guiding trains safely through a given railway network. However, these techniques fail to scale to the interlocking systems controlling large stations, composed of hundreds and even thousands of controlled entities, due to the state space explosion problem. Indeed, interlocking systems exhibit a certain degree of locality that allows some reasoning only on the mere set of entities that regard the train movements, but safe routing through a complex station layout requires a global reservation policy, which can require global state conditions to be taken into account.<\/jats:p>\n          <jats:p>In this article, we present a compositional approach aimed at chopping the verification of a large interlocking system into that of smaller fragments, exploiting in each fragment a proper abstraction of the global information on routing state. A proof is given of the thesis that verifying the safety of the smaller fragments is sufficient to verify the safety of the whole network. Experiments using this compositional approach have shown important gains in performance of the verification, as well as in the size of affordable station layouts.<\/jats:p>","DOI":"10.1145\/3549736","type":"journal-article","created":{"date-parts":[[2022,7,21]],"date-time":"2022-07-21T12:16:41Z","timestamp":1658405801000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Compositional Verification of Railway Interlocking Systems"],"prefix":"10.1145","volume":"35","author":[{"given":"Anne Elisabeth","family":"Haxthausen","sequence":"first","affiliation":[{"name":"DTU Compute, Technical University of Denmark, Lyngby, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[{"name":"DINFO, University of Florence, Firenze, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,12]]},"reference":[{"key":"e_1_3_5_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3054-3_33"},{"key":"e_1_3_5_3_2","volume-title":"Principles of model checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press."},{"key":"e_1_3_5_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.04.004"},{"key":"e_1_3_5_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693137"},{"key":"e_1_3_5_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49646-7_22"},{"key":"e_1_3_5_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_5_8_2","volume-title":"EN 50128:2011\u2014Railway Applications\u2014Communications, Signalling and Processing Systems\u2014Software for Railway Control and Protection Systems","author":"Standardization CENELEC European Committee for Electrotechnical","year":"2011","unstructured":"CENELEC European Committee for Electrotechnical Standardization. 2011. EN 50128:2011\u2014Railway Applications\u2014Communications, Signalling and Processing Systems\u2014Software for Railway Control and Protection Systems."},{"key":"e_1_3_5_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-05814-1_1"},{"key":"e_1_3_5_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66197-1_15"},{"key":"e_1_3_5_11_2","first-page":"107","volume-title":"FORMS\/FORMAT 2010\u2014Formal Methods for Automation and Safety in Railway and Automotive Systems","author":"Ferrari Alessio","year":"2010","unstructured":"Alessio Ferrari, Gianluca Magnani, Daniele Grasso, and Alessandro Fantechi. 2010. Model checking interlocking control tables. In FORMS\/FORMAT 2010\u2014Formal Methods for Automation and Safety in Railway and Automotive Systems. Eckehard Schnieder and G\u00e9za Tarnai (Eds.). Springer, 107\u2013115."},{"key":"e_1_3_5_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_12"},{"key":"e_1_3_5_13_2","first-page":"225","volume-title":"Formal Methods for Components and Objects (Lecture Notes in Computer Science)","author":"Hansen Helle Hvid","year":"2010","unstructured":"Helle Hvid Hansen, Jeroen Ketema, Bas Luttik, Mohammad Reza Mousavi, Jaco van de Pol, and Osmar Marchi dos Santos. 2010. Automated verification of executable UML models. In Formal Methods for Components and Objects (Lecture Notes in Computer Science), Bernhard K. Aichernig, Frank S. de Boer, and Marcello M. Bonsangue (Eds.), Vol. 6957. Springer, 225\u2013250."},{"key":"e_1_3_5_14_2","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/978-3-642-12566-9_8","volume-title":"Foundations of Computer Software, Future Trends and Techniques for Development (Lecture Notes in Computer Science)","author":"Haxthausen Anne E.","year":"2010","unstructured":"Anne E. Haxthausen, Marie Le Bliguet, and Andreas A. Kj\u00e6r. 2010. Modelling and verification of relay interlocking systems. In Foundations of Computer Software, Future Trends and Techniques for Development (Lecture Notes in Computer Science), Christine Choppy and Oleg Sokolsky (Eds.), Vol. 6028. Springer, 141\u2013153."},{"key":"e_1_3_5_15_2","volume-title":"Proof of Completeness of Compositional Verification of Interlocking Systems","author":"Haxthausen Anne E.","year":"2022","unstructured":"Anne E. Haxthausen and Alessandro Fantechi. 2022. Proof of Completeness of Compositional Verification of Interlocking Systems. Technical Report. Retrieved fromhttp:\/\/www.imm.dtu.dk\/aeha\/RobustRailS\/data\/compositionalmethod\/completeness.pdf."},{"key":"e_1_3_5_16_2","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/978-3-319-47169-3_19","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, Part II (Lecture Notes in Computer Science)","author":"Haxthausen Anne E.","year":"2016","unstructured":"Anne E. Haxthausen and Peter H. \u00d8stergaard. 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 (Lecture Notes in Computer Science), Vol. 9953. Springer, 266\u2013278."},{"key":"e_1_3_5_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-05032-4_19"},{"key":"e_1_3_5_18_2","first-page":"210","volume-title":"Proceedings of the FORMS\/FORMAT 2014\u201410th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems","author":"James Philip","year":"2014","unstructured":"Philip James, Faron M\u00f6ller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, and Helen Treharne. 2014. Decomposing scheme plans to manage verification complexity. In Proceedings of the FORMS\/FORMAT 2014\u201410th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems. Institute for Traffic Safety and Automation Engineering, Technische Universit\u00e4t Braunschweig, 210\u2013220."},{"key":"e_1_3_5_19_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-319-05032-4_15","volume-title":"Software Engineering and Formal Methods","author":"James Philip","year":"2014","unstructured":"Philip James, Faron M\u00f6ller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, Helen Treharne, Matthew Trumble, and David Williams. 2014. Verification of scheme plans using CSP \\( | \\) \\( | \\) B. In Software Engineering and Formal Methods. Steve Counsell and Manuel N\u00fa\u00f1ez (Eds.). Lecture Notes in Computer Science, Vol. 8368. Springer, 189\u2013204."},{"key":"e_1_3_5_20_2","volume-title":"Formal Verification of Railway Interlocking Systems","author":"Limbr\u00e9e Christophe","year":"2019","unstructured":"Christophe Limbr\u00e9e. 2019. Formal Verification of Railway Interlocking Systems. Ph.D. Dissertation. Catholic University of Louvain, Louvain-la-Neuve, Belgium."},{"key":"e_1_3_5_21_2","volume-title":"Reliability, Safety and Security of Railway Systems\u2014RSSR 2016 (Lecture Notes in Computer Science)","author":"Limbr\u00e9e Christophe","year":"2016","unstructured":"Christophe Limbr\u00e9e, Quentin Pecheur, Charles Moller, and Stefano Tonetta. 2016. Verification of railway interlocking\u2014Compositional approach with OCRA. In Reliability, Safety and Security of Railway Systems\u2014RSSR 2016 (Lecture Notes in Computer Science), Thierry Lecomte, Ralf Pinger, and Alexander Romanovsky (Eds.), Vol. 9707. Springer."},{"key":"e_1_3_5_22_2","first-page":"279","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation, Part II (Lecture Notes in Computer Science)","author":"Macedo Hugo D.","year":"2016","unstructured":"Hugo D. Macedo, Alessandro Fantechi, and Anne E. Haxthausen. 2016. Compositional verification of multi-station interlocking systems. In Leveraging Applications of Formal Methods, Verification and Validation, Part II (Lecture Notes in Computer Science), Tiziana Margaria and Bernhard Steffen (Eds.), Vol. 9953. Springer, 279\u2013293."},{"key":"e_1_3_5_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_11"},{"key":"e_1_3_5_24_2","volume-title":"Railway Operation and Control","author":"Pachl J\u00f6rn","year":"2002","unstructured":"J\u00f6rn Pachl. 2002. Railway Operation and Control. VTD Rail Publishing."},{"key":"e_1_3_5_25_2","series-title":"8th Workshop on Model-Based Testing, Rome, Italy","first-page":"3","volume":"111","author":"Peleska Jan","year":"2013","unstructured":"Jan Peleska. 2013. Industrial-strength model-based testing\u2014State of the art and current challenges. In 8th Workshop on Model-Based Testing, Rome, Italy(Electronic Proceedings in Theoretical Computer Science), Alexander K. Petrenko and Holger Schlingloff (Eds.), Vol. 111. Open Publishing Association, 3\u201328."},{"key":"e_1_3_5_26_2","first-page":"298","volume-title":"NASA Formal Methods (Lecture Notes in Computer Science)","author":"Peleska Jan","year":"2011","unstructured":"Jan Peleska, Elena Vorobev, and Florian Lapschies. 2011. Automated test case generation with SMT-solving and abstract interpretation. In NASA Formal Methods (Lecture Notes in Computer Science), M. Bobaru, K. Havelund, G. Holzmann, and Joshi (Eds.), Vol. 6617. Springer, 298\u2013312."},{"key":"e_1_3_5_27_2","volume-title":"Railway Signalling & Interlocking: International Compendium","author":"Theeg Gregor","year":"2009","unstructured":"Gregor Theeg, Sergej Vlasenko, Eds, 2009. Railway Signalling & Interlocking: International Compendium. Eurailpress."},{"key":"e_1_3_5_28_2","volume-title":"RT-Tester Model-Based Test Case and Test Data Generator - RTT-MBT - User Manual","author":"GmbH Verified Systems International","year":"2013","unstructured":"Verified Systems International GmbH. 2013. RT-Tester Model-Based Test Case and Test Data Generator - RTT-MBT - User Manual. Retrieved from http:\/\/www.verified.de."},{"key":"e_1_3_5_29_2","volume-title":"Formal Development and Verification of Railway Control Systems\u2014In the Context of ERTMS\/ETCS Level 2","author":"Vu Linh Hong","year":"2015","unstructured":"Linh Hong Vu. 2015. Formal Development and Verification of Railway Control Systems\u2014In the Context of ERTMS\/ETCS Level 2. Ph.D. Dissertation. Technical University of Denmark, DTU Compute."},{"key":"e_1_3_5_30_2","first-page":"200","volume-title":"FORMS\/FORMAT 2014\u201410th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems","author":"Vu Linh H.","year":"2014","unstructured":"Linh H. Vu, Anne E. Haxthausen, and Jan Peleska. 2014. A domain-specific language for railway interlocking systems. In FORMS\/FORMAT 2014\u201410th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems. Eckehard Schnieder and G\u00e9za Tarnai (Eds.). Institute for Traffic Safety and Automation Engineering, Technische Universit\u00e4t Braunschweig, 200\u2013209."},{"key":"e_1_3_5_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68499-4_7"},{"key":"e_1_3_5_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.05.010"},{"key":"e_1_3_5_33_2","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/978-3-642-34032-1_24","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (Lecture Notes in Computer Science)","author":"Winter Kirsten","year":"2012","unstructured":"Kirsten Winter. 2012. Optimising ordering strategies for symbolic model checking of railway interlockings. In Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (Lecture Notes in Computer Science), Tiziana Margaria and Bernhard Steffen (Eds.), Vol. 7610. Springer, 246\u2013260."},{"key":"e_1_3_5_34_2","volume-title":"Railway Safety, Reliability, and Security: Technologies and Systems Engineering","author":"Winter K.","year":"2012","unstructured":"K. Winter. 2012. Symbolic model checking for interlocking systems. In Railway Safety, Reliability, and Security: Technologies and Systems Engineering. Francesco Flammini (Ed.). IGI Global."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3549736","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3549736","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:12Z","timestamp":1750186812000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3549736"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,12]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3,31]]}},"alternative-id":["10.1145\/3549736"],"URL":"https:\/\/doi.org\/10.1145\/3549736","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,12]]},"assertion":[{"value":"2021-12-21","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-06","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}