{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T20:10:01Z","timestamp":1773259801036,"version":"3.50.1"},"reference-count":32,"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,11,24]],"date-time":"2021-11-24T00:00:00Z","timestamp":1637712000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["1798533"],"award-info":[{"award-number":["1798533"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"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>The decentralised railway signalling systems have a potential to\nincrease capacity, availability and reduce maintenance costs of\nrailway networks. However, given the safety-critical nature of\nrailway signalling and the complexity of novel distributed\nsignalling solutions, their safety should be guaranteed by using\nthorough system validation methods. To achieve such a high-level of\nsafety assurance of these complex signalling systems, scenario-based\ntesting methods are far from being sufficient despite that they are\nstill widely used in the industry. Formal verification is an\nalternative approach which provides a rigorous approach to verifying\ncomplex systems and has been successfully used in the railway\ndomain. Despite the successes, little work has been done in applying\nformal methods for distributed railway systems. In our research we\nare working towards a multifaceted formal development methodology of\ncomplex railway signalling systems. The methodology is based on the\nEvent-B modelling language which provides an expressive modelling\nlanguage, a stepwise development and a proof-based model\nverification. In this paper, we present the application of the\nmethodology for the development and verification of a distributed\nprotocol for reservation of railway sections. The main challenge of\nthis work is developing a distributed protocol which ensures safety\nand liveness of the distributed railway system when message delays\nare allowed in the model.<\/jats:p>","DOI":"10.1007\/s00165-021-00567-y","type":"journal-article","created":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T14:02:51Z","timestamp":1637762571000},"page":"1009-1036","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A refinement-based development of a distributed signalling system"],"prefix":"10.1145","volume":"33","author":[{"given":"Paulius","family":"Stankaitis","sequence":"first","affiliation":[{"name":"School of Computing, Newcastle University, Newcastle upon Tyne, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexei","family":"Iliasov","sequence":"additional","affiliation":[{"name":"The Formal Route Limited, 32A Woodhouse Grove, E12 6SR, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tsutomu","family":"Kobayashi","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yamine","family":"A\u00eft-Ameur","sequence":"additional","affiliation":[{"name":"INPT\u2013ENSEEIHT, 2 Rue Charles Camichel, Toulouse, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fuyuki","family":"Ishikawa","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Romanovsky","sequence":"additional","affiliation":[{"name":"School of Computing, Newcastle University, Newcastle upon Tyne, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abrial J R (1996) The B-book: assigning programs to meanings. Cambridge University Press New York","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_2_2","unstructured":"Abrial JR (2013) Modeling in Event-B: system and software engineering. Cambridge University Press New York"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Back RJR (1990) Refinement calculus part II: parallel and reactive programs. In: de Bakker JW de Roever WP Rozenberg G\n(eds) Stepwise refinement of distributed systems models formalisms correctness. Springer Berlin pp 67\u201393","DOI":"10.1007\/3-540-52559-9_61"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Behm P Benoit P Faivre A Meynadier JM (1999) M\u00e9t\u00e9or: a successful application of B in a large project. In Wing JM Woodcock\nK Davies J (eds) FM\u201999\u2014formal methods. Springer Berlin pp 369\u2013387","DOI":"10.1007\/3-540-48119-2_22"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bernstein PA Shipman DW Rothnie JB Jr (1980) Concurrency control in a system for distributed databases (SDD-1). ACM\nTrans Database Syst 5(1):18\u201351","DOI":"10.1145\/320128.320131"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Cansell D M\u00e9ry D (2006) Formal and incremental construction of distributed algorithms: on the distributed reference counting\nalgorithm. Theor Comput Sci 364(3):318\u2013337","DOI":"10.1016\/j.tcs.2006.08.015"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe D Fontaine P Guyot Y Voisin L (2014) Integrating SMT Solvers in Rodin. Sci Comput Program 94(P2):130\u2013143","DOI":"10.1016\/j.scico.2014.04.012"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Essam\u00e9 D Doll\u00e9 D (2006) B in large-scale projects: the Canarsie line CBTC experience. In: Julliand J Kouchnarenko O (eds) B\n2007: formal specification and development in B. Springer Berlin pp 252\u2013254","DOI":"10.1007\/11955757_21"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Eswaran Kapali P Gray Jim Lorie Raymond A Traiger Irving L (1976) The Notions of Consistency and Predicate Locks in a\nDatabase System. Commun. ACM 19(11):624\u2013633","DOI":"10.1145\/360363.360369"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Fantechi A Haxthausen AE (2018) Safety interlocking as a distributed mutual exclusion problem. In Howar F Barnat J (eds)\nFormal methods for industrial critical systems. Springer Cham pp 52\u201366","DOI":"10.1007\/978-3-030-00244-2_4"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Fantechi A Haxthausen AE Nielsen MBR (2017) Model checking geographically distributed interlocking systems using UMC.\nIn: 25th Euromicro international conference on parallel distributed and network-based processing (PDP) pp 278\u2013286","DOI":"10.1109\/PDP.2017.66"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Geisler S Haxthausen AE (2021) Stepwise development and model checking of a distributed interlocking system using RAISE.\nFormal Aspects Comput 33:87\u2013125","DOI":"10.1007\/s00165-020-00507-2"},{"key":"e_1_2_1_2_13_2","unstructured":"Gray J Reuter A (1992) Transaction processing: concepts and techniques 1st edn. Morgan Kaufmann Publishers Inc. San\nFrancisco"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Hawblitzel C Howell J Kapritsos M Lorch JR Parno B Roberts ML Setty S Zill B (2017) IronFleet: proving safety and\nliveness of practical distributed systems. Commun ACM 60(7):83\u201392","DOI":"10.1145\/3068608"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Hoang TS Kuruma H Basin D Abrial JR (2009) Developing topology discovery in Event-B. Sci Comput Program 74(11):879\u2013\n899","DOI":"10.1016\/j.scico.2009.07.006"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Hinton A Kwiatkowska M Norman G Parker D (2006) PRISM: a tool for automatic verification of probabilistic systems. In:\nHermanns H Palsberg J (eds) Tools and algorithms for the construction and analysis of systems. Springer Berlin pp 441\u2013444","DOI":"10.1007\/11691372_29"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Hoang TS (2014) Reasoning about almost-certain convergence properties using Event-B. Sci Comput Program 81:108\u2013121","DOI":"10.1016\/j.scico.2013.08.006"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Haxthausen AE Peleska J (2000) Formal development and verification of a distributed railway control system. IEEE Trans\nSoftw Eng 26(8):687\u2013701","DOI":"10.1109\/32.879808"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Iliasov A Laibinis L Troubitsyna E Romanovsky A (2011) Formal derivation of a distributed program in Event B. In: Qin S Qiu Z ( eds) Formal methods and software engineering. Springer Berlin pp 420\u2013436","DOI":"10.1007\/978-3-642-24559-6_29"},{"key":"#cr-split#-e_1_2_1_2_20_2.1","doi-asserted-by":"crossref","unstructured":"Iliasov A Stankaitis P Adjepon-Yamoah D Romanovsky A (2016) Rodin platform Why3 plug-in. In: Proceedings of the 5th","DOI":"10.1007\/978-3-319-33600-8_21"},{"key":"#cr-split#-e_1_2_1_2_20_2.2","unstructured":"international conference on abstract state machines alloy B TLA VDM and Z ABZ 2016. Springer Berlin pp 275-281"},{"key":"e_1_2_1_2_21_2","unstructured":"INTO-CPS Project (2016) Deliverable D1.2-Case studies 2. Available at https:\/\/into-cps.org\/publications\/"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Leuschel M Butler M (2003) ProB: a model checker for B. In: Araki K Gnesi S Mandrioli D (eds) FME 2003: formal methods.\nSpringer Berlin pp 855\u2013874","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Lecomte T D\u00e9harbe D Fournier P Oliveira M (2020) The CLEARSY safety platform: 5 years of research development and\ndeployment. Sci Comput Program 199:102524","DOI":"10.1016\/j.scico.2020.102524"},{"key":"e_1_2_1_2_24_2","unstructured":"Morley MJ (1996) Safety assurance in interlocking design. PhD thesis University of Edinburgh. College of Science and Engineering.\nSchool of Informatics"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Newcombe C (2014) Why Amazon Chose TLA+. In: Ait Ameur Y Schewe KD (eds) Abstract state machines alloy B TLA VDM and Z. Springer Berlin pp 25\u201339","DOI":"10.1007\/978-3-662-43652-3_3"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Stankaitis P Dupont G Singh NK Ait-Ameur Y Iliasov A Romanovsky A (2019) Modelling hybrid train speed controller\nusing proof and refinement. In: 2019 24th International conference on engineering of complex computer systems (ICECCS) pp\n107\u2013113","DOI":"10.1109\/ICECCS.2019.00019"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Stankaitis P Iliasov A (2017) Theories techniques and tools for engineering heterogeneous railway networks. In: Fantechi\nA Lecomte T Romanovsky A (eds) Reliability safety and security of railway systems. Modelling analysis verification and\ncertification. Springer Cham pp 241\u2013250","DOI":"10.1007\/978-3-319-68499-4_16"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Stankaitis P Iliasov A Ait-Ameur Y Kobayashi T Ishikawa F Romanovsky A(2019)Arefinement based method for developing\ndistributed protocols. In: IEEE 19th international symposium on high assurance systems engineering (HASE) pp 90\u201397","DOI":"10.1109\/HASE.2019.00023"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Stankaitis P Iliasov A Kobayashi T A\u00eft-Ameur Y Ishikawa F Romanovsky A (2020) Formal distributed protocol development\nfor reservation of railway sections. In: Raschke A M\u00e9ry D Houdek F (eds) Rigorous state-based methods. Springer Cham pp\n203\u2013219","DOI":"10.1007\/978-3-030-48077-6_14"},{"key":"e_1_2_1_2_30_2","unstructured":"The RODIN platform (2006). Available at https:\/\/sourceforge.net\/projects\/rodin-b-sharp\/files\/Core_Rodin_Platform\/"},{"key":"e_1_2_1_2_31_2","unstructured":"Whitwam F Kanner A (2012) Control of automatic guided vehicles without wayside INterlocking. Patent US 20120323411 A1"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00567-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-021-00567-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00567-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00567-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,21]],"date-time":"2022-04-21T20:43:29Z","timestamp":1650573809000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-021-00567-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":32,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["10.1007\/s00165-021-00567-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-021-00567-y","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":"21 January 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 September 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 September 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 November 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}