{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:05:05Z","timestamp":1746745505259},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319684987"},{"type":"electronic","value":"9783319684994"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68499-4_12","type":"book-chapter","created":{"date-parts":[[2017,10,18]],"date-time":"2017-10-18T10:35:37Z","timestamp":1508322937000},"page":"173-191","source":"Crossref","is-referenced-by-count":12,"title":["Formal Verification of Train Control with Air Pressure Brakes"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Mitsch","sequence":"first","affiliation":[]},{"given":"Marco","family":"Gario","sequence":"additional","affiliation":[]},{"given":"Christof J.","family":"Budnik","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Golm","sequence":"additional","affiliation":[]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,10,19]]},"reference":[{"key":"12_CR1","volume-title":"The B-book - Assigning Programs to Meanings","author":"J Abrial","year":"2005","unstructured":"Abrial, J.: The B-book - Assigning Programs to Meanings. Cambridge University Press, New York (2005)"},{"key":"12_CR2","unstructured":"Ahmad, H.A.: Dynamic braking control for accurate train braking distance estimation under different operating conditions (2013)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Bohrer, B., Rahli, V., Vukotic, I., V\u00f6lp, M., Platzer, A.: Formally verified differential dynamic logic. In: Bertot, Y., Vafeiadis, V. (eds.) Certified Programs and Proofs - 6th ACM SIGPLAN Conference, Cp. 2017, Paris, France, January 16\u201317, 2017, pp. 208\u2013221. ACM (2017)","DOI":"10.1145\/3018610.3018616"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-319-05032-4_18","volume-title":"Software Engineering and Formal Methods","author":"A Bonacchi","year":"2014","unstructured":"Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M., Cipriani, L.: Validation of railway interlocking systems by formal verification, a case study. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 237\u2013252. Springer, Cham (2014). doi:\n10.1007\/978-3-319-05032-4_18"},{"issue":"4","key":"12_CR5","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/s001650050021","volume":"10","author":"A Bor\u00e4lv","year":"1998","unstructured":"Bor\u00e4lv, A.: Case study: Formal verification of a computerized railway interlocking. Formal Aspects Comput. 10(4), 338\u2013360 (1998)","journal-title":"Formal Aspects Comput."},{"key":"12_CR6","unstructured":"Brossaeu, J., Ede, B.M.: Development of an adaptive predictive braking enforcement algorithm. Technical report FRA\/DOT\/ORD-9\/13, Federal Railroad Administration (2009)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-31424-7_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T., Roveri, M., Sanseviero, A., Tchaltsev, A.: Formal verification and validation of ERTMS industrial railway train spacing system. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 378\u2013393. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-31424-7_29"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-49646-7_22","volume-title":"Computer Safety, Reliability and Security","author":"A Cimatti","year":"1998","unstructured":"Cimatti, A., Giunchiglia, F., Mongardi, G., Romano, D., Torielli, F., Traverso, P.: Model checking safety critical software with spin: an application to a railway interlocking system. In: Ehrenberger, W. (ed.) SAFECOMP 1998. LNCS, vol. 1516, pp. 284\u2013293. Springer, Heidelberg (1998). doi:\n10.1007\/3-540-49646-7_22"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-30101-1_4","volume-title":"Formal Methods for Components and Objects","author":"W Damm","year":"2004","unstructured":"Damm, W., Hungar, H., Olderog, E.-R.: On the verification of cooperating traffic agents. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 77\u2013110. Springer, Heidelberg (2004). doi:\n10.1007\/978-3-540-30101-1_4"},{"key":"12_CR10","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). doi:\n10.1007\/11955757_21"},{"key":"12_CR11","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-3-642-33170-1_4","volume-title":"Industrial Deployment of System Engineering Methods","author":"J Falampin","year":"2013","unstructured":"Falampin, J., Le-Dang, H., Leuschel, M., Mokrani, M., Plagge, D.: Improving railway data validation with ProB. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 27\u201343. Springer, Berlin (2013)"},{"issue":"7","key":"12_CR12","doi-asserted-by":"crossref","first-page":"828","DOI":"10.1016\/j.scico.2012.04.003","volume":"78","author":"A Ferrari","year":"2013","unstructured":"Ferrari, A., Fantechi, A., Magnani, G., Grasso, D., Tempestini, M.: The Metr\u00f4 Rio case study. Sci. Comput. Program. 78(7), 828\u2013842 (2013)","journal-title":"Sci. Comput. Program."},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera\u00a0X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 527\u2013538. Springer, Cham (2015). doi:\n10.1007\/978-3-319-21401-6_36"},{"issue":"2","key":"12_CR14","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s00165-009-0143-6","volume":"23","author":"AE Haxthausen","year":"2011","unstructured":"Haxthausen, A.E., Peleska, J., Kinder, S.: A formal approach for the construction and verification of railway control systems. Formal Asp. Comput. 23(2), 191\u2013219 (2011)","journal-title":"Formal Asp. Comput."},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Heitmeyer, C.L., Lynch, N.A.: The generalized railroad crossing: a case study in formal verification of real-time systems. In: RTSS, pp. 120\u2013131. IEEE Computer Society (1994)","DOI":"10.1109\/REAL.1994.342724"},{"key":"12_CR16","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/j.scico.2016.05.010","volume":"133","author":"LV Hong","year":"2017","unstructured":"Hong, L.V., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. 133, 91\u2013115 (2017)","journal-title":"Sci. Comput. Program."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Iliasov, A., Romanovsky, A.: Formal analysis of railway signalling data. In: HASE 2016, pp. 70\u201377. IEEE Computer Society (2016)","DOI":"10.1109\/HASE.2016.44"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/11408901_15","volume-title":"Dependable Computing - EDCC 5","author":"F Ortmeier","year":"2005","unstructured":"Ortmeier, F., Reif, W., Schellhorn, G.: Formal safety analysis of a radio-based railroad crossing using deductive cause-consequence analysis (DCCA). In: Cin, M., Ka\u00e2niche, M., Pataricza, A. (eds.) EDCC 2005. LNCS, vol. 3463, pp. 210\u2013224. Springer, Heidelberg (2005). doi:\n10.1007\/11408901_15"},{"issue":"2","key":"12_CR19","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas. 41(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reas."},{"key":"12_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010)"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logics of dynamical systems. In: LICS, pp. 13\u201324. IEEE (2012)","DOI":"10.1109\/LICS.2012.13"},{"issue":"2","key":"12_CR22","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/s10817-016-9385-1","volume":"59","author":"A Platzer","year":"2017","unstructured":"Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reas. 59(2), 219\u2013265 (2017)","journal-title":"J. Autom. Reas."},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-10373-5_13","volume-title":"Formal Methods and Software Engineering","author":"A Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D.: European train control system: a case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 246\u2013265. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-10373-5_13"},{"key":"12_CR24","unstructured":"Polivka, A., Ede, B.M., Drapa, J.: North american joint positive train control project. Technical report DOT\/FRA\/ORD-09\/04 (2009)"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-54108-7_14","volume-title":"Verified Software: Theories, Tools, Experiments","author":"L Zou","year":"2014","unstructured":"Zou, L., Lv, J., Wang, S., Zhan, N., Tang, T., Yuan, L., Liu, Y.: Verifying chinese train control system under a combined scenario by theorem proving. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 262\u2013280. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-642-54108-7_14"}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68499-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,18]],"date-time":"2017-10-18T10:38:10Z","timestamp":1508323090000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68499-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319684987","9783319684994"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68499-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}