{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:10:51Z","timestamp":1770275451905,"version":"3.49.0"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T00:00:00Z","timestamp":1586217600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T00:00:00Z","timestamp":1586217600000},"content-version":"vor","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":[[2020,12]]},"DOI":"10.1007\/s10009-020-00561-4","type":"journal-article","created":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T12:03:52Z","timestamp":1586261032000},"page":"689-708","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["The Refinement Calculus of Reactive Systems Toolset"],"prefix":"10.1007","volume":"22","author":[{"given":"Iulia","family":"Dragomir","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viorel","family":"Preoteasa","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":[[2020,4,7]]},"reference":[{"key":"561_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. Electron. Notes Theor. Comput. Sci. 109, 43\u201356 (2004). Proceedings of the Workshop on Graph Transformation and Visual Modelling Techniques (GT-VMT 2004)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"561_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Grosu, R., Lee, I., Sokolsky, O.: Compositional refinement for hierarchical hybrid systems. In: 4th International Workshop on Hybrid Systems: Computation and Control, HSCC \u201901, pp. 33\u201348. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45351-2_7"},{"key":"561_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.: Reactive modules. Formal Methods Syst. Des. 15, 7\u201348 (1999)","journal-title":"Formal Methods Syst. Des."},{"key":"561_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus","author":"R-J Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus. Springer, Berlin (1998)"},{"key":"561_CR5","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u2019c, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan G., Qadeer S. (eds.) Proceedings of the 23rd International Conference on Computer Aided Verification (CAV \u201911). Lecture Notes in Computer Science, vol. 6806, pp. 171\u2013177. Springer, Utah (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"561_CR6","unstructured":"Boulton, R.J., Gordon, A., Gordon, M.J.C., Harrison, J., Herbert, J., Tassel, J.V.: Experience with embedding hardware description languages in HOL. In: IFIP TC10\/WG 10.2 International Conference on Theorem Provers in Circuit Design, pp. 129\u2013156. North-Holland Publishing Co., Amsterdam (1992)"},{"key":"561_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0091-5","volume-title":"Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement","author":"M Broy","year":"2001","unstructured":"Broy, M., St\u00f8len, K.: Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer, Berlin (2001)"},{"issue":"5","key":"561_CR8","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":"561_CR9","volume-title":"Interface automata. In Foundations of Software Engineering (FSE)","author":"L de Alfaro","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.: Interface automata. In Foundations of Software Engineering (FSE). ACM Press, New York (2001)"},{"key":"561_CR10","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Proceedings of the Theory and Practice of Software 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201908\/ETAPS\u201908, pp. 337\u2013340, Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"8","key":"561_CR11","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E Dijkstra","year":"1975","unstructured":"Dijkstra, E.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"561_CR12","volume-title":"Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits","author":"D Dill","year":"1987","unstructured":"Dill, D.: Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. MIT Press, Cambridge (1987)"},{"key":"561_CR13","first-page":"38","volume-title":"Compositional Semantics and Analysis of Hierarchical Block Diagrams. In SPIN","author":"I Dragomir","year":"2016","unstructured":"Dragomir, I., Preoteasa, V., Tripakis, S.: Compositional Semantics and Analysis of Hierarchical Block Diagrams. In SPIN, pp. 38\u201356. Springer, Berlin (2016)"},{"key":"561_CR14","first-page":"38","volume-title":"Compositional Semantics and Analysis of Hierarchical Block Diagrams. In SPIN","author":"I Dragomir","year":"2016","unstructured":"Dragomir, I., Preoteasa, V., Tripakis, S.: Compositional Semantics and Analysis of Hierarchical Block Diagrams. In SPIN, pp. 38\u201356. Springer, Berlin (2016)"},{"key":"561_CR15","doi-asserted-by":"publisher","unstructured":"Dragomir, I., Preoteasa, V., Tripakis, S.: The Refinement Calculus of Reactive Systems Toolset. figshare. (2018) Doi: https:\/\/doi.org\/10.6084\/m9.figshare.5900911","DOI":"10.6084\/m9.figshare.5900911"},{"key":"561_CR16","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver. Technical report, SRI International (2006)"},{"key":"561_CR17","doi-asserted-by":"crossref","unstructured":"Fan, C., Qi, B., Mitra, S., Viswanathan, M., Duggirala, P.S.: Automatic reachability analysis for nonlinear hybrid models with C2E2. In: Chaudhuri S., Farzan A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Lecture Notes in Computer Science, vol. 9779, pp. 531\u2013538. Springer, Berlin (2016)","DOI":"10.1007\/978-3-319-41528-4_29"},{"issue":"6","key":"561_CR18","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/113446.113468","volume":"26","author":"T Freeman","year":"1991","unstructured":"Freeman, T., Pfenning, F.: Refinement types for ML. SIGPLAN Not. 26(6), 268\u2013277 (1991)","journal-title":"SIGPLAN Not."},{"key":"561_CR19","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.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6806, pp. 379\u2013395. Springer, (2011)"},{"key":"561_CR20","doi-asserted-by":"crossref","DOI":"10.1002\/9781118989166","volume-title":"Principles of Object-Oriented Modeling and Simulation with Modelica 3.3: A Cyber-Physical Approach","author":"P Fritzson","year":"2014","unstructured":"Fritzson, P.: Principles of Object-Oriented Modeling and Simulation with Modelica 3.3: A Cyber-Physical Approach, 2nd edn. Wiley, Hoboken (2014)","edition":"2"},{"key":"561_CR21","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Ho, P.-H., Wong Toi, H.: Hytech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1, (1997)","DOI":"10.1007\/s100090050008"},{"key":"561_CR22","unstructured":"Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain Control Verification Benchmark. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC\u201914, pp. 253\u2013262. ACM, (2014)"},{"key":"561_CR23","first-page":"219","volume":"2","author":"N Lynch","year":"1989","unstructured":"Lynch, N., Tuttle, M.: An introduction to input\/output automata. CWI Q. 2, 219\u2013246 (1989)","journal-title":"CWI Q."},{"issue":"7","key":"561_CR24","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. CAD Integra. Circuits Syst. 13(7), 950\u2013956 (1994)","journal-title":"IEEE Trans. CAD Integra. Circuits Syst."},{"key":"561_CR25","unstructured":"Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Formal Methods and Software Engineering, LNCS, vol. 4260, pp. 606\u2013620. Springer, (2006)"},{"key":"561_CR26","volume-title":"The Definition of Standard ML","author":"R Milner","year":"1990","unstructured":"Milner, R., Tofte, M., Harper, R.: The Definition of Standard ML. MIT Press, Cambridge (1990)"},{"key":"561_CR27","doi-asserted-by":"crossref","unstructured":"Minopoli, S., Frehse, G.: SL2SX Translator: From Simulink to SpaceEx Verification Tool. In: 19th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), (2016)","DOI":"10.1145\/2883817.2883826"},{"key":"561_CR28","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer, (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"561_CR29","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Dragomir, I., Tripakis, S.: Type Inference of Simulink Hierarchical Block Diagrams in Isabelle. In: FORTE, (2017)","DOI":"10.1007\/978-3-319-60225-7_14"},{"key":"561_CR30","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Dragomir, I., Tripakis, S.: The refinement calculus of reactive systems. CoRR, arXiv:1710.03979 (2018)","DOI":"10.1007\/978-3-319-89963-3_12"},{"key":"561_CR31","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Dragomir, I., Tripakis, S.: Mechanically proving determinacy of hierarchical block diagram translations. In: Enea C., Piskac R. (eds.) Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13-15, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11388, pp. 577\u2013600. Springer, Berlin (2019)","DOI":"10.1007\/978-3-030-11245-5_27"},{"key":"561_CR32","unstructured":"Preoteasa, V., Dragomir, I., Tripakis, S.: Mechanically proving determinacy of hierarchical block diagram translations. In: VMCAI 2019 - 20th International Conference on Verification, Model Checking, and Abstract Interpretation, (2019). Extended version available as arXiv report arXiv:1611.01337"},{"key":"561_CR33","unstructured":"Preoteasa, V., Tripakis, S.: Refinement calculus of reactive systems. In: Embedded Software (EMSOFT), 2014 International Conference on, pp. 1\u201310, (Oct 2014)"},{"key":"561_CR34","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Tripakis, S.: Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. In: 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), (2016)","DOI":"10.1145\/2933575.2934503"},{"issue":"1","key":"561_CR35","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10009-015-0367-0","volume":"18","author":"J Quesel","year":"2016","unstructured":"Quesel, J., Mitsch, S., Loos, S.M., Arechiga, N., Platzer, A.: How to model and prove hybrid systems with keymaera: a tutorial on safety. STTT 18(1), 67\u201391 (2016)","journal-title":"STTT"},{"key":"561_CR36","doi-asserted-by":"crossref","unstructured":"Reicherdt, R., Glesner, S.: Formal verification of discrete-time MATLAB\/Simulink models using boogie. In: Giannakopoulou D., Sala\u00fcn G. (eds.) Software Engineering and Formal Methods: 12th International Conference, SEFM 2014, Grenoble, France, September 1\u20135, 2014. Proceedings, pp. 190\u2013204. Springer International Publishing, Cham (2014)","DOI":"10.1007\/978-3-319-10431-7_14"},{"key":"561_CR37","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201908, pp. 159\u2013169, New York, NY, USA, ACM (2008)","DOI":"10.1145\/1379022.1375602"},{"issue":"2","key":"561_CR38","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s11334-011-0145-4","volume":"7","author":"P Roy","year":"2011","unstructured":"Roy, P., Shankar, N.: SimCheck: a contract type system for Simulink. Innov. Syst. Softw. Eng. 7(2), 73\u201383 (2011)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"561_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: Industrial Embedded Systems (SIES), 2010 International Symposium on, pp. 217\u2013220, (July 2010)","DOI":"10.1109\/SIES.2010.5551374"},{"key":"561_CR40","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"AP Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logic. Theor. Comput. Sci. 49, 217\u2013237 (1987)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"561_CR41","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/1985342.1985345","volume":"33","author":"S Tripakis","year":"2011","unstructured":"Tripakis, S., Lickly, B., Henzinger, T.A., Lee, E.A.: A Theory of Synchronous Relational Interfaces. ACM TOPLAS 33(4), 14:1\u201314:41 (2011)","journal-title":"ACM TOPLAS"},{"issue":"4","key":"561_CR42","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":"561_CR43","unstructured":"Tripakis, S., Stergiou, C., Broy, M., Lee, E.A.: Error-completion in interface theories. In: International SPIN Symposium on Model Checking of Software \u2013 SPIN 2013, LNCS, vol. 7976, pp. 358\u2013375. Springer, (2013)"},{"key":"561_CR44","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL, pp. 214\u2013227. ACM, (1999)","DOI":"10.1145\/292540.292560"},{"issue":"12","key":"561_CR45","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."},{"issue":"2","key":"561_CR46","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. Discrete Event Dyn. Syst. 22(2), 223\u2013247 (2012)","journal-title":"Discrete Event Dyn. Syst."},{"key":"561_CR47","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: Embedded Software (EMSOFT), (Sept 2013)","DOI":"10.1109\/EMSOFT.2013.6658587"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00561-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-020-00561-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00561-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,29]],"date-time":"2023-09-29T16:54:35Z","timestamp":1696006475000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-020-00561-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4,7]]},"references-count":47,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["561"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00561-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,4,7]]},"assertion":[{"value":"7 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}