{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:07:55Z","timestamp":1762459675131},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030112448"},{"type":"electronic","value":"9783030112455"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-11245-5_27","type":"book-chapter","created":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T18:45:18Z","timestamp":1547145918000},"page":"577-600","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Mechanically Proving Determinacy of Hierarchical Block Diagram Translations"],"prefix":"10.1007","author":[{"given":"Viorel","family":"Preoteasa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Iulia","family":"Dragomir","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,11]]},"reference":[{"issue":"2","key":"27_CR1","doi-asserted-by":"publisher","first-page":"1003","DOI":"10.1007\/s10270-013-0358-0","volume":"14","author":"LA Rahim","year":"2015","unstructured":"Rahim, L.A., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003\u20131028 (2015)","journal-title":"Softw. Syst. Model."},{"key":"27_CR2","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. Electron. Notes Theor. Comput. Sci. 109, 43\u201356 (2004)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"3","key":"27_CR3","doi-asserted-by":"publisher","first-page":"1:1","DOI":"10.5381\/jot.2015.14.3.a1","volume":"14","author":"M Amrani","year":"2015","unstructured":"Amrani, M., et al.: Formal verification techniques for model transformations: a tridimensional classification. J. Object Technol. 14(3), 1:1\u201343 (2015)","journal-title":"J. Object Technol."},{"key":"27_CR4","unstructured":"Auger, C.: Compilation certifi\u00e9e de SCADE\/LUSTRE. (Certified compilation of SCADE\/LUSTRE). Ph.D. thesis, University of Paris-Sud, Orsay, France (2013). (in French)"},{"key":"27_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R-J Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998). https:\/\/doi.org\/10.1007\/978-1-4612-1674-2"},{"key":"27_CR6","unstructured":"Baez, J.C., Erbele, J.: Categories in control. CoRR, abs\/1405.6881 (2015)"},{"issue":"2","key":"27_CR7","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014)","journal-title":"J. Autom. Reason."},{"key":"27_CR8","unstructured":"Berry, G.: The constructive semantics of pure Esterel (1999)"},{"issue":"5","key":"27_CR9","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/2345141.2248437","volume":"47","author":"O Bouissou","year":"2012","unstructured":"Bouissou, O., Chapoutot, A.: An operational semantics for Simulink\u2019s simulation engine. SIGPLAN Not. 47(5), 129\u2013138 (2012)","journal-title":"SIGPLAN Not."},{"issue":"6","key":"27_CR10","doi-asserted-by":"publisher","first-page":"586","DOI":"10.1145\/3140587.3062358","volume":"52","author":"T Bourke","year":"2017","unstructured":"Bourke, T., Brun, L., Dagand, P.\u00c9., Leroy, X., Pouzet, M., Rieg, L.: A formally verified compiler for lustre. SIGPLAN Not. 52(6), 586\u2013601 (2017)","journal-title":"SIGPLAN Not."},{"key":"27_CR11","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2013.02.002","volume":"292","author":"D Calegari","year":"2013","unstructured":"Calegari, D., Szasz, N.: Verification of model transformations. Electron. Notes Theor. Comput. Sci. 292, 5\u201325 (2013)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"5","key":"27_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. Form. Asp. Comput. 21(5), 451\u2013483 (2009)","journal-title":"Form. Asp. Comput."},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/3-540-18771-5_49","volume-title":"Graph-Grammars and Their Application to Computer Science","author":"B Courcelle","year":"1987","unstructured":"Courcelle, B.: A representation of graphs by algebraic expressions and its use for graph rewriting systems. In: Ehrig, H., Nagl, M., Rozenberg, G., Rosenfeld, A. (eds.) Graph Grammars 1986. LNCS, vol. 291, pp. 112\u2013132. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-18771-5_49"},{"key":"27_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0479-7","volume-title":"Network Algebra","author":"G \u015etef\u0103nescu","year":"2000","unstructured":"\u015etef\u0103nescu, G.: Network Algebra. Springer, London (2000). https:\/\/doi.org\/10.1007\/978-1-4471-0479-7"},{"issue":"8","key":"27_CR15","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-32582-8_3","volume-title":"Model Checking Software","author":"I Dragomir","year":"2016","unstructured":"Dragomir, I., Preoteasa, V., Tripakis, S.: Compositional semantics and analysis of hierarchical block diagrams. In: Bo\u0161na\u010dki, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 38\u201356. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-32582-8_3"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-89963-3_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"I Dragomir","year":"2018","unstructured":"Dragomir, I., Preoteasa, V., Tripakis, S.: The refinement calculus of reactive systems toolset. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 201\u2013208. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_12"},{"key":"27_CR18","doi-asserted-by":"publisher","unstructured":"Dragomir, I., Preoteasa, V., Tripakis, S.: The refinement calculus of reactive systems toolset - February 2018. Figshare. https:\/\/doi.org\/10.6084\/m9.figshare.5900911 . Accessed Feb 2018","DOI":"10.6084\/m9.figshare.5900911"},{"key":"27_CR19","unstructured":"Eclipse: ATL - a model transformation technology. http:\/\/www.eclipse.org\/atl\/"},{"key":"27_CR20","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0167-6423(02)00096-5","volume":"48","author":"S Edwards","year":"2003","unstructured":"Edwards, S., Lee, E.A.: The semantics and execution of a synchronous block-diagram language. Sci. Comput. Prog. 48, 21\u201342(22) (2003)","journal-title":"Sci. Comput. Prog."},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Ghica, D.R., Jung, A.: Categorical semantics of digital circuits. In: Piskac, R., Talupur, M. (eds.) 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, 3\u20136 October 2016, pp. 41\u201348. IEEE (2016)","DOI":"10.1109\/FMCAD.2016.7886659"},{"key":"27_CR22","unstructured":"Ghica, D.R., Jung, A., Lopez, A.: Diagrammatic semantics for digital circuits. In: Goranko, V., Dam, M. (eds.) 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, LIPIcs, Stockholm, Sweden, vol. 82, pp. 24:1\u201324:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"27_CR23","doi-asserted-by":"publisher","first-page":"71","DOI":"10.4204\/EPTCS.266.4","volume":"266","author":"Dan R Ghica","year":"2018","unstructured":"Ghica, D.R., Lopez, A.: A structural and nominal syntax for diagrams. In: Coecke, B., Kissinger, A. (eds.) Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017, EPTCS, Nijmegen, The Netherlands, 3\u20137 July 2017, vol. 266, pp. 71\u201383 (2017)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"12","key":"27_CR24","doi-asserted-by":"publisher","first-page":"1259","DOI":"10.1016\/j.conengprac.2012.06.008","volume":"20","author":"C Yang","year":"2012","unstructured":"Yang, C., Vyatkin, V.: Transformation of Simulink models to IEC 61499 function blocks for verification of distributed control systems. Control Eng. Pract. 20(12), 1259\u20131269 (2012)","journal-title":"Control Eng. Pract."},{"key":"27_CR25","unstructured":"Leroy, X., Blazy, S., K\u00e4stner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert - a formally verified optimizing compiler. In: 8th European Congress on ERTS 2016: Embedded Real Time Software and Systems, Toulouse, France, January 2016. SEE"},{"issue":"3","key":"27_CR26","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10270-014-0429-x","volume":"15","author":"L L\u00facio","year":"2016","unstructured":"L\u00facio, L., et al.: Model transformation intents and their properties. Softw. Syst. Model. 15(3), 647\u2013684 (2016)","journal-title":"Softw. Syst. Model."},{"issue":"7","key":"27_CR27","doi-asserted-by":"publisher","first-page":"950","DOI":"10.1109\/43.293952","volume":"13","author":"S Malik","year":"1994","unstructured":"Malik, S.: Analysis of cyclic combinational circuits. IEEE Trans. Comput.-Aided Des. 13(7), 950\u2013956 (1994)","journal-title":"IEEE Trans. Comput.-Aided Des."},{"key":"27_CR28","unstructured":"MathWorks: Simulink. https:\/\/www.mathworks.com\/products\/simulink.html"},{"key":"27_CR29","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., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606\u2013620. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901433_33"},{"key":"27_CR30","doi-asserted-by":"crossref","unstructured":"Minopoli, S., Frehse, G.: SL2SX translator: from Simulink to SpaceEx models. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 93\u201398. ACM, New York (2016)","DOI":"10.1145\/2883817.2883826"},{"key":"27_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Dragomir, I., Tripakis, S.: Mechanically proving determinacy of hierarchical block diagram translations. CoRR, abs\/1611.01337 (2018)","DOI":"10.1007\/978-3-030-11245-5_27"},{"key":"27_CR33","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Tripakis, S.: Towards compositional feedback in non-deterministic and non-input-receptive systems. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 768\u2013777. ACM, New York (2016)","DOI":"10.1145\/2933575.2934503"},{"key":"27_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-10431-7_14","volume-title":"Software Engineering and Formal Methods","author":"R Reicherdt","year":"2014","unstructured":"Reicherdt, R., Glesner, S.: Formal verification of discrete-time MATLAB\/Simulink models using Boogie. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 190\u2013204. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_14"},{"key":"27_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-02658-4_57","volume-title":"Computer Aided Verification","author":"M Ryabtsev","year":"2009","unstructured":"Ryabtsev, M., Strichman, O.: Translation validation: from Simulink to C. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 696\u2013701. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_57"},{"key":"27_CR36","unstructured":"Schlesinger, S., Herber, P., G\u00f6thel, T., Glesner, S.: Proving transformation correctness of refactorings for discrete and continuous Simulink models. In: ICONS 2016, The Eleventh International Conference on Systems, EMBEDDED 2016, International Symposium on Advances in Embedded Systems and Applications, pp. 45\u201350. IARIA XPS Press (2016)"},{"issue":"2","key":"27_CR37","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/0022-0000(83)90038-7","volume":"27","author":"H Schmeck","year":"1983","unstructured":"Schmeck, H.: Algebraic characterization of reducible flowcharts. J. Comput. Syst. Sci. 27(2), 165\u2013199 (1983)","journal-title":"J. Comput. Syst. Sci."},{"key":"27_CR38","series-title":"Lecture Notes in Physics","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-12821-9_4","volume-title":"New Structures for Physics","author":"P Selinger","year":"2011","unstructured":"Selinger, P.: A survey of graphical languages for Monoidal categories. In: Coecke, B. (ed.) New Structures for Physics. LNP, vol. 813, pp. 289\u2013355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-12821-9_4"},{"key":"27_CR39","doi-asserted-by":"crossref","unstructured":"Sfyrla, V., Tsiligiannis, G., Safaka, I., Bozga, M., Sifakis, J.: Compositional translation of Simulink models into synchronous BIP. In: SIES, pp. 217\u2013220, July 2010","DOI":"10.1109\/SIES.2010.5551374"},{"key":"27_CR40","unstructured":"The Coq Development Team: The Coq proof assistant reference. INRIA, 2016. Version 8.5 (2016)"},{"issue":"4","key":"27_CR41","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":"27_CR42","unstructured":"Zanasi, F.: Interacting Hopf algebras - the theory of linear systems. (Interacting Hopf Algebras - la th\u00e9orie des syst\u00e8mes lin\u00e9aires). Ph.D. thesis, \u00c9cole normale sup\u00e9rieure de Lyon, France (2015)"},{"issue":"2","key":"27_CR43","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10626-010-0096-1","volume":"22","author":"C Zhou","year":"2012","unstructured":"Zhou, C., Kumar, R.: Semantic translation of Simulink diagrams to input\/output extended finite automata. Discret. Event Dyn. Syst. 22(2), 223\u2013247 (2012)","journal-title":"Discret. Event Dyn. Syst."},{"key":"27_CR44","doi-asserted-by":"crossref","unstructured":"Zou, L., Zhany, N., Wang, S., Franzle, M., Qin, S.: Verifying Simulink diagrams via a hybrid Hoare logic prover. In: EMSOFT, pp. 9:1\u20139:10, September 2013","DOI":"10.1109\/EMSOFT.2013.6658587"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-11245-5_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,22]],"date-time":"2020-11-22T07:08:14Z","timestamp":1606028894000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-11245-5_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030112448","9783030112455"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-11245-5_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cascais","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl19.sigplan.org\/track\/VMCAI-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}