{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:20Z","timestamp":1773827480470,"version":"3.50.1"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,9,26]],"date-time":"2019-09-26T00:00:00Z","timestamp":1569456000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,9,26]],"date-time":"2019-09-26T00:00:00Z","timestamp":1569456000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,6]]},"DOI":"10.1007\/s10009-019-00540-4","type":"journal-article","created":{"date-parts":[[2019,9,26]],"date-time":"2019-09-26T05:12:50Z","timestamp":1569474770000},"page":"281-296","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Validating the Hybrid ERTMS\/ETCS Level 3 concept with Electrum"],"prefix":"10.1007","volume":"22","author":[{"given":"Alcino","family":"Cunha","sequence":"first","affiliation":[]},{"given":"Nuno","family":"Macedo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,26]]},"reference":[{"key":"540_CR1","volume-title":"The B-Book\u2014Assigning Programs to Meanings","author":"J Abrial","year":"2005","unstructured":"Abrial, J.: The B-Book\u2014Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"540_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B\u2014System and Software Engineering","author":"J Abrial","year":"2010","unstructured":"Abrial, J.: Modeling in Event-B\u2014System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"540_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.: The ABZ-2018 case study with Event-B. In: ABZ, Volume 10817 of LNCS, pp. 322\u2013337. Springer (2018)","DOI":"10.1007\/978-3-319-91271-4_22"},{"issue":"6","key":"540_CR4","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J Abrial","year":"2010","unstructured":"Abrial, J., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447\u2013466 (2010)","journal-title":"STTT"},{"key":"540_CR5","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Jezek, P., Kofron, J.: Modelling the Hybrid ERTMS\/ETCS Level 3 case study in S pin. In: ABZ, Volume 10817 of LNCS, pp. 277\u2013291. Springer (2018)","DOI":"10.1007\/978-3-319-91271-4_19"},{"key":"540_CR6","doi-asserted-by":"crossref","unstructured":"Couto, R., Campos, J.C., Macedo, N., Cunha, A.: Improving the visualization of Alloy instances. In: F-IDE@FLoC, Volume 284 of EPTCS, pp. 37\u201352 (2018)","DOI":"10.4204\/EPTCS.284.4"},{"key":"540_CR7","doi-asserted-by":"crossref","unstructured":"Cunha, A., Macedo, N.: Validating the Hybrid ERTMS\/ETCS Level 3 concept with Electrum. In: ABZ, Volume 10817 of LNCS, pp. 307\u2013321. Springer (2018)","DOI":"10.1007\/978-3-319-91271-4_21"},{"key":"540_CR8","doi-asserted-by":"crossref","unstructured":"Dghaym, D., Poppleton, M., Snook, C.: Diagram-led formal modelling using iUML-B for Hybrid ERTMS Level 3. In: ABZ, Volume 10817 of LNCS, pp. 338\u2013352. Springer (2018)","DOI":"10.1007\/978-3-319-91271-4_23"},{"key":"540_CR9","unstructured":"EEIG ERTMS Users Group: Hybrid ERTMS\/ETCS Level 3\u2014principles. \nhttp:\/\/www.ertms.be\/sites\/default\/files\/2018-03\/16E0421A_HL3.pdf\n\n 16E042, version 1A (2017)"},{"key":"540_CR10","unstructured":"EEIG ERTMS Users Group: Hybrid ERTMS\/ETCS Level 3\u2014principles. \nhttps:\/\/ertms.be\/sites\/default\/files\/2018-07\/16E0421C_HL3-clean.pdf\n\n 16E042, version 1C (2018)"},{"key":"540_CR11","unstructured":"ERA, UNISIG, and EEIG ERTMS Users Group: Glossary of unisig terms and abbreviations. \nhttps:\/\/www.era.europa.eu\/filebrowser\/download\/492_en\n\n SUBSET-023, issue 3.3.0 (2016)"},{"key":"540_CR12","doi-asserted-by":"crossref","unstructured":"Fotso, S., Frappier, M., Laleau, R., Mammar, A.: Modeling the Hybrid ERTMS\/ETCS Level 3 standard using a formal requirements engineering approach. In: ABZ, Volume 10817 of LNCS, pp. 262\u2013276. Springer (2018)","DOI":"10.1007\/978-3-319-91271-4_18"},{"key":"540_CR13","doi-asserted-by":"crossref","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: ABZ, Volume 10817 of LNCS, pp. 292\u2013306. Springer (2018)","DOI":"10.1007\/978-3-319-91271-4_20"},{"key":"540_CR14","doi-asserted-by":"crossref","unstructured":"Hoang, T.S., Butler, M., Reichl, K.: The Hybrid ERTMS\/ETCS Level 3 case study. In: ABZ, Volume 10817 of LNCS, pp. 251\u2013261. Springer (2018)","DOI":"10.1007\/978-3-319-91271-4_17"},{"key":"540_CR15","volume-title":"The SPIN Model Checker-Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker-Primer and Reference Manual. Addison-Wesley, Boston (2004)"},{"key":"540_CR16","unstructured":"INESC TEC and ONERA: Electrum Analyzer, v1.0. Available under the MIT License at \nhttps:\/\/github.com\/haslab\/Electrum\/releases\/tag\/v1.0\n\n (2018)"},{"key":"540_CR17","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)"},{"key":"540_CR18","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.: ProB: A model checker for B. In: FME, Volume 2805 of LNCS, pp. 855\u2013874. Springer (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"540_CR19","doi-asserted-by":"crossref","unstructured":"Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: SIGSOFT FSE, pp. 373\u2013383. ACM (2016)","DOI":"10.1145\/2950290.2950318"},{"key":"540_CR20","doi-asserted-by":"crossref","unstructured":"Mammar, A., Frappier, M., Fotso, S., Laleau, R.: An Event-B model of the Hybrid ERTMS\/ETCS Level 3 standard. In: ABZ, Volume 10817 of LNCS, pp. 353\u2013366. Springer (2018)","DOI":"10.1007\/978-3-319-91271-4_24"},{"key":"540_CR21","doi-asserted-by":"crossref","unstructured":"Mammar, A., Laleau, R.: On the use of domain and system knowledge modeling in goal-based Event-B specifications. In: ISoLA, Volume 9952 of LNCS, pp. 325\u2013339 (2016)","DOI":"10.1007\/978-3-319-47166-2_23"},{"key":"540_CR22","doi-asserted-by":"crossref","unstructured":"Moreira, J.M., Cunha, A., Macedo, N.: An ORCID based synchronization framework for a national CRIS ecosystem. F1000Research 4, 181 (2015)","DOI":"10.12688\/f1000research.6499.1"},{"key":"540_CR23","doi-asserted-by":"crossref","unstructured":"Snook, C.: iUML-B statemachines. In: Proceedings of the Rodin Workshop 2014, pp. 29\u201330. \nhttp:\/\/eprints.soton.ac.uk\/365301\/\n\n (2014)","DOI":"10.7748\/ns.29.6.30.s35"},{"issue":"1","key":"540_CR24","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."}],"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-00540-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00540-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00540-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,24]],"date-time":"2020-09-24T23:59:10Z","timestamp":1600991950000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00540-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,26]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["540"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00540-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9,26]]},"assertion":[{"value":"26 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}