{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T09:51:27Z","timestamp":1790502687139,"version":"4.1.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,11,12]],"date-time":"2019-11-12T00:00:00Z","timestamp":1573516800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,11,12]],"date-time":"2019-11-12T00:00:00Z","timestamp":1573516800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000739","name":"University of Southampton","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000739","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n<jats:p>We demonstrate refinement-based formal development of the hybrid, \u2018fixed virtual block\u2019 approach to train movement control for the emerging <jats:italic>European Rail Traffic Management System<\/jats:italic> (ERTMS) level 3. Our approach uses iUML-B diagrams as a front end to the Event-B modelling language. We use abstraction to verify the principle of movement authority before gradually developing the details of the <jats:italic>Virtual Block Detector<\/jats:italic> component in subsequent refinements, thus verifying that it preserves the safety properties. We animate the refined models to demonstrate their validity using the scenarios from the <jats:italic>Hybrid ERTMS Level 3<\/jats:italic> (HLIII) specification. We reflect on our team-based approach to finding useful modelling abstractions and demonstrate a systematic modelling method based on the state and class diagrams of iUML-B. The component and control flow architectures of the application, its environment and interacting systems emerge through the layered refinement process. The runtime semantics of the specification\u2019s state-machine behaviour are modelled in the final refinements. We discuss how the model could be used to generate an implementation using code generation tools and techniques.<\/jats:p>","DOI":"10.1007\/s10009-019-00548-w","type":"journal-article","created":{"date-parts":[[2019,11,12]],"date-time":"2019-11-12T09:03:28Z","timestamp":1573549408000},"page":"297-313","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B"],"prefix":"10.1007","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2196-2749","authenticated-orcid":false,"given":"Dana","family":"Dghaym","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mohammadsadegh","family":"Dalvandi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Poppleton","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0210-0983","authenticated-orcid":false,"given":"Colin","family":"Snook","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,11,12]]},"reference":[{"key":"548_CR1","unstructured":"EEIG ERTMS\u00a0Users Group.: Principles: Hybrid ERTMS\/ETCS Level 3, 1c edition, July (2018). https:\/\/ertms.be\/sites\/default\/files\/2018-07\/16E0421C_HL3-clean.pdf. Accessed 24 Jan 2019"},{"key":"548_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"issue":"12","key":"548_CR3","doi-asserted-by":"publisher","first-page":"2350","DOI":"10.1002\/spe.2634","volume":"48","author":"M Atif","year":"2018","unstructured":"Atif, M., Felix, K., Alexander, E.: Evaluating the suitability of state-based formal methods for industrial deployment. Softw. Pract. Exper. 48(12), 2350\u20132379 (2018)","journal-title":"Softw. Pract. Exper."},{"key":"548_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines: A Method for High-Level System Design and Analysis","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Berlin (2003)"},{"key":"548_CR5","volume-title":"The Z Notation: A Reference Manual","author":"J Michael Spivey","year":"1989","unstructured":"Michael Spivey, J.: The Z Notation: A Reference Manual. Prentice-Hall, Inc., Upper Saddle River (1989)"},{"issue":"6","key":"548_CR6","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"A Jean-Raymond","year":"2010","unstructured":"Jean-Raymond, A., Michael, B., Stefan, H., Son, H.T., Farhad, M., Laurent, V.: Rodin: an open toolset for modelling and reasoning in Event-B. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Softw. Tools Technol. Transf."},{"issue":"4","key":"548_CR7","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/2237796.2237825","volume":"37","author":"J Paul Gibson","year":"2012","unstructured":"Paul Gibson, J., Isabelle, P.: Introduction to UML and formal methods. SIGSOFT Softw. Eng. Notes 37(4), 32\u201333 (2012)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"548_CR8","volume-title":"Modern Formal Methods and Applications","author":"ME Beato","year":"2006","unstructured":"Beato, M.E., Barrio-Sol\u00f3rzano, M., Cuesta, C.E., de la Fuente, P.: Formal methods for UML. In: Gabbar, H.A. (ed.) Modern Formal Methods and Applications. Springer, Dordrecht (2006)"},{"issue":"1","key":"548_CR9","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C Snook","year":"2006","unstructured":"Snook, C., Butler, M.: UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92\u2013122 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"548_CR10","unstructured":"Snook, C.: iUML-B statemachines. In: Proceedings of the Rodin Workshop 2014, pp. 29\u201330, Toulouse, France http:\/\/eprints.soton.ac.uk\/365301\/ (2014). Accessed 7 Nov 2019"},{"issue":"4","key":"548_CR11","doi-asserted-by":"publisher","first-page":"1557","DOI":"10.1007\/s10270-013-0391-z","volume":"14","author":"MY Said","year":"2015","unstructured":"Said, M.Y., Butler, M., Snook, C.: A method of refinement in UML-B. Softw. Syst. Model 14(4), 1557\u20131580 (2015)","journal-title":"Softw. Syst. Model"},{"key":"548_CR12","doi-asserted-by":"crossref","unstructured":"Kossak, F., Mashkoor, A., Geist, V., Illibauer, C.: Improving the understandability of formal specifications: an experience report. In: Proceedings of the 20th International Working Conference on Requirements Engineering: Foundation for Software Quality\u2014Volume 8396, REFSQ 2014, pp. 184\u2013199. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-05843-6_14"},{"key":"548_CR13","unstructured":"Pang, C., Pakonen, A., Buzhinsky, I., Vyatkin, V.: A study on user-friendly formal specification languages for requirements formalization. In: 14th IEEE International Conference on Industrial Informatics, INDIN 2016, Poitiers, France, July 19\u201321, 2016, pp. 676\u2013682. IEEE (2016)"},{"issue":"2","key":"548_CR14","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Softw. Tools Technol. Transf. (STTT) 10(2), 185\u2013203 (2008)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"key":"548_CR15","doi-asserted-by":"crossref","unstructured":"Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising Event-B models with B-motion studio. In: Proceedings of FMICS 2009, Volume 5825 of Lecture Notes in Computer Science, pp. 202\u2013204. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04570-7_17"},{"key":"548_CR16","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-319-91271-4_23","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Dghaym","year":"2018","unstructured":"Dghaym, D., Poppleton, M., Snook, C.: Diagram-led formal modelling using iUML-B for Hybrid ERTMS Level 3. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 338\u2013352. Springer International Publishing, Cham (2018)"},{"key":"548_CR17","unstructured":"EEIG ERTMS\u00a0Users Group.: Principles: Hybrid ERTMS\/ETCS Level 3. http:\/\/www.southampton.ac.uk\/assets\/sharepoint\/groupsite\/Academic\/ABZ-Coneference-2018\/Public. Accessed 18 Jan 2018"},{"key":"548_CR18","unstructured":"Hoang, T.S.: An introduction to the Event-B modelling method. In: Industrial Deployment of System Engineering Methods, pp. 211\u2013236. Springer, Berlin (2013)"},{"key":"548_CR19","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/j.scico.2016.04.010","volume":"131","author":"F Andreas","year":"2016","unstructured":"Andreas, F., Son, H.T., Basin, D., Sato, N., Miyazaki, K.: Large-scale system development using Abstract Data Types and refinement. Sci. Comput. Program. 131, 59\u201375 (2016)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"548_CR20","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/s00165-014-0311-1","volume":"27","author":"A Salehi","year":"2015","unstructured":"Salehi, A., Butler, M., Rezazadeh, A.: Language and tool support for event refinement structures in Event-B. Formal Asp. Comput. 27(3), 499\u2013523 (2015)","journal-title":"Formal Asp. Comput."},{"issue":"05","key":"548_CR21","doi-asserted-by":"publisher","first-page":"36","DOI":"10.4204\/EPTCS.115.3","volume":"115","author":"M Butler","year":"2013","unstructured":"Butler, M., Colley, J., Edmunds, A., Snook, C., Evans, N., Grant, N., Marshall, H.: Modelling and refinement in CODA. Electron. Proc. Theor. Comput. Sci. 115(05), 36\u201351 (2013)","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"548_CR22","unstructured":"Edmunds, A., Butler, M.: Tasking Event-B: an extension to Event-B for generating concurrent code. In: PLACES2011 April (2011)"},{"key":"548_CR23","doi-asserted-by":"crossref","unstructured":"Butler, M.: Decomposition structures for Event-B. In: International Conference on Integrated Formal Methods, pp. 20\u201338. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-00255-7_2"},{"key":"548_CR24","unstructured":"Dalvandi, M., Fathabadi, A.S., Butler, M.: A report on PRiME code generation activities. In: 7th Rodin Workshop (05\/06\/18), June (2018)"},{"key":"548_CR25","doi-asserted-by":"crossref","unstructured":"Dalvandi, M., Butler, M., Fathabadi, A.S.: SEB-CG: Code generation tool with algorithmic refinement support for Event-B. In: Workshop on Practical Formal Verification for Software Dependability (AFFORD\u201919) (2019)","DOI":"10.1007\/978-3-030-54994-7_3"},{"key":"548_CR26","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.scico.2017.05.010","volume":"148","author":"M Dalvandi","year":"2017","unstructured":"Dalvandi, M., Butler, M., Rezazadeh, A.: Derivation of algorithmic control structures in Event-B refinement. Sci. Comput. Program. 148, 49\u201365 (2017)","journal-title":"Sci. Comput. Program."},{"key":"548_CR27","doi-asserted-by":"crossref","unstructured":"Dalvandi, M., Butler, M., Rezazadeh, A., Fathabadi, A.S.: Verifiable code generation from scheduled Event-B models. In: International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 234\u2013248. Springer (2018)","DOI":"10.1007\/978-3-319-91271-4_16"},{"key":"548_CR28","doi-asserted-by":"crossref","unstructured":"Dalvandi, M., Butler, M., Rezazadeh A.: Transforming Event-B models to Dafny contracts. In: Electronic Communications of the EASST, vol. 72 (2015)","DOI":"10.1007\/978-3-319-24644-4_21"},{"key":"548_CR29","doi-asserted-by":"crossref","unstructured":"Eysholdt, M., Behrens, H.: Xtext: Implement your language faster than the quick and dirty way. In: Proceedings of the ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion, OOPSLA \u201910, pp. 307\u2013309. ACM, New York, NY, USA (2010)","DOI":"10.1145\/1869542.1869625"},{"key":"548_CR30","doi-asserted-by":"crossref","unstructured":"Hoang, T.S., Dghaym, D., Snook, C., Butler, M.: A composition mechanism for refinement-based methods. In: Proceedings 2017 22nd International Conference on Engineering of Complex Computer Systems: ICECCS 2017. IEEE (2018)","DOI":"10.1109\/ICECCS.2017.27"},{"key":"548_CR31","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-319-91271-4_22","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"J-R Abrial","year":"2018","unstructured":"Abrial, J.-R.: The ABZ-2018 case study with Event-B. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 322\u2013337. Springer International Publishing, Cham (2018)"},{"key":"548_CR32","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-319-91271-4_18","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"SJT Fotso","year":"2018","unstructured":"Fotso, S.J.T., Frappier, M., Laleau, R., Mammar, A.: Modeling the Hybrid ERTMS\/ETCS Level 3 standard using a formal requirements engineering approach. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 262\u2013276. Springer International Publishing, Cham (2018)"},{"key":"548_CR33","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-319-91271-4_24","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A Mammar","year":"2018","unstructured":"Mammar, A., Frappier, M., Fotso, S.J.T., Laleau, R.: An Event-B model of the Hybrid ERTMS\/ETCS Level 3 standard. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 353\u2013366. Springer International Publishing, Cham (2018)"},{"key":"548_CR34","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-91271-4_21","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"A Cunha","year":"2018","unstructured":"Cunha, A., Macedo, N.: Validating the Hybrid ERTMS\/ETCS Level 3 concept with Electrum. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 307\u2013321. Springer International Publishing, Cham (2018)"},{"key":"548_CR35","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-319-91271-4_19","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"P Arcaini","year":"2018","unstructured":"Arcaini, P., Je\u017eek, P., Kofro\u0148, J.: Modelling the Hybrid ERTMS\/ETCS Level 3 case study in SPIN. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 277\u2013291. Springer International Publishing, Cham (2018)"},{"key":"548_CR36","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-91271-4_20","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Hansen","year":"2018","unstructured":"Hansen, D., Leuschel, M., Schneider, D., Krings, S., K\u00f6rner, P., Naulin, T., Nayeri, N., Skowron, F.: Using a formal B model at runtime in a demonstration of the ETCS Hybrid Level 3 concept with real trains. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 292\u2013306. Springer International Publishing, Cham (2018)"},{"key":"548_CR37","unstructured":"Butler, M., Dghaym, D., Fischer, T., Hoang, T.S., Reichl, K., Snook, C., Tummeltshammer, P.: Formal modelling techniques for efficient development of railway control products. In: RSSRail 2017, Pistoia, Italy, 2017, volume 10598 of LNCS, pp. 71\u201386. Springer (2017)"},{"issue":"3","key":"548_CR38","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/s00165-014-0311-1","volume":"27","author":"A Salehi","year":"2015","unstructured":"Salehi, A., Butler, M., Rezazadeh, A.: Language and tool support for event refinement structures in Event-B. Formal Asp. Comput. 27(3), 499\u2013523 (2015)","journal-title":"Formal Asp. Comput."},{"key":"548_CR39","doi-asserted-by":"crossref","unstructured":"Hoang, T.S., Snook, C., Dghaym, D., Butler, M.: Class-diagrams for Abstract Data Types. In: ICTAC 2017, Hanoi, Vietnam, 2017, Proceedings, volume 10580 of LNCS, pp. 100\u2013117. Springer (2017)","DOI":"10.1007\/978-3-319-67729-3_7"},{"key":"548_CR40","doi-asserted-by":"crossref","unstructured":"Platzer, A., Quesel, J.-D.: European Train Control System: a case study in formal verification. In ICFEM 2009, Rio de Janeiro, Brazil, 2009. Proceedings, volume 5885 of LNCS, pp. 246\u2013265. Springer (2009)","DOI":"10.1007\/978-3-642-10373-5_13"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00548-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00548-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00548-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,11]],"date-time":"2020-11-11T00:26:08Z","timestamp":1605054368000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00548-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,12]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["548"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00548-w","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,12]]},"assertion":[{"value":"12 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}