{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:27Z","timestamp":1773827487181,"version":"3.50.1"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,2,15]],"date-time":"2020-02-15T00:00:00Z","timestamp":1581724800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,2,15]],"date-time":"2020-02-15T00:00:00Z","timestamp":1581724800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003484","name":"Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003484","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><jats:p>In this article, we present a concrete realisation of the ETCS hybrid level 3 concept, whose practical viability was evaluated in a field demonstration in 2017. Hybrid level 3 introduces virtual subsections as sub-divisions of classical track sections with trackside train detection. Our approach introduces an add-on for the radio block centre (RBC) of Thales, called virtual block function (VBF), which computes the occupation states of the virtual subsections using the train position reports, train integrity information, and the track occupation states. From the perspective of the RBC, the VBF behaves as an interlocking that transmits all signal aspects for virtual signals introduced for each virtual subsection to the RBC. We report on the development of the VBF, implemented as a formal B model executed at runtime using <jats:sc>ProB<\/jats:sc> and successfully used in a field demonstration to control real trains.\n<\/jats:p>","DOI":"10.1007\/s10009-020-00551-6","type":"journal-article","created":{"date-parts":[[2020,2,15]],"date-time":"2020-02-15T17:02:51Z","timestamp":1581786171000},"page":"315-332","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":29,"title":["Validation and real-life demonstration of ETCS hybrid level 3 principles using a formal B model"],"prefix":"10.1007","volume":"22","author":[{"given":"Dominik","family":"Hansen","sequence":"first","affiliation":[]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"K\u00f6rner","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Krings","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Naulin","sequence":"additional","affiliation":[]},{"given":"Nader","family":"Nayeri","sequence":"additional","affiliation":[]},{"given":"David","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Frank","family":"Skowron","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,2,15]]},"reference":[{"key":"551_CR1","unstructured":"Hybrid ERTMS\/ETCS level 3. Principles Ref: 16E042, Version: 1A, EEIG ERTMS Users Group, 123-133 Rue Froissart, 1040 Brussels, Belgium (2017)"},{"issue":"2","key":"551_CR2","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.J.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"551_CR3","doi-asserted-by":"crossref","unstructured":"Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification of a dual chamber implantable pacemaker. In: Proceedings TACAS\u20192012, Volume 7214 of LNCS, pp. 188\u2013203. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28756-5_14"},{"key":"551_CR4","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: Proceedings ABZ\u20192018, Volume 10817 of LNCS, pp. 292\u2013306. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-91271-4_20"},{"key":"551_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"551_CR6","volume-title":"The Z Notation: A Reference Manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall, London (1992)"},{"issue":"1","key":"551_CR7","first-page":"11","volume":"22","author":"D Doll\u00e9","year":"2003","unstructured":"Doll\u00e9, D., Essam\u00e9, D.: B dans le transport ferroviaire. L\u2019exp\u00e9rience de Siemens Transportation Systems. Tech. Sci. Inform. 22(1), 11\u201332 (2003)","journal-title":"Tech. Sci. Inform."},{"key":"551_CR8","doi-asserted-by":"crossref","unstructured":"Essam\u00e9, D., Doll\u00e9, D.: B in large scale projects: the Canarsie line CBTC experience. In: Proceedings B\u20192007, Volume 4355 of LNCS, pp. 252\u2013254. Springer, Berlin (2007)","DOI":"10.1007\/11955757_21"},{"key":"551_CR9","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S.: An open extensible tool environment for Event-B. In: Proceedings ICFEM\u20192006, Volume 4260 of LNCS, pp. 588\u2013605. Springer, Berlin (2006)","DOI":"10.1007\/11901433_32"},{"key":"551_CR10","doi-asserted-by":"crossref","unstructured":"Essam\u00e9, D., Doll\u00e9, D.: B in large-scale projects: the Canarsie line CBTC experience. In: Proceedings B\u20192007, Volume 4355 of LNCS, pp. 252\u2013254. Springer, Berlin (2007)","DOI":"10.1007\/11955757_21"},{"issue":"6","key":"551_CR11","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1007\/s00165-010-0172-1","volume":"23","author":"M Leuschel","year":"2011","unstructured":"Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models with ProB. Form. Asp. Comput. 23(6), 683\u2013709 (2011)","journal-title":"Form. Asp. Comput."},{"key":"551_CR12","unstructured":"Lecomte, T., Burdy, L., Leuschel, M.: Formally checking large data sets in the railways. CoRR, arXiv:1210.6815 (2012)"},{"key":"551_CR13","doi-asserted-by":"crossref","unstructured":"Sabatier, D., Burdy, L., Requet, A., Gu\u00e9ry, J.: Formal proofs for the NYCT line 7 (flushing) modernization project. In: Proceedings ABZ\u20192012, pp. 369\u2013372 (2012)","DOI":"10.1007\/978-3-642-30885-7_34"},{"key":"551_CR14","doi-asserted-by":"crossref","unstructured":"Sabatier, D.: Using formal proof and B method at system level for industrial projects. In: Proceedings RSSRail\u20192016, Volume 9707 of LNCS, pp. 20\u201331. Springer, Berlin (2016)","DOI":"10.1007\/978-3-319-33951-1_2"},{"key":"551_CR15","doi-asserted-by":"crossref","unstructured":"Comptier, M., D\u00e9harbe, D., Perez, J.M., Mussat, L., Thibaut, P., Sabatier, D.: Safety analysis of a CBTC system: a rigorous approach with Event-B. In: Proceedings RSSRail\u20192017, Volume 10598 of LNCS, pp. 148\u2013159. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-68499-4_10"},{"key":"551_CR16","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Butler, M.J.: ProB: a model checker for B. In: Proceedings FME\u20192003, Volume 2805 of LNCS, pp. 855\u2013874. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45236-2_46"},{"key":"551_CR17","doi-asserted-by":"crossref","unstructured":"Hansen, D., Schneider, D., Leuschel, M.: Using B and ProB for data validation projects. In: Proceedings ABZ\u20192016, Volume 9675 of LNCS, pp. 167\u2013182. Springer, Berlin (2016)","DOI":"10.1007\/978-3-319-33600-8_10"},{"key":"551_CR18","doi-asserted-by":"crossref","unstructured":"Schneider, D., Leuschel, M., Witt, T.: Model-based problem solving for university timetable validation and improvement. In: Proceedings FM\u20192015, Volume 9109 of LNCS, pp. 487\u2013495. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-19249-9_30"},{"key":"551_CR19","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)"},{"key":"551_CR20","unstructured":"ERTMS\/ETCS\u2014Baseline 3. System Requirements Specification Ref: SUBSET-026-3, Issue: 3.0.0, EEIG ERTMS Users Group, 123-133 Rue Froissart, 1040 Brussels, Belgium (2008)"},{"key":"551_CR21","doi-asserted-by":"crossref","unstructured":"Mammar, A., Frappier, M., Fotso, S.J.T., Laleau, R.: An Event-B model of the hybrid ERTMS\/ETCS level 3 standard. In: Proceedings ABZ\u20192018, pp. 353\u2013366 (2018)","DOI":"10.1007\/978-3-319-91271-4_24"},{"key":"551_CR22","doi-asserted-by":"crossref","unstructured":"Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising Event-B models with B-Motion Studio. In: Proceedings FMICS\u20192009, Volume 5825 of LNCS, pp. 202\u2013204. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04570-7_17"},{"key":"551_CR23","unstructured":"Ladenberger, L.: Rapid Creation of Interactive Formal Prototypes for Validating Safety-Critical Systems. PhD thesis, University of D\u00fcsseldorf, Germany (2017)"},{"key":"551_CR24","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s10009-015-0395-9","volume":"19","author":"L Ladenberger","year":"2017","unstructured":"Ladenberger, L., Hansen, D., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. Int. J. Softw. Tools Technol. Transf. 19, 187\u2013203 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"551_CR25","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: On B and Event-B: principles, success and challenges. In: Proceedings ABZ\u20192018, Volume 10817 of LNCS, pp. 31\u201335. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-91271-4_3"},{"key":"551_CR26","doi-asserted-by":"crossref","unstructured":"Reichl, K., Fischer, T., Tummeltshammer, P.: Using formal methods for verification and validation in railway. In: Proceedings TAP\u20192016, Volume 9762 of LNCS, pp. 3\u201313. Springer, Berlin (2016)","DOI":"10.1007\/978-3-319-41135-4_1"},{"key":"551_CR27","doi-asserted-by":"crossref","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: Proceedings ABZ\u20192018, Volume 10817 of LNCS, pp. 262\u2013276. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-91271-4_18"},{"key":"551_CR28","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The ABZ-2018 case study with Event-B. In: Proceedings ABZ\u20192018, Volume 10817 of LNCS, pp. 322\u2013337. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-91271-4_22"},{"key":"551_CR29","doi-asserted-by":"crossref","unstructured":"Dghaym, D., Poppleton, M., Snook, C.F.: Diagram-led formal modelling using iUML-B for hybrid ERTMS Level 3. In: Proceedings ABZ\u20192018, Volume 10817 of LNCS, pp. 338\u2013352. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-91271-4_23"},{"key":"551_CR30","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Jezek, P., Kofron, J.: Modelling the hybrid ERTMS\/ETCS level 3 case study in Spin. In: Proceedings ABZ\u20192018, Volume 10817 of LNCS, pp. 277\u2013291. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-91271-4_19"},{"key":"551_CR31","doi-asserted-by":"crossref","unstructured":"Cunha, A., Macedo, N.: Validating the hybrid ERTMS\/ETCS Level 3 concept with electrum. In: Proceedings ABZ\u20192018, Volume 10817 of LNCS, pp. 307\u2013321. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-91271-4_21"},{"key":"551_CR32","doi-asserted-by":"crossref","unstructured":"Snook, C.F., Hoang, T.S., Dghaym, D., Butler, M.J., Fischer, T., Schlick, R., Wang, K.: Behaviour-driven formal model development. In: Proceedings ICFEM\u20192018, pp. 21\u201336 (2018)","DOI":"10.1007\/978-3-030-02450-5_2"}],"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-020-00551-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-020-00551-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00551-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,14]],"date-time":"2021-02-14T09:37:18Z","timestamp":1613295438000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-020-00551-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,15]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["551"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00551-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,2,15]]},"assertion":[{"value":"15 February 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}