{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T20:12:14Z","timestamp":1770408734661,"version":"3.49.0"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319296272","type":"print"},{"value":"9783319296289","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29628-9_6","type":"book-chapter","created":{"date-parts":[[2016,2,28]],"date-time":"2016-02-28T21:04:31Z","timestamp":1456693471000},"page":"290-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Combining Formal and Informal Methods in\u00a0the\u00a0Design of Spacecrafts"],"prefix":"10.1007","author":[{"given":"Mengfei","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,3,1]]},"reference":[{"key":"6_CR1","unstructured":"Simulink User\u2019s Guide (2013). http:\/\/www.mathworks.com\/help\/pdf_doc\/simulink\/sl_using.pdf"},{"key":"6_CR2","unstructured":"Stateflow User\u2019s Guide (2013). http:\/\/www.mathworks.com\/help\/pdf_doc\/stateflow\/sf_using.pdf"},{"key":"6_CR3","unstructured":"SysML V 1.4 Beta Specification (2013). http:\/\/www.omg.org\/spec\/SysML"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-88387-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A Eggers","year":"2008","unstructured":"Eggers, A., Fr\u00e4nzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171\u2013185. Springer, Heidelberg (2008)"},{"key":"6_CR5","first-page":"43","volume":"109","author":"A Agrawal","year":"2004","unstructured":"Agrawal, A., Simon, G., Karsai, G.: Semantic translation of simulink\/stateflow models to hybrid automata using graph transformations. Int. Workshop Graph Transform. Visual Model. Tech. 109, 43\u201356 (2004)","journal-title":"Int. Workshop Graph Transform. Visual Model. Tech."},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR\u201997: Concurrency Theory","author":"R Alur","year":"1997","unstructured":"Alur, R., Henzinger, T.A.: Modularity for timed and hybrid systems. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243. Springer, Heidelberg (1997)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Anta, A., Majumdar, R., Saha, I., Tabuada, P.: Automatic verification of control system implementations. In: EMSOFT 2010, pp. 9\u201318 (2010)","DOI":"10.1145\/1879021.1879024"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"Computer Aided Verification","author":"E Asarin","year":"2002","unstructured":"Asarin, E., Dang, T., Maler, O.: The $$\\mathbf{d\/dt}$$ tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365\u2013370. Springer, Heidelberg (2002)"},{"issue":"4","key":"6_CR9","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1109\/MC.2003.1193228","volume":"36","author":"F Balarin","year":"2003","unstructured":"Balarin, F., Watanabe, Y., Hsieh, H., Lavagno, L., Passerone, C., Sangiovanni-Vincentelli, A.L.: Metropolis: an integrated electronic system design environment. IEEE Comput. 36(4), 45\u201352 (2003)","journal-title":"IEEE Comput."},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/978-3-642-02658-4_46","volume-title":"Computer Aided Verification","author":"O Bouissou","year":"2009","unstructured":"Bouissou, O., Goubault, E., Putot, S., Tekkal, K., Vedrine, F.: HybridFluctuat: a static analyzer of numerical programs within a continuous environment. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 620\u2013626. Springer, Heidelberg (2009)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/11526841_18","volume-title":"FM 2005: Formal Methods","author":"A Cavalcanti","year":"2005","unstructured":"Cavalcanti, A., Clayton, P., O\u2019Halloran, C.: Control law diagrams in circus. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 253\u2013268. Springer, Heidelberg (2005)"},{"issue":"5","key":"6_CR12","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s00165-009-0108-9","volume":"21","author":"C Chen","year":"2009","unstructured":"Chen, C., Dong, J.S., Sun, J.: A formal framework for modeling and validating simulink diagrams. Formal Asp. Comput. 21(5), 451\u2013483 (2009)","journal-title":"Formal Asp. Comput."},{"key":"6_CR13","unstructured":"Chen, M., Han, X., Tang, T., Wang, S., Yang, M., Zhan, N., Zhao, H., Zou, L.: MARS: A toolchain for modeling, analysis and verification of spacecraft control systems. Technical Report ISCAS-SKLCS-15-04, State Key Laboratories of Computer Science, Institute of Software, CAS (2015)"},{"key":"6_CR14","unstructured":"Chen, M., Ravn, A., Yang, M., Zhan, N., Zou, L.: A two-way path between formal and informal design of embedded systems. Technical Report ISCAS-SKLCS-15-06, State Key Laboratories of Computer Science, Institute of Software, Chinese Academy of Sciences (2015)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013)"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/11575467_10","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2005","unstructured":"Cousot, P.: Integrating physical systems in the static analysis of embedded control software. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 135\u2013138. Springer, Heidelberg (2005)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-40196-1_13","volume-title":"Quantitative Evaluation of Systems","author":"Y Deng","year":"2013","unstructured":"Deng, Y., Rajhans, A., Julius, A.A.: STRONG: a trajectory-based verification toolbox for hybrid systems. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 165\u2013168. Springer, Heidelberg (2013)"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167\u2013170. Springer, Heidelberg (2010)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-662-46681-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PS Duggirala","year":"2015","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68\u201382. Springer, Heidelberg (2015)"},{"issue":"1","key":"6_CR20","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1109\/JPROC.2002.805829","volume":"91","author":"J Eker","year":"2003","unstructured":"Eker, J., Janneck, J., Lee, E.A., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., Xiong, Y.: Taming heterogeneity - the ptolemy approach. Proc. IEEE 91(1), 127\u2013144 (2003)","journal-title":"Proc. IEEE"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Esteve, M.-A., Katoen, J.-P., Nguyen, V., Postma, B., Yushtein, Y.: Formal correctness, safety, dependability, and performance analysis of a satellite. In: ICSE 2012, pp. 1022\u20131031 (2012)","DOI":"10.1109\/ICSE.2012.6227118"},{"key":"6_CR22","unstructured":"Goubault, E., Martel, M., Putot, S.: Some future challenges in the validation of control systems. In: ERTS 2006 (2006)"},{"issue":"5","key":"6_CR23","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-007-0049-7","volume":"9","author":"G Hamon","year":"2007","unstructured":"Hamon, G., Rushby, J.: An operational semantics for stateflow. Int. J. Softw. Tools Technol. Transf. 9(5), 447\u2013456 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"6_CR24","first-page":"171","volume-title":"A Classical Mind, Essays in Honour of C.A.R. Hoare","author":"J He","year":"1994","unstructured":"He, J.: From CSP to hybrid systems. In: Roscoe, A.W. (ed.) A Classical Mind, Essays in Honour of C.A.R. Hoare, pp. 171\u2013189. Prentice Hall International (UK) Ltd, Hertfordshire (1994)"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278\u2013292, July 1996","DOI":"10.1109\/LICS.1996.561342"},{"key":"6_CR26","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming, vol. 14. Prentice Hall, Englewood Cliffs (1998)"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-32759-9_22","volume-title":"FM 2012: Formal Methods","author":"TT Johnson","year":"2012","unstructured":"Johnson, T.T., Green, J., Mitra, S., Dudley, R., Erwin, R.S.: Satellite rendezvous and conjunction avoidance: case studies in verification of nonlinear hybrid systems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 252\u2013266. Springer, Heidelberg (2012)"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-39799-8_17","volume-title":"Computer Aided Verification","author":"H Kong","year":"2013","unstructured":"Kong, H., He, F., Song, X., Hung, W.N.N., Gu, M.: Exponential-condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 242\u2013257. Springer, Heidelberg (2013)"},{"key":"6_CR29","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. 6461, pp. 1\u201315. Springer, Heidelberg (2010)"},{"key":"6_CR30","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 (2011)","DOI":"10.1145\/2038642.2038659"},{"issue":"4","key":"6_CR31","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/s11786-012-0133-6","volume":"6","author":"J Liu","year":"2012","unstructured":"Liu, J., Zhan, N., Zhao, H.: Automatically discovering relaxed lyapunov functions for polynomial dynamical systems. Math. Comput. Sci. 6(4), 395\u2013408 (2012)","journal-title":"Math. Comput. Sci."},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-319-19249-9_23","volume-title":"FM 2015: Formal Methods","author":"J Liu","year":"2015","unstructured":"Liu, J., Zhan, N., Zhao, H., Zou, L.: Abstraction of elementary hybrid systems by variable transformation. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 360\u2013377. Springer, Heidelberg (2015)"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-28891-3_33","volume-title":"NASA Formal Methods","author":"R Majumdar","year":"2012","unstructured":"Majumdar, R., Saha, I., Shashidhar, K.C., Wang, Z.: CLSE: closed-loop symbolic execution. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 356\u2013370. Springer, Heidelberg (2012)"},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/11901433_33","volume-title":"Formal Methods and Software Engineering","author":"B Meenakshi","year":"2006","unstructured":"Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606\u2013620. Springer, Heidelberg (2006)"},{"issue":"2","key":"6_CR35","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/1646353.1646372","volume":"53","author":"SP Miller","year":"2010","unstructured":"Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58\u201364 (2010)","journal-title":"Commun. ACM"},{"issue":"2","key":"6_CR36","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. J. Autom. Reasoning 41(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"6_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-540-70545-1_17","volume-title":"Computer Aided Verification","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 176\u2013189. Springer, Heidelberg (2008)"},{"key":"6_CR38","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008)"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"Scaife, N., Sofronis, C., Caspi, P., Tripakis, S., Maraninchi, F.: Defining and translating a safe subset of simulink\/stateflow into lustre. In: EMSOFT 2004, pp. 259\u2013268. ACM (2004)","DOI":"10.1145\/1017753.1017795"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Selic, B., Gerard, S.: Modeling and Analysis or Real-Time and Embedded Systems with UML and MARTE: Developing Cyber-Physical Systems. The MK\/OMG Press, Burlington (2013)","DOI":"10.1016\/B978-0-12-416619-6.00008-0"},{"key":"6_CR41","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-1561-6","volume-title":"Introduction to Physical Modeling with Modelica","author":"M Tiller","year":"2001","unstructured":"Tiller, M.: Introduction to Physical Modeling with Modelica, vol. 615. Springer, New York (2001)"},{"key":"6_CR42","unstructured":"Tiwari, A.: Formal semantics and analysis methods for Simulink Stateflow models. Technical report, SRI International, (2002)"},{"issue":"4","key":"6_CR43","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1145\/1113830.1113834","volume":"4","author":"S Tripakis","year":"2005","unstructured":"Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embed. Comput. Syst. 4(4), 779\u2013818 (2005)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"6_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-29952-0_13","volume-title":"Theory and Applications of Models of Computation","author":"S Wang","year":"2012","unstructured":"Wang, S., Zhan, N., Guelev, D.: An assume\/guarantee based compositional calculus for hybrid CSP. In: Agrawal, M., Cooper, S.B., Li, A. (eds.) TAMC 2012. LNCS, vol. 7287, pp. 72\u201383. Springer, Heidelberg (2012)"},{"key":"6_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-25423-4_25","volume-title":"Formal Methods and Software Engineering","author":"S Wang","year":"2015","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved hhl prover: an interactive theorem prover for hybrid systems. In: Butler, M., et al. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382\u2013399. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-25423-4_25"},{"key":"6_CR46","unstructured":"Zhan, N., Wang, S., Guelev, D.: Extending Hoare logic to hybrid systems. Technical report ISCAS-SKLCS-13-02, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (2013)"},{"key":"6_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-39721-9_5","volume-title":"Unifying Theories of Programming and Formal Engineering Methods","author":"N Zhan","year":"2013","unstructured":"Zhan, N., Wang, S., Zhao, H.: Formal modelling, analysis and verification of hybrid systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Unifying Theories of Programming and Formal Engineering Methods. LNCS, vol. 8050, pp. 207\u2013281. Springer, Heidelberg (2013)"},{"key":"6_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1007\/978-3-319-06410-9_49","volume-title":"FM 2014: Formal Methods","author":"H Zhao","year":"2014","unstructured":"Zhao, H., Yang, M., Zhan, N., Gu, B., Zou, L., Chen, Y.: Formal verification of a descent guidance control program of a lunar lander. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 733\u2013748. Springer, Heidelberg (2014)"},{"key":"6_CR49","series-title":"Monographs in Theoretical Computer Science. An EATCS Series","volume-title":"Duration Calculus \u2013 A Formal Approach to Real-Time Systems","author":"C Zhou","year":"2004","unstructured":"Zhou, C., Hansen, M.R.: Duration Calculus \u2013 A Formal Approach to Real-Time Systems. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)"},{"issue":"5","key":"6_CR50","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.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991)","journal-title":"Inf. Process. Lett."},{"key":"6_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020972","volume-title":"Hybrid Systems III","author":"Z Chaochen","year":"1996","unstructured":"Chaochen, Z., Ji, W., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066. Springer, Heidelberg (1996)"},{"key":"6_CR52","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)"},{"key":"6_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-319-24953-7_33","volume-title":"Automated Technology for Verification and Analysis","author":"L Zou","year":"2015","unstructured":"Zou, L., Zhan, N., Wang, S., Fr\u00e4nzle, M.: Formal verification of simulink\/stateflow diagrams. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 464\u2013481. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-24953-7_33"},{"key":"6_CR54","doi-asserted-by":"crossref","unstructured":"Zou, L., Zhan, N., Wang, S., Fr\u00e4nzle, M., Qin, S.: Verifying Simulink diagrams via a hybrid hoare logic prover. In: EMSOFT 2013, pp. 1\u201310 (2013)","DOI":"10.1109\/EMSOFT.2013.6658587"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29628-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T09:57:47Z","timestamp":1770371867000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-29628-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296272","9783319296289"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29628-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"1 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}