{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:03:13Z","timestamp":1762459393567},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319325811"},{"type":"electronic","value":"9783319325828"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-32582-8_3","type":"book-chapter","created":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T06:04:23Z","timestamp":1460009063000},"page":"38-56","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Compositional Semantics and Analysis of Hierarchical Block Diagrams"],"prefix":"10.1007","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":[[2016,4,8]]},"reference":[{"key":"3_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)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"3_CR2","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)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-24559-6_21","volume-title":"Formal Methods and Software Engineering","author":"P Bostr\u00f6m","year":"2011","unstructured":"Bostr\u00f6m, P.: Contract-based verification of Simulink models. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 291\u2013306. Springer, Heidelberg (2011)"},{"issue":"5","key":"3_CR4","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 Aspects Comput. 21(5), 451\u2013483 (2009)","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"3_CR5","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1111\/j.1934-6093.2006.tb00275.x","volume":"8","author":"JA Cook","year":"2006","unstructured":"Cook, J.A., Sun, J., Buckland, J.H., Kolmanovsky, I.V., Peng, H., Grizzle, J.W.: Automotive powertrain control - A survey. Asian J. Control 8(3), 237\u2013260 (2006)","journal-title":"Asian J. Control"},{"issue":"8","key":"3_CR6","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. Comm. ACM 18(8), 453\u2013457 (1975)","journal-title":"Comm. ACM"},{"key":"3_CR7","unstructured":"Dragomir, I., Preoteasa, V., Tripakis, S.: Translating hierarchical block diagrams into composite predicate transformers. CoRR, abs\/1510.04873 (2015)"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Frehse, G., Han, Z., Krogh, B.: Assume-guarantee reasoning for hybrid I\/O-automata by over-approximation of continuous interaction. In: CDC, pp. 479\u2013484 (2004)","DOI":"10.1109\/CDC.2004.1428676"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Garavel, H., Sighireanu, M.: A graphical parallel composition operator for process algebras. In: FORTE XII. IFIP Conference Proceedings, vol. 156, pp. 185\u2013202. Kluwer (1999)","DOI":"10.1007\/978-0-387-35578-8_11"},{"key":"3_CR10","unstructured":"Jin, X., Deshmukh, J., Kapinski, J., Ueda, K., Butts, K.: Benchmarks for model transformations and conformance checking. In: ARCH (2014)"},{"key":"3_CR11","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"},{"issue":"9","key":"3_CR12","doi-asserted-by":"publisher","first-page":"1235","DOI":"10.1109\/PROC.1987.13876","volume":"75","author":"E Lee","year":"1987","unstructured":"Lee, E., Messerschmitt, D.: Synchronous data flow. Proc. IEEE 75(9), 1235\u20131245 (1987)","journal-title":"Proc. IEEE"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Lublinerman, R., Szegedy, C., Tripakis, S.: Modular code generation from synchronous block diagrams - modularity vs. code size. In: POPL, pp. 78\u201389. ACM, January 2009","DOI":"10.1145\/1594834.1480893"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Lublinerman, R., Tripakis, S.: Modularity vs. reusability: code generation from synchronous block diagrams. In: DATE, pp. 1504\u20131509. ACM, March 2008","DOI":"10.1109\/DATE.2008.4484887"},{"issue":"1","key":"3_CR15","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"N Lynch","year":"2003","unstructured":"Lynch, N., Segala, R., Vaandrager, F.: Hybrid I\/O automata. Inf. Comput. 185(1), 105\u2013157 (2003)","journal-title":"Inf. Comput."},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Manamcheri, K., Mitra, S., Bak, S., Caccamo, M.: A step towards verification and synthesis from Simulink\/Stateflow models. In: HSCC, pp. 317\u2013318. ACM (2011)","DOI":"10.1145\/1967701.1967749"},{"key":"3_CR17","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., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606\u2013620. Springer, Heidelberg (2006)"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Minopoli, S., Frehse, G.: SL2SX Translator: from Simulink to SpaceEx verification tool. In: HSCC (2016)","DOI":"10.1145\/2883817.2883826"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Tripakis, S.: Refinement calculus of reactive systems. In: EMSOFT, pp. 1\u201310, October 2014","DOI":"10.1145\/2656045.2656068"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Tripakis, S.: Towards compositional feedback in non-deterministic and non-input-receptive systems. CoRR, abs\/1510.06379 (2015)","DOI":"10.1145\/2933575.2934503"},{"issue":"2","key":"3_CR21","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. Innovations Syst. Softw. Eng. 7(2), 73\u201383 (2011)","journal-title":"Innovations Syst. Softw. Eng."},{"key":"3_CR22","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"},{"issue":"4","key":"3_CR23","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 Trans. Program. Lang. Syst. 33(4), 14:1\u201314:41 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"3_CR24","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."},{"issue":"12","key":"3_CR25","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":"3_CR26","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":"3_CR27","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","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-32582-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T21:17:30Z","timestamp":1584998250000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-32582-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319325811","9783319325828"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-32582-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"8 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}