{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T03:50:07Z","timestamp":1783741807933,"version":"3.55.0"},"reference-count":34,"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:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"EPSRC STRATA platform","award":["EP\/N023641\/1"],"award-info":[{"award-number":["EP\/N023641\/1"]}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA2386-17-1-4065"],"award-info":[{"award-number":["FA2386-17-1-4065"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]},{"name":"DISCONT Project of the French National Research Agency","award":["ANR-17-CE25-0005"],"award-info":[{"award-number":["ANR-17-CE25-0005"]}]}],"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>For years, formal methods have been successfully applied in the railway domain to formally demonstrate safety of railway systems. Despite that, little has been done in the field of formal methods to address the cyber-physical nature of modern railway signalling systems. In this article, we present an approach for a formal development of cyber-physical railway signalling systems that is based on a refinement-based modelling and proof-based verification. Our approach utilises the Event-B formal specification language together with a hybrid system and communication modelling patterns to developing a generic hybrid railway signalling system model that can be further refined to capture a specific railway signalling system. The main technical contribution of this article is the refinement of the hybrid train Event-B model with other railway signalling sub-systems. The complete model of the cyber-physical railway signalling system was formally proved to ensure a safe rolling stock separation and prevent their derailment. Furthermore, the article demonstrates the advantage of the refinement-based development approach of cyber-physical systems, which enables a problem decomposition and in turn reduction in the verification and modelling effort.<\/jats:p>","DOI":"10.1145\/3524052","type":"journal-article","created":{"date-parts":[[2022,8,27]],"date-time":"2022-08-27T10:26:28Z","timestamp":1661595988000},"page":"1-1","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A Refinement-based Formal Development of Cyber-physical Railway Signalling Systems"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4582-9712","authenticated-orcid":false,"given":"Yamine","family":"A\u00eft-Ameur","sequence":"first","affiliation":[{"name":"INPT\u2013ENSEEIHT, Toulouse, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0686-0365","authenticated-orcid":false,"given":"Sergiy","family":"Bogomolov","sequence":"additional","affiliation":[{"name":"Newcastle University, Newcastle upon Tyne, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9185-0515","authenticated-orcid":false,"given":"Guillaume","family":"Dupont","sequence":"additional","affiliation":[{"name":"INPT\u2013ENSEEIHT, Toulouse, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1153-9581","authenticated-orcid":false,"given":"Alexei","family":"Iliasov","sequence":"additional","affiliation":[{"name":"The Formal Route Limited, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4076-3331","authenticated-orcid":false,"given":"Alexander","family":"Romanovsky","sequence":"additional","affiliation":[{"name":"Newcastle University, Newcastle upon Tyne, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1301-4447","authenticated-orcid":false,"given":"Paulius","family":"Stankaitis","sequence":"additional","affiliation":[{"name":"Newcastle University, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,12]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_3_3_3_2","volume-title":"Modeling in Event-B: System and Software Engineering","author":"Abrial J.-R.","year":"2013","unstructured":"J.-R. Abrial. 2013. Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York, NY."},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038685"},{"key":"e_1_3_3_5_2","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-319-25942-0_4","volume-title":"Proceedings of the International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","author":"Babin G.","year":"2015","unstructured":"G. Babin, Y. A\u00eft-Ameur, S. Nakajima, and M. Pantel. 2015. Refinement and proof-based development of systems characterized by continuous functions. In Proceedings of the International Symposium on Dependable Software Engineering: Theories, Tools, and Applications. Springer, 55\u201370."},{"key":"e_1_3_3_6_2","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-52559-9_61","volume-title":"Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness","author":"Back R. J. R.","year":"1990","unstructured":"R. J. R. Back. 1990. Refinement calculus, part II: Parallel and reactive programs. In Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness, J. W. de Bakker, W. P. de Roever, and G. Rozenberg (Eds.). Springer, 67\u201393."},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/11415787_20"},{"key":"e_1_3_3_8_2","first-page":"161","article-title":"Cyber-physical systems","author":"Baheti Radhakisan","year":"2011","unstructured":"Radhakisan Baheti and Helen Gill. 2011. Cyber-physical systems. The Impact of Control Technology (2011), 161\u2013166. www.ieeecss.org.","journal-title":"The Impact of Control Technology"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.02.003"},{"key":"e_1_3_3_10_2","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"Proceedings of the Conference on Formal Methods (FM\u201999)","author":"Behm Patrick","year":"1999","unstructured":"Patrick Behm, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. 1999. M\u00e9t\u00e9or: A successful application of B in a large project. In Proceedings of the Conference on Formal Methods (FM\u201999), Jeannette M. Wing, Jim Woodcock, and Jim Davies (Eds.). Springer, Berlin, 369\u2013387."},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.10.011"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.3384\/ecp11063105"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2017.40"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39698-4_5"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_17"},{"key":"e_1_3_3_16_2","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/978-3-319-91271-4_11","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"Dupont Guillaume","year":"2018","unstructured":"Guillaume Dupont, Yamine A\u00eft-Ameur, Marc Pantel, and Neeraj Kumar Singh. 2018. Proof-based approach to hybrid systems development: Dynamic logic and Event-B. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, Michael Butler, Alexander Raschke, Thai Son Hoang, and Klaus Reichl (Eds.). Springer International Publishing, Cham, 155\u2013170."},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3448270"},{"key":"e_1_3_3_18_2","unstructured":"ERTMS User Group. 2002. UNISIG: ERTMS\/ETCS: System Requirements Specification v. 3.4.0."},{"key":"e_1_3_3_19_2","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/978-3-319-92970-5_4","volume-title":"Software Engineering and Formal Methods","author":"Golra Fahad Rafique","year":"2018","unstructured":"Fahad Rafique Golra, Fabien Dagnat, Jeanine Souqui\u00e8res, Imen Sayar, and Sylvain Guerin. 2018. Bridging the gap between informal requirements and formal specifications using model federation. In Software Engineering and Formal Methods, Einar Broch Johnsen and Ina Schaefer (Eds.). Springer International Publishing, 54\u201369."},{"key":"e_1_3_3_20_2","volume-title":"Proceedings of the 13th International Symposium on Theoretical Aspects of Software Engineering (TASE\u201919)","author":"Halchin Alexandra","year":"2019","unstructured":"Alexandra Halchin, Yamine A\u00eft Ameur, Neeraj Kumar Singh, Abderrahmane Feliachi, and Julien Ordioni. 2019. Certified embedding of B models in an integrated verification framework. In Proceedings of the 13th International Symposium on Theoretical Aspects of Software Engineering (TASE\u201919)."},{"key":"e_1_3_3_21_2","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/978-3-319-68499-4_11","volume-title":"Proceedings of the 2nd International Conference on Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (RSSRail\u201917)","author":"Halchin Alexandra","year":"2017","unstructured":"Alexandra Halchin, Abderrahmane Feliachi, Neeraj Kumar Singh, Yamine A\u00eft Ameur, and Julien Ordioni. 2017. B-PERFect\u2014Applying the PERF approach to B-based system developments. In Proceedings of the 2nd International Conference on Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification (RSSRail\u201917). 160\u2013172."},{"key":"e_1_3_3_22_2","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Hinton Andrew","year":"2006","unstructured":"Andrew Hinton, Marta Kwiatkowska, Gethin Norman, and David Parker. 2006. PRISM: A tool for automatic verification of probabilistic systems. In Tools and Algorithms for the Construction and Analysis of Systems, Holger Hermanns and Jens Palsberg (Eds.). Springer, Berlin, 441\u2013444."},{"issue":"4","key":"e_1_3_3_23_2","first-page":"301","article-title":"CSP-OZ-DC: A combination of specification techniques for processes, data and time","volume":"9","author":"Hoenicke Jochen","year":"2002","unstructured":"Jochen Hoenicke and Ernst-R\u00fcdiger Olderog. 2002. CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nord. J. Comput. 9, 4 (2002), 301\u2013334.","journal-title":"Nord. J. Comput."},{"key":"e_1_3_3_24_2","unstructured":"IEEE Std 1474.1-2004. 2005. IEEE standard for communications-based train control (CBTC) performance and functional requirements. https:\/\/standards.ieee.org\/ieee\/1474.1\/3552\/."},{"key":"e_1_3_3_25_2","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/978-3-319-33600-8_21","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"Iliasov Alexei","year":"2016","unstructured":"Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah, and Alexander Romanovsky. 2016. Rodin platform why3 plug-in. In Abstract State Machines, Alloy, B, TLA, VDM, and Z, Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, and Miklos Biro (Eds.). Springer International Publishing, Cham, 275\u2013281."},{"key":"e_1_3_3_26_2","volume-title":"Proceedings of the Systems Engineering Infrastructure Conference","author":"Jastram Michael","year":"2010","unstructured":"Michael Jastram. 2010. ProR, an open source platform for requirements engineering based on RIF. In Proceedings of the Systems Engineering Infrastructure Conference."},{"key":"e_1_3_3_27_2","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-642-15057-9_7","volume-title":"Verified Software: Theories, Tools, Experiments","author":"Jastram Michael","year":"2010","unstructured":"Michael Jastram, Stefan Hallerstede, Michael Leuschel, and Aryldo G. Russo. 2010. An approach of requirements tracing in formal refinement. In Verified Software: Theories, Tools, Experiments, Gary T. Leavens, Peter O\u2019Hearn, and Sriram K. Rajamani (Eds.). Springer, Berlin, 97\u2013111."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_3_3_29_2","first-page":"246","volume-title":"Proceedings of the International Conference on Formal Engineering Methods","author":"Platzer A.","year":"2009","unstructured":"A. Platzer and J.-D. Quesel. 2009. European train control system: A case study in formal verification. In Proceedings of the International Conference on Formal Engineering Methods. Springer, 246\u2013265."},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1243\/0954409001531306"},{"key":"e_1_3_3_31_2","first-page":"2867","volume-title":"Proceedings of the 40th IEEE Conference on Decision and Control","volume":"3","author":"Silva B. I.","year":"2001","unstructured":"B. I. Silva, O. Stursberg, B. H. Krogh, and S. Engell. 2001. An assessment of the current status of algorithmic approaches to the verification of hybrid systems. In Proceedings of the 40th IEEE Conference on Decision and Control, Vol. 3. IEEE, 2867\u20132874."},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2019.00019"},{"key":"e_1_3_3_33_2","first-page":"90","article-title":"A refinement-based method for developing distributed protocols","author":"Stankaitis Paulius","year":"2019","unstructured":"Paulius Stankaitis, Alexei Iliasov, Yamine A\u00eft Ameur, Tsutomu Kobayashi, Fuyuki Ishikawa, and Alexander Romanovsky. 2019. A refinement-based method for developing distributed protocols. In Proceedings of the IEEE 19th International Symposium on High Assurance Systems Engineering (HASE\u201919). 90\u201397.","journal-title":"Proceedings of the IEEE 19th International Symposium on High Assurance Systems Engineering (HASE\u201919)"},{"key":"e_1_3_3_34_2","unstructured":"The RODIN platform. 2006. Retrieved fromhttps:\/\/sourceforge.net\/projects\/rodin-b-sharp\/files\/Core_Rodin_Platform\/."},{"key":"e_1_3_3_35_2","first-page":"262","volume-title":"Verified Software: Theories, Tools, Experiments","author":"Zou Liang","year":"2014","unstructured":"Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan, and Yu Liu. 2014. Verifying chinese train control system under a combined scenario by theorem proving. In Verified Software: Theories, Tools, Experiments, Ernie Cohen and Andrey Rybalchenko (Eds.). Springer, Berlin, 262\u2013280."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524052","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3524052","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:37Z","timestamp":1750188637000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3524052"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,12]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3,31]]}},"alternative-id":["10.1145\/3524052"],"URL":"https:\/\/doi.org\/10.1145\/3524052","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-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-03-02","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"}}]}}