{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:59:44Z","timestamp":1770753584501,"version":"3.50.0"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,6,12]],"date-time":"2017-06-12T00:00:00Z","timestamp":1497225600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1007\/s10009-017-0458-1","type":"journal-article","created":{"date-parts":[[2017,6,12]],"date-time":"2017-06-12T14:44:12Z","timestamp":1497278652000},"page":"87-104","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Hybrid automata: from verification to implementation"],"prefix":"10.1007","volume":"21","author":[{"given":"Stanley","family":"Bak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Omar Ali","family":"Beg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergiy","family":"Bogomolov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luan Viet","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Schilling","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,6,12]]},"reference":[{"key":"458_CR1","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.entcs.2004.02.055","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. Electr. Notes Theor. Comput. Sci 109, 43\u201356 (2004). doi: 10.1016\/j.entcs.2004.02.055","journal-title":"Electr. Notes Theor. Comput. Sci"},{"issue":"1","key":"458_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlap.2012.07.001","volume":"82","author":"DEN Agut","year":"2013","unstructured":"Agut, D.E.N., van Beek, D.A., Rooda, J.E.: Syntax and semantics of the compositional interchange format for hybrid systems. J. Log. Algebr. Program 82(1), 1\u201352 (2013). doi: 10.1016\/j.jlap.2012.07.001","journal-title":"J. Log. Algebr. Program"},{"key":"458_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Kanade, A., Ramesh, S., Shashidhar, K.C.: Symbolic analysis for improving simulation coverage of Simulink\/Stateflow models. In: EMSOFT, pp. 89\u201398. ACM (2008). doi: 10.1145\/1450058.1450071","DOI":"10.1145\/1450058.1450071"},{"key":"458_CR4","doi-asserted-by":"publisher","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G.E., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: TACAS, vol. 6605, pp. 254\u2013257. Springer (2011). doi: 10.1007\/978-3-642-19835-9_21","DOI":"10.1007\/978-3-642-19835-9_21"},{"key":"458_CR5","doi-asserted-by":"publisher","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: HSCC, pp. 128\u2013133, ACM (2015). doi: 10.1145\/2728606.2728630","DOI":"10.1145\/2728606.2728630"},{"key":"458_CR6","doi-asserted-by":"publisher","unstructured":"Bak, S., Johnson, T.T.: Periodically-scheduled controller analysis using hybrid systems reachability and continuization. In: RTSS, pp. 195\u2013205. IEEE Computer Society (2015). doi: 10.1109\/RTSS.2015.26","DOI":"10.1109\/RTSS.2015.26"},{"key":"458_CR7","doi-asserted-by":"publisher","unstructured":"Balasubramanian, D., Pasareanu, C.S., Whalen, M.W., Karsai, G., Lowry, M.R.: Polyglot: modeling and analysis for multiple statechart formalisms. In: ISSTA, pp. 45\u201355. ACM (2011), doi: 10.1145\/2001420.2001427","DOI":"10.1145\/2001420.2001427"},{"issue":"4","key":"458_CR8","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/s10009-015-0393-y","volume":"18","author":"S Bogomolov","year":"2016","unstructured":"Bogomolov, S., Donz\u00e9, A., Frehse, G., Grosu, R., Johnson, T.T., Ladan, H., Podelski, A., Wehrle, M.: Guided search for hybrid systems based on coarse-grained space abstractions. STTT 18(4), 449\u2013467 (2016). doi: 10.1007\/s10009-015-0393-y","journal-title":"STTT"},{"key":"458_CR9","doi-asserted-by":"publisher","unstructured":"Bogomolov, S., Frehse, G., Greitschus, M., Grosu, R., Pasareanu, C.S., Podelski, A., Strump, T.: Assume-guarantee abstraction refinement meets hybrid systems. In: HVC. LNCS, vol. 8855, pp. 116\u2013131. Springer (2014). doi: 10.1007\/978-3-319-13338-6_10","DOI":"10.1007\/978-3-319-13338-6_10"},{"key":"458_CR10","doi-asserted-by":"publisher","unstructured":"Bogomolov, S., Frehse, G., Grosu, R., Ladan, H., Podelski, A., Wehrle, M.: A box-based distance between regions for guiding the reachability analysis of SpaceEx. In: CAV. LNCS, vol. 7358, pp. 479\u2013494. Springer (2012). doi: 10.1007\/978-3-642-31424-7_35","DOI":"10.1007\/978-3-642-31424-7_35"},{"key":"458_CR11","doi-asserted-by":"publisher","unstructured":"Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., Grosu, R.: Abstraction-based parameter synthesis for multiaffine systems. In: HVC. LNCS, vol. 9434, pp. 19\u201335. Springer (2015). doi: 10.1007\/978-3-319-26287-1_2","DOI":"10.1007\/978-3-319-26287-1_2"},{"key":"458_CR12","doi-asserted-by":"publisher","unstructured":"Bouissou, O., Chapoutot, A.: An operational semantics for Simulink\u2019s simulation engine. In: LCTES, pp. 129\u2013138. ACM (2012). doi: 10.1145\/2248418.2248437","DOI":"10.1145\/2248418.2248437"},{"key":"458_CR13","unstructured":"Carloni, L., Di\u00a0Benedetto, M.D., Pinto, A., Sangiovanni-Vincentelli, A.: Modeling techniques, programming languages, design toolsets and interchange formats for hybrid systems. Tech. Rep. (2004)"},{"key":"458_CR14","doi-asserted-by":"publisher","unstructured":"Carloni, L.P., Passerone, R., Pinto, A., Sangiovanni-Vincentelli, A.L.: Languages and tools for hybrid systems design. In: Foundations and Trends in Electronic Design Automation 1(1\/2) (2006). doi: 10.1561\/1000000001","DOI":"10.1561\/1000000001"},{"key":"458_CR15","doi-asserted-by":"crossref","unstructured":"Chen, M., Ravn, A.P., Wang, S., Yang, M., Zhan, N.: A two-way path between formal and informal design of embedded systems. In: UTP. LNCS, vol. 10134, pp. 65\u201392. Springer (2016)","DOI":"10.1007\/978-3-319-52228-9_4"},{"key":"458_CR16","doi-asserted-by":"publisher","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: CAV. LNCS, vol. 8044, pp. 258\u2013263. Springer (2013). doi: 10.1007\/978-3-642-39799-8_18","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"458_CR17","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: ATVA. LNCS, vol. 6996, pp. 1\u201312. Springer (2011). doi: 10.1007\/978-3-642-24372-1_1","DOI":"10.1007\/978-3-642-24372-1_1"},{"key":"458_CR18","doi-asserted-by":"publisher","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: CAV. LNCS, vol. 6174, pp. 167\u2013170. Springer (2010). doi: 10.1007\/978-3-642-14295-6_17","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"458_CR19","doi-asserted-by":"publisher","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: EMSOFT, pp. 26:1\u201326:10. IEEE (2013). doi: 10.1109\/EMSOFT.2013.6658604","DOI":"10.1109\/EMSOFT.2013.6658604"},{"issue":"1","key":"458_CR20","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1109\/10.68209","volume":"38","author":"ME Fisher","year":"1991","unstructured":"Fisher, M.E.: A semiclosed-loop algorithm for the control of blood glucose levels in diabetics. IEEE Trans. Biomed. Eng. 38(1), 57\u201361 (1991)","journal-title":"IEEE Trans. Biomed. Eng."},{"key":"458_CR21","doi-asserted-by":"publisher","unstructured":"Frehse, G., Guernic, C.L., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. LNCS, vol. 6806, pp. 379\u2013395. Springer (2011). doi: 10.1007\/978-3-642-22110-1_30","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"458_CR22","doi-asserted-by":"publisher","unstructured":"Hamon, G.: A denotational semantics for Stateflow. In: EMSOFT, pp. 164\u2013172. ACM (2005). doi: 10.1145\/1086228.1086260","DOI":"10.1145\/1086228.1086260"},{"issue":"5\u20136","key":"458_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.M.: An operational semantics for Stateflow. STTT 9(5\u20136), 447\u2013456 (2007). doi: 10.1007\/s10009-007-0049-7","journal-title":"STTT"},{"key":"458_CR24","unstructured":"Hybrid Automata: From verification to implementation\u2014supplementary material. http:\/\/swt.informatik.uni-freiburg.de\/tool\/spaceex\/ha2slsf"},{"issue":"2","key":"458_CR25","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10009-013-0289-7","volume":"16","author":"Z Jiang","year":"2014","unstructured":"Jiang, Z., Pajic, M., Alur, R., Mangharam, R.: Closed-loop verification of medical devices with model abstraction and refinement. STTT 16(2), 191\u2013213 (2014). doi: 10.1007\/s10009-013-0289-7","journal-title":"STTT"},{"issue":"3","key":"458_CR26","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/S0167-6911(99)00059-6","volume":"38","author":"KH Johansson","year":"1999","unstructured":"Johansson, K.H., Egerstedt, M., Lygeros, J., Sastry, S.: On the regularization of zeno hybrid automata. Syst. Control Lett. 38(3), 141\u2013150 (1999)","journal-title":"Syst. Control Lett."},{"issue":"1\u20132","key":"458_CR27","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1\u20132), 134\u2013152 (1997). doi: 10.1007\/s100090050010","journal-title":"STTT"},{"key":"458_CR28","unstructured":"Lavalle, S.M., Kuffner, J.J., Jr.: Rapidly-exploring random trees: progress and prospects. In: Donald, B., Lynch, K., Rus, D. (eds.) Algorithmic and Computational Robotics: New Directions, pp. 293\u2013308. A K Peters\/CRC Press (2000)"},{"key":"458_CR29","doi-asserted-by":"publisher","unstructured":"Manamcheri, K., Mitra, S., Bak, S., Caccamo, M.: A step towards verification and synthesis from Simulink\/Stateflow models. In: Proceedings of the 14th international conference on Hybrid systems: computation and control HSCC\u201911, pp. 317\u2013318. ACM (2011). doi: 10.1145\/1967701.1967749","DOI":"10.1145\/1967701.1967749"},{"key":"458_CR30","doi-asserted-by":"publisher","unstructured":"Minopoli, S., Frehse, G.: From simulation models to hybrid automata using urgency and relaxation. In: HSCC, pp. 287\u2013296. ACM (2016). doi: 10.1145\/2883817.2883825","DOI":"10.1145\/2883817.2883825"},{"key":"458_CR31","doi-asserted-by":"publisher","unstructured":"Minopoli, S., Frehse, G.: SL2SX translator: from Simulink to SpaceEx models. In: HSCC, pp. 93\u201398. ACM (2016). doi: 10.1145\/2883817.2883826","DOI":"10.1145\/2883817.2883826"},{"key":"458_CR32","doi-asserted-by":"crossref","unstructured":"Nguyen, L.V., Johnson, T.T.: Benchmark: DC-to-DC switched-mode power converters (buck converters, boost converters, and buck-boost converters). In: ARCH. EPiC Series in Computing, vol.\u00a034, pp. 19\u201324. EasyChair (2014). http:\/\/www.easychair.org\/publications\/paper\/Benchmark_DC-to-DC_Switched-Mode_Power_Converters_-Buck_Converters-_Boost_Converters-_and_Buck-Boost_Converters","DOI":"10.29007\/23pm"},{"key":"458_CR33","doi-asserted-by":"publisher","unstructured":"Pajic, M., Jiang, Z., Lee, I., Sokolsky, O., Mangharam, R.: From verification to implementation: a model translation tool and a pacemaker case study. In: RTAS, pp. 173\u2013184. IEEE Computer Society (2012). doi: 10.1109\/RTAS.2012.25","DOI":"10.1109\/RTAS.2012.25"},{"key":"458_CR34","doi-asserted-by":"publisher","unstructured":"Pajic, M., Jiang, Z., Lee, I., Sokolsky, O., Mangharam, R.: Safety-critical medical device development using the UPP2SF model translation tool. ACM Trans. Embed. Comput. Syst. 13(4s), 127:1\u2013127:26 (2014). doi: 10.1145\/2584651","DOI":"10.1145\/2584651"},{"issue":"1","key":"458_CR35","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/TII.2012.2226594","volume":"10","author":"M Pajic","year":"2014","unstructured":"Pajic, M., Mangharam, R., Sokolsky, O., Arney, D., Goldman, J.M., Lee, I.: Model-driven safety analysis of closed-loop medical systems. IEEE Trans. Ind. Inform. 10(1), 3\u201316 (2014). doi: 10.1109\/TII.2012.2226594","journal-title":"IEEE Trans. Ind. Inform."},{"key":"458_CR36","doi-asserted-by":"publisher","unstructured":"Pinto, A., Carloni, L.P., Passerone, R., Sangiovanni-Vincentelli, A.L.: Interchange format for hybrid systems: abstract semantics. In: HSCC. LNCS, vol. 3927, pp. 491\u2013506. Springer (2006). doi: 10.1007\/11730637_37","DOI":"10.1007\/11730637_37"},{"key":"458_CR37","doi-asserted-by":"publisher","unstructured":"Pinto, A., Sangiovanni-Vincentelli, A.L., Carloni, L.P., Passerone, R.: Interchange formats for hybrid systems: review and proposal. In: HSCC. LNCS, vol. 3414, pp. 526\u2013541. Springer (2005). doi: 10.1007\/978-3-540-31954-2_34","DOI":"10.1007\/978-3-540-31954-2_34"},{"key":"458_CR38","doi-asserted-by":"publisher","unstructured":"Sampath, P., Rajeev, A.C., Ramesh, S.: Translation validation for Stateflow to C. In: DAC, pp. 23:1\u201323:6. ACM (2014). doi: 10.1145\/2593069.2593237","DOI":"10.1145\/2593069.2593237"},{"key":"458_CR39","doi-asserted-by":"publisher","unstructured":"Sanfelice, R.G., Copp, D.A., Nanez, P.: A toolbox for simulation of hybrid systems in Matlab\/Simulink: hybrid equations (HyEQ) toolbox. In: HSCC, pp. 101\u2013106. ACM (2013). doi: 10.1145\/2461328.2461346","DOI":"10.1145\/2461328.2461346"},{"key":"458_CR40","doi-asserted-by":"publisher","unstructured":"Schrammel, P., Jeannet, B.: From hybrid data-flow languages to hybrid automata: a complete translation. In: HSCC, pp. 167\u2013176. ACM (2012). doi: 10.1145\/2185632.2185658","DOI":"10.1145\/2185632.2185658"},{"key":"458_CR41","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-8085-6","volume-title":"Modern DC-to-DC Switchmode Power Converter Circuits","author":"RP Severns","year":"1985","unstructured":"Severns, R.P., Bloom, G.: Modern DC-to-DC Switchmode Power Converter Circuits. Van Nostrand Reinhold Company, New York (1985)"},{"key":"458_CR42","unstructured":"Simulink Design Verifier. http:\/\/www.mathworks.com\/products\/sldesignverifier\/"},{"issue":"1","key":"458_CR43","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1109\/JPROC.2002.805818","volume":"91","author":"A Tiwari","year":"2003","unstructured":"Tiwari, A., Shankar, N., Rushby, J.M.: Invisible formal methods for embedded control systems. Proc. IEEE 91(1), 29\u201339 (2003)","journal-title":"Proc. IEEE"},{"key":"458_CR44","doi-asserted-by":"publisher","unstructured":"Yan, G., Jiao, L., Li, Y., Wang, S., Zhan, N.: Approximate bisimulation and discretization of hybrid CSP. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A., (eds.) FM. LNCS, vol. 9995, pp. 702\u2013720. Springer, Cham (2016) doi: 10.1007\/978-3-319-48989-6_43","DOI":"10.1007\/978-3-319-48989-6_43"},{"key":"458_CR45","doi-asserted-by":"publisher","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. LNCS, vol. 9364, pp. 464\u2013481. Springer, Cham (2015) doi: 10.1007\/978-3-319-24953-7_33","DOI":"10.1007\/978-3-319-24953-7_33"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0458-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0458-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0458-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T12:18:35Z","timestamp":1750335515000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0458-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,12]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["458"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0458-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,6,12]]},"assertion":[{"value":"12 June 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}