{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:21:56Z","timestamp":1778498516403,"version":"3.51.4"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319486277","type":"print"},{"value":"9783319486284","type":"electronic"}],"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-48628-4_3","type":"book-chapter","created":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T07:45:31Z","timestamp":1488354331000},"page":"39-58","source":"Crossref","is-referenced-by-count":20,"title":["MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Mingshuai","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiao","family":"Han","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tao","family":"Tang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuling","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mengfei","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hengjun","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Liang","family":"Zou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,2]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Aerts, A., Mousavi, M.R., Reniers, M.: A tool prototype for model-based testing of cyber-physical systems. In: Leucker, M., Rueda, C., Valencia, D.F. (eds.) ICTAC 2015, pp. 563\u2013572. Springer International Publishing (2015)","DOI":"10.1007\/978-3-319-25150-9_32"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems. Lecture Notes in Computer Science, vol. 736, pp. 209\u2013229. Springer, Berlin, Heidelberg (1993)","DOI":"10.1007\/3-540-57318-6_30"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011, pp. 254\u2013257. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-19835-9_21"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Asarin, E., Dang, T., Maler, O.: The d\/dt tool for verification of hybrid systems. In: CAV 2002. Lecture Notes in Computer Science, vol. 2404, pp. 365\u2013370 (2002)","DOI":"10.1007\/3-540-45657-0_30"},{"key":"3_CR5","unstructured":"Chen, C., Dong, J.S., Sun, J.: A formal framework for modelling and validating Simulink diagrams. Form. Asp. Comput. 21(5), 451\u2013483 (2009)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow $$^*$$ : An analyzer for non-linear hybrid systems. In: CAV 2013. Lecture Notes in Computer Science, vol. 8044, pp. 258\u2013263 (2013)","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Chen, M., Ravn, A., Yang, M., Zhan, N., Zou, L.: A two-way path between formal and informal design of embedded systems. In: Proc. UTP 2016 (2016)","DOI":"10.1007\/978-3-319-52228-9_4"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. Lecture Notes in Computer Science, vol. 33, pp. 134\u2013183. Springer, Berlin, Heidelberg (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"3_CR9","unstructured":"Dang, T., Nahhal, T.: Coverage-guided test generation for continuous and hybrid systems. Form. Methods Syst. Des. 34(2), 183\u2013213 (2009)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1\u20132), 29\u201335 (1988)","DOI":"10.1016\/S0747-7171(88)80004-X"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS 2008. Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Deng, Y., Rajhans, A., Julius, A.A.: STRONG: a trajectory-based verification toolbox for hybrid systems. In: QEST 2013. Lecture Notes in Computer Science, vol. 8054, pp. 165\u2013168 (2013)","DOI":"10.1007\/978-3-642-40196-1_13"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: CAV 2010. Lecture Notes in Computer Science, vol. 6174, pp. 167\u2013170 (2010)","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for annotated Stateflow models. In: TACAS 2015. Lecture Notes in Computer Science, vol. 9035, pp. 68\u201382 (2015)","DOI":"10.1145\/2728606.2728646"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Eggers, A., Ramdani, N., Nedialkov, N., Fr\u00e4nzle, M.: Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods. In: SEFM 2011, pp. 172\u2013187. Springer-Verlag, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-24690-6_13"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Fulton, N., Mitsch, S., Quesel, J., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. CADE 2015, 527\u2013538 (2015)","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"3_CR17","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":"3_CR18","unstructured":"Hoare, C.: Communicating Sequential Processes, vol. 178. Prentice-hall Englewood Cliffs (1985)"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Kong, H., He, F., Song, X., Hung, W.N., Gu, M.: Exponential-condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. Lecture Notes in Computer Science, vol. 8044, pp. 242\u2013257. Springer, Berlin Heidelberg (2013)","DOI":"10.1007\/978-3-642-39799-8_17"},{"key":"3_CR20","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput 32(3), 231\u2013253 (2001)"},{"key":"3_CR21","doi-asserted-by":"crossref","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. Lecture Notes in Computer Science, vol. 6461, pp. 1\u201315. Springer, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-17164-2_1"},{"key":"3_CR22","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, New York, NY, USA (2011)","DOI":"10.1145\/2038642.2038659"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhan, N., Zhao, H., Zou, L.: Abstraction of elementary hybrid systems by variable transformation. In: FM 2015. Lecture Notes in Computer Science, vol. 9109, pp. 360\u2013377 (2015)","DOI":"10.1007\/978-3-319-19249-9_23"},{"key":"3_CR24","unstructured":"L\u00f6fberg, J.: YALMIP: a toolbox for modeling and optimization in MATLAB. In: Proceedings of the CACSD Conference. Taipei, Taiwan (2004). http:\/\/users.isy.liu.se\/johanl\/yalmip"},{"key":"3_CR25","unstructured":"L\u00f6fberg, J.: Pre- and post-processing sum-of-squares programs in practice. IEEE Trans. Autom. Control 54(5), 1007\u20131011 (2009)"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Verifying hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems. Lecture Notes in Computer Science, vol. 736, pp. 4\u201335. Springer, Berlin, Heidelberg (1993)","DOI":"10.1007\/3-540-57318-6_22"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293\u2013320 (2003)","DOI":"10.1007\/s10107-003-0387-5"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Logic Comput. 20(1), 309\u2013352 (2010)","DOI":"10.1093\/logcom\/exn070"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. Lecture Notes in Computer Science, vol. 5123, pp. 176\u2013189. Springer, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-70545-1_17"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Platzer, A., Quesel, J.D.: KeYmaera: a hybrid theorem prover for hybrid systems. In: IJCAR 2008. Lecture Notes in Computer Science, vol. 5195, pp. 171\u2013178. Springer, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-71070-7_15"},{"key":"3_CR31","unstructured":"Simulink User\u2019s Guide. http:\/\/www.mathworks.com\/help\/pdf_doc\/simulink\/sl_using.pdf (2013)"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Toh, K.C., Todd, M., T\u00fct\u00fcnc\u00fc, R.H.: SDPT3 \u2013 a MATLAB software package for semidefinite programming. Optim. Methods Softw. 11, 545\u2013581 (1999)","DOI":"10.1080\/10556789908805762"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"T\u00fct\u00fcnc\u00fc, R.H., Toh, K.C., Todd, M.J.: Solving semidefinite-quadratic-linear programs using SDPT3. Math. Program. 95(2), 189\u2013217 (2003)","DOI":"10.1007\/s10107-002-0347-5"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Rev. 38(1), 49\u201395 (1996)","DOI":"10.1137\/1038003"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: ICFEM 2015. Lecture Notes in Computer Science, vol. 9407, pp. 382\u2013399 (2015)","DOI":"10.1007\/978-3-319-25423-4_25"},{"key":"3_CR36","doi-asserted-by":"crossref","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: FM 2014. Lecture Notes in Computer Science, vol. 8442, pp. 733\u2013748 (2014)","DOI":"10.1007\/978-3-319-06410-9_49"},{"key":"3_CR37","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-Verlag, Berlin Heidelberg (2004)"},{"key":"3_CR38","unstructured":"Zhou, C., Hoare, C., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991)"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Zhou, C., Wang, J., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) Hybrid Systems III. Lecture Notes in Computer Science, vol. 1066, pp. 511\u2013530. Springer, Berlin, Heidelberg (1996)","DOI":"10.1007\/BFb0020972"},{"key":"3_CR40","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. EMSOFT 2013, 1\u201310 (2013)","DOI":"10.1109\/EMSOFT.2013.6658587"},{"key":"3_CR41","doi-asserted-by":"crossref","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. Lecture Notes in Computer Science, vol. 8164, pp. 262\u2013280. Springer, Berlin Heidelberg (2014)","DOI":"10.1007\/978-3-642-54108-7_14"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Zou, L., Zhan, N., Wang, S., Fr\u00e4nzle, M.: Formal verification of Simulink\/Stateflow diagrams. In: ATVA 2015. Lecture Notes in Computer Science, vol. 9346, pp. 464\u2013481 (2015)","DOI":"10.1007\/978-3-319-24953-7_33"}],"container-title":["NASA Monographs in Systems and Software Engineering","Provably Correct Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48628-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,19]],"date-time":"2019-09-19T02:16:16Z","timestamp":1568859376000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48628-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319486277","9783319486284"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48628-4_3","relation":{},"ISSN":["1860-0131","2197-6597"],"issn-type":[{"value":"1860-0131","type":"print"},{"value":"2197-6597","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}