{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:03:30Z","timestamp":1757311410833},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319912707"},{"type":"electronic","value":"9783319912714"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-91271-4_20","type":"book-chapter","created":{"date-parts":[[2018,5,7]],"date-time":"2018-05-07T10:32:55Z","timestamp":1525689175000},"page":"292-306","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains"],"prefix":"10.1007","author":[{"given":"Dominik","family":"Hansen","sequence":"first","affiliation":[]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]},{"given":"David","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Krings","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"K\u00f6rner","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Naulin","sequence":"additional","affiliation":[]},{"given":"Nader","family":"Nayeri","sequence":"additional","affiliation":[]},{"given":"Frank","family":"Skowron","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,8]]},"reference":[{"key":"20_CR1","unstructured":"Hybrid ERTMS\/ETCS Level 3. Principles Ref: 16E042, Version: 1A, EEIG ERTMS Users Group, 123\u2013133 Rue Froissart, 1040 Brussels, Belgium, 7 2017"},{"key":"20_CR2","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)"},{"issue":"1","key":"20_CR3","first-page":"11","volume":"22","author":"D Doll\u00e9","year":"2003","unstructured":"Doll\u00e9, D., Essam\u00e9, D., Falampin, J.: 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":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11955757_21","volume-title":"B 2007: Formal Specification and Development in B","author":"D Essam\u00e9","year":"2006","unstructured":"Essam\u00e9, D., Doll\u00e9, D.: B in large-scale projects: the canarsie line CBTC experience. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 252\u2013254. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11955757_21"},{"issue":"6","key":"20_CR5","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. Formal Asp. Comput. 23(6), 683\u2013709 (2011)","journal-title":"Formal Asp. Comput."},{"key":"20_CR6","unstructured":"Lecomte, T., Burdy, L., Leuschel, M.: Formally Checking Large Data Sets in the Railways. CoRR, abs\/1210.6815 (2012)"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-30885-7_34","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D Sabatier","year":"2012","unstructured":"Sabatier, D., Burdy, L., Requet, A., Gu\u00e9ry, J.: Formal proofs for the NYCT Line 7 (flushing) modernization project. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 369\u2013372. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-30885-7_34"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-33951-1_2","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"D Sabatier","year":"2016","unstructured":"Sabatier, D.: Using formal proof and B method at system level for industrial projects. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 20\u201331. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-33951-1_2"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-68499-4_10","volume-title":"RSSRail 2017","author":"M Comptier","year":"2017","unstructured":"Comptier, M., D\u00e9harbe, D., Perez, J.M., Mussat, L., Pierre, T., Sabatier, D.: Safety analysis of a CBTC system: a rigorous approach with Event-B. In: Fantechi, A., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2017. LNCS, vol. 10598, pp. 148\u2013159. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-68499-4_10"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-33600-8_10","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Hansen","year":"2016","unstructured":"Hansen, D., Schneider, D., Leuschel, M.: Using B and ProB for data validation projects. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 167\u2013182. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-33600-8_10"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-319-19249-9_30","volume-title":"FM 2015: Formal Methods","author":"D Schneider","year":"2015","unstructured":"Schneider, D., Leuschel, M., Witt, T.: Model-based problem solving for university timetable validation and improvement. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 487\u2013495. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19249-9_30"},{"key":"20_CR13","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":"20_CR14","unstructured":"ERTMS\/ETCS Baseline 3. System Requirements Specification Ref: SUBSET-026-3, Issue: 3.0.0, EEIG ERTMS Users Group, 123\u2013133 Rue Froissart, 1040 Brussels, Belgium, December 2008"},{"key":"20_CR15","unstructured":"Bendisposto, J., Clark, J., Dobrikov, I., K\u00f6rner, P., Krings, S., Ladenberger, L., Leuschel, M., Plagge, D.: Prob 2.0 Tutorial. In: Proceedings of the 4th Rodin User and Developer Workshop, TUCS Lecture Notes, Turku, June 2013. Turku Centre for Computer Science"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-04570-7_17","volume-title":"Formal Methods for Industrial Critical Systems","author":"L Ladenberger","year":"2009","unstructured":"Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising Event-B models with B-motion studio. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 202\u2013204. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-04570-7_17"},{"key":"20_CR17","unstructured":"Ladenberger, L.: Rapid creation of interactive formal prototypes for validating safety-critical systems. Ph.D. thesis, University of D\u00fcsseldorf, Germany (2017)"},{"key":"20_CR18","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-319-07512-9_5","volume-title":"ABZ 2014: The Landing Gear Case Study","author":"D Hansen","year":"2014","unstructured":"Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 66\u201379. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-07512-9_5"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91271-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,5,7]],"date-time":"2018-05-07T10:41:33Z","timestamp":1525689693000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91271-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319912707","9783319912714"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91271-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}