{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:12:29Z","timestamp":1760202749485},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319602240"},{"type":"electronic","value":"9783319602257"}],"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-60225-7_14","type":"book-chapter","created":{"date-parts":[[2017,5,27]],"date-time":"2017-05-27T02:26:37Z","timestamp":1495851997000},"page":"194-209","source":"Crossref","is-referenced-by-count":6,"title":["Type Inference of Simulink Hierarchical Block Diagrams in Isabelle"],"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":[[2017,5,28]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","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 Theoret. Comput. Sci. 109, 43\u201356 (2004)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"issue":"5","key":"14_CR2","doi-asserted-by":"crossref","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 Aspects Comput. 21(5), 451\u2013483 (2009)","journal-title":"Formal Aspects Comput."},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: POPL 1982, pp. 207\u2013212. ACM (1982)","DOI":"10.1145\/582153.582176"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura De","year":"2008","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"issue":"8","key":"14_CR5","doi-asserted-by":"crossref","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. Comm. ACM 18(8), 453\u2013457 (1975)","journal-title":"Comm. ACM"},{"key":"14_CR6","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). doi: 10.1007\/978-3-319-32582-8_3"},{"key":"14_CR7","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver. Technical report, SRI International (2006)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-74464-1_11","volume-title":"Types for Proofs and Programs","author":"F Haftmann","year":"2007","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 160\u2013174. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74464-1_11"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain control verification benchmark. In: HSCC, pp. 253\u2013262. ACM (2014)","DOI":"10.1145\/2562059.2562140"},{"key":"14_CR10","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). doi: 10.1007\/11901433_33"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Minopoli, S., Frehse, G.: SL2SX translator: from Simulink to SpaceEx models. In: HSCC, pp. 93\u201398. ACM (2016)","DOI":"10.1145\/2883817.2883826"},{"key":"14_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). doi: 10.1007\/3-540-55602-8_217"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Dragomir, I., Tripakis, S.: Type inference of Simulink hierarchical block diagrams in Isabelle. CoRR, abs\/1612.05494 (2016)","DOI":"10.1007\/978-3-319-60225-7_14"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Tripakis, S.: Refinement calculus of reactive systems. In: EMSOFT, pp. 2:1\u20132:10. ACM (2014)","DOI":"10.1145\/2656045.2656068"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Tripakis, S.: Towards compositional feedback in non-deterministic and non-input-receptive systems. In: LICS. ACM (2016)","DOI":"10.1145\/2933575.2934503"},{"key":"14_CR17","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). doi: 10.1007\/978-3-319-10431-7_14"},{"issue":"2","key":"14_CR18","doi-asserted-by":"crossref","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":"14_CR19","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. IEEE (2010)","DOI":"10.1109\/SIES.2010.5551374"},{"key":"14_CR20","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual \u2013 Version V8.6, December 2016"},{"issue":"4","key":"14_CR21","doi-asserted-by":"crossref","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 Trans. Program. Lang. Syst. 33(4), 14:1\u201314:41 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"10","key":"14_CR22","doi-asserted-by":"crossref","first-page":"1300","DOI":"10.1109\/TC.2008.81","volume":"57","author":"S Tripakis","year":"2008","unstructured":"Tripakis, S., Pinello, C., Benveniste, A., Sangiovanni-Vincentelli, A., Caspi, P., Natale, M.D.: Implementing synchronous models on loosely time-triggered architectures. IEEE Trans. Comput. 57(10), 1300\u20131314 (2008)","journal-title":"IEEE Trans. Comput."},{"issue":"4","key":"14_CR23","doi-asserted-by":"crossref","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."},{"issue":"12","key":"14_CR24","doi-asserted-by":"crossref","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":"14_CR25","doi-asserted-by":"crossref","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":"14_CR26","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 (2013)","DOI":"10.1109\/EMSOFT.2013.6658587"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-60225-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,25]],"date-time":"2019-09-25T05:19:57Z","timestamp":1569388797000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-60225-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319602240","9783319602257"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-60225-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}