{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T22:34:40Z","timestamp":1784932480049,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642541070","type":"print"},{"value":"9783642541087","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54108-7_14","type":"book-chapter","created":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T10:09:36Z","timestamp":1389780576000},"page":"262-280","source":"Crossref","is-referenced-by-count":26,"title":["Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving"],"prefix":"10.1007","author":[{"given":"Liang","family":"Zou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jidong","family":"Lv","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shuling","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tao","family":"Tang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lei","family":"Yuan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yu","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol.\u00a0736, pp. 209\u2013229. Springer, Heidelberg (1993)"},{"key":"14_CR2","unstructured":"He, J.: From CSP to hybrid systems. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, pp. 171\u2013189. Prentice Hall International (UK) Ltd. (1994)"},{"key":"14_CR3","unstructured":"Heilmann, S.T.: Proof Support for Duration Calculus. PhD thesis, Technical University of Denmark (1999)"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278\u2013292. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561342"},{"issue":"4","key":"14_CR5","first-page":"301","volume":"9","author":"J. Hoenicke","year":"2002","unstructured":"Hoenicke, J., Olderog, E.: CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nord. J. Comput.\u00a09(4), 301\u2013334 (2002)","journal-title":"Nord. J. Comput."},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17164-2_1","volume-title":"Programming Languages and Systems","author":"J. Liu","year":"2010","unstructured":"Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol.\u00a06461, pp. 1\u201315. Springer, Heidelberg (2010)"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT 2011, pp. 97\u2013106. ACM (2011)","DOI":"10.1145\/2038642.2038659"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-57318-6_22","volume-title":"Hybrid Systems","author":"Z. Manna","year":"1993","unstructured":"Manna, Z., Pnueli, A.: Verifying hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol.\u00a0736, pp. 4\u201335. Springer, Heidelberg (1993)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/3-540-64358-3_47","volume-title":"Hybrid Systems: Computation and Control","author":"Z. Manna","year":"1998","unstructured":"Manna, Z., Sipma, H.: Deductive verification of hybrid systems using STeP. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol.\u00a01386, pp. 305\u2013318. Springer, Heidelberg (1998)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Moszkowski, B.C., Manna, Z.: Reasoning in interval temporal logic. In: Clarke, E., Kozen, D. (eds.) Logic of Programs, vol.\u00a0164, pp. 371\u2013382. Springer, Heidelberg (1983)","DOI":"10.1007\/3-540-12896-4_374"},{"issue":"2","key":"14_CR11","doi-asserted-by":"publisher","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. Journal of Automated Reasoning\u00a041(2), 143\u2013189 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR12","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.: European train control system: A case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol.\u00a05885, pp. 246\u2013265. Springer, Heidelberg (2009)"},{"key":"14_CR13","unstructured":"Rasmussen, T.M.: Interval Logic - Proof Theory and Theorem Proving. PhD thesis, Technical University of Denmark (2002)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/3-540-58468-4_189","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J.U. Skakkebaek","year":"1994","unstructured":"Skakkebaek, J.U., Shankar, N.: Towards a duration calculus proof assistant in PVS. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol.\u00a0863, pp. 660\u2013679. Springer, Heidelberg (1994)"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-30142-4_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wildmoser","year":"2004","unstructured":"Wildmoser, M., Nipkow, T.: Certifying machine code safety: Shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 305\u2013320. Springer, Heidelberg (2004)"},{"key":"14_CR16","unstructured":"Zhang, S.: CTCS-3 Technology Specification. China Railway Publishing House (2008)"},{"key":"14_CR17","unstructured":"Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. Series: Monographs in Theoretical Computer Science. An EATCS Series. Springer (2004)"},{"issue":"5","key":"14_CR18","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C. Zhou","year":"1991","unstructured":"Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters\u00a040(5), 269\u2013276 (1991)","journal-title":"Information Processing Letters"},{"key":"14_CR19","unstructured":"Zhou, C., Li, X.: A mean-value duration calculus. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, pp. 432\u2013451. Prentice-Hall International (1994)"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/BFb0020972","volume-title":"Hybrid Systems III","author":"C. Zhou","year":"1996","unstructured":"Zhou, C., Wang, J., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 511\u2013530. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54108-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T14:49:55Z","timestamp":1746110995000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54108-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642541070","9783642541087"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54108-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}