{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T14:04:33Z","timestamp":1766066673424},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319522272"},{"type":"electronic","value":"9783319522289"}],"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-52228-9_4","type":"book-chapter","created":{"date-parts":[[2017,1,9]],"date-time":"2017-01-09T23:23:43Z","timestamp":1484004223000},"page":"65-92","source":"Crossref","is-referenced-by-count":7,"title":["A Two-Way Path Between Formal and Informal Design of Embedded Systems"],"prefix":"10.1007","author":[{"given":"Mingshuai","family":"Chen","sequence":"first","affiliation":[]},{"given":"Anders P.","family":"Ravn","sequence":"additional","affiliation":[]},{"given":"Shuling","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Mengfei","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,1,11]]},"reference":[{"key":"4_CR1","unstructured":"Simulink User\u2019s Guide. http:\/\/www.mathworks.com\/help\/pdf_doc\/simulink\/sl_using.pdf"},{"key":"4_CR2","unstructured":"Stateflow User\u2019s Guide. http:\/\/www.mathworks.com\/help\/pdf_doc\/stateflow\/sf_using.pdf"},{"key":"4_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-1561-6","volume-title":"Introduction to Physical Modeling with Modelica","author":"M Tiller","year":"2001","unstructured":"Tiller, M.: Introduction to Physical Modeling with Modelica. Springer, New York (2001)"},{"key":"4_CR4","unstructured":"SysML V 1.4 Beta Specification (2013). http:\/\/www.omg.org\/spec\/SysML"},{"key":"4_CR5","series-title":"The Springer International Series in Engineering and Computer Science","volume-title":"Modeling and Analysis or Real-Time and Embedded Systems with UML and MARTE: Developing Cyber-Physical Systems","author":"B Selic","year":"2013","unstructured":"Selic, B., Gerard, S.: Modeling and Analysis or Real-Time and Embedded Systems with UML and MARTE: Developing Cyber-Physical Systems. The Springer International Series in Engineering and Computer Science. The MK\/OMG Press, Burlington (2013)"},{"issue":"4","key":"4_CR6","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1109\/MC.2003.1193228","volume":"36","author":"F Balarin","year":"2003","unstructured":"Balarin, F., Watanabe, Y., Hsieh, H., Lavagno, H., Passerone, C., Sangiovanni-Vincentelli, A.L.: Metropolis: an integrated electronic system design environment. IEEE Comput. 36(4), 45\u201352 (2003)","journal-title":"IEEE Comput."},{"issue":"1","key":"4_CR7","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1109\/JPROC.2002.805829","volume":"91","author":"J Eker","year":"2003","unstructured":"Eker, J., Janneck, J., Lee, E.A., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., Xiong, Y.: Taming heterogeneity - the ptolemy approach. Proc. IEEE 91(1), 127\u2013144 (2003)","journal-title":"Proc. IEEE"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Henzinger, T.: The theory of hybrid automata. In: LICS 1996, pp. 278\u2013292, July 1996","DOI":"10.1109\/LICS.1996.561342"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-63141-0_6","volume-title":"CONCUR \u201997: Concurrency Theory","author":"R Alur","year":"1997","unstructured":"Alur, R., Henzinger, T.A.: Modularity for timed and hybrid systems. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 74\u201388. Springer, Berlin (1997). doi: 10.1007\/3-540-63141-0_6"},{"key":"4_CR10","unstructured":"He, J.: From CSP to hybrid systems. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, pp. 171\u2013189. Prentice Hall International (UK) Ltd. (1994)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/BFb0020972","volume-title":"Hybrid Systems III","author":"Z Chaochen","year":"1996","unstructured":"Chaochen, Z., Ji, W., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 511\u2013530. Springer, Berlin (1996). doi: 10.1007\/BFb0020972"},{"issue":"1","key":"4_CR12","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1093\/logcom\/exn070","volume":"20","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309\u2013352 (2010)","journal-title":"J. Log. Comput."},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17164-2_1","volume-title":"Programming Languages and Systems","author":"J Liu","year":"2010","unstructured":"Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1\u201315. Springer, Berlin (2010). doi: 10.1007\/978-3-642-17164-2_1"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Zou, L., Zhan, N., Wang, V., Fr\u00e4nzle, M., Qin, S.: Verifying simulink diagrams via a hybrid hoare logic prover. In: EMSOFT 2013, pp. 1\u201310 (2013)","DOI":"10.1109\/EMSOFT.2013.6658587"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-319-24953-7_33","volume-title":"Automated Technology for Verification and Analysis","author":"L Zou","year":"2015","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 2015. LNCS, vol. 9364, pp. 464\u2013481. Springer, Cham (2015). doi: 10.1007\/978-3-319-24953-7_33"},{"key":"4_CR16","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 (extended version). http:\/\/lcs.ios.ac.cn\/~chenms\/papers\/UTP2016_FULL.pdf","DOI":"10.1007\/978-3-319-52228-9_4"},{"key":"4_CR17","unstructured":"Simulink Design Verifier User\u2019s Guide (2010). http:\/\/www.manualslib.com\/manual\/392930\/Matlab-Simulink-Design-Verifier-1.html#manual"},{"key":"4_CR18","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/2461328.2461345","volume":"2013","author":"Z Han","year":"2013","unstructured":"Han, Z., Mosterman, P.J.: Towards sensitivity analysis of hybrid systems using simulink. HSCC 2013, 95\u2013100 (2013)","journal-title":"HSCC"},{"issue":"4","key":"4_CR19","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. Embedded Comput. Syst. 4(4), 779\u2013818 (2005)","journal-title":"ACM Trans. Embedded Comput. Syst."},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Scaife, N., Sofronis, C., Caspi, P., Tripakis, S., Maraninchi, F.: Defining and translating a \u201csafe\u201d subset of simulink\/stateflow into lustre. In: EMSOFT 2004, pp. 259\u2013268. ACM (2004)","DOI":"10.1145\/1017753.1017795"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/11526841_18","volume-title":"FM 2005: Formal Methods","author":"A Cavalcanti","year":"2005","unstructured":"Cavalcanti, A., Clayton, P., O\u2019Halloran, C.: Control law diagrams in Circus. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 253\u2013268. Springer, Berlin (2005). doi: 10.1007\/11526841_18"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-45648-1_10","volume-title":"ZB 2002:Formal Specification and Development in Z and B","author":"J Woodcock","year":"2002","unstructured":"Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 184\u2013203. Springer, Berlin (2002). doi: 10.1007\/3-540-45648-1_10"},{"key":"4_CR23","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, Berlin (2006). doi: 10.1007\/11901433_33"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Sfyrla, V., Tsiligiannis, G., Safaka, I., Bozga, M., Sifakis, J.: Compositional translation of simulink models into synchronous BIP. In: IEEE Fifth International Symposium on Industrial Embedded Systems, SIES 2010, pp. 217\u2013220. IEEE (2010)","DOI":"10.1109\/SIES.2010.5551374"},{"issue":"10","key":"4_CR25","doi-asserted-by":"crossref","first-page":"1315","DOI":"10.1109\/TC.2008.26","volume":"57","author":"S Bliudze","year":"2008","unstructured":"Bliudze, S., Sifakis, J.: The algebra of connectors - structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315\u20131330 (2008)","journal-title":"IEEE Trans. Comput."},{"issue":"12","key":"4_CR26","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":"4_CR27","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. Discrete Event Dyn. Syst. 22(2), 223\u2013247 (2012)","journal-title":"Discrete Event Dyn. Syst."},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Minpoli, S., Frehse, G.: SL2SX translator: from simulink to SpaceEx verification tool. In: HSCC 2016 (2016)","DOI":"10.1145\/2883817.2883826"},{"issue":"5","key":"4_CR29","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/s00165-009-0108-9","volume":"21","author":"R Chen","year":"2009","unstructured":"Chen, R., 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":"4_CR30","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, Berlin (2011). doi: 10.1007\/978-3-642-24559-6_21"},{"issue":"2","key":"4_CR31","first-page":"73","volume":"7","author":"P Roy","year":"2011","unstructured":"Roy, P., Shankar, N.: Simcheck: a contract type system for simulink. ISSE 7(2), 73\u201383 (2011)","journal-title":"ISSE"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Tripakis, S.: Refinement calculus of reactive systems. In: EMSOFT 2014, pp. 2:1\u20132:10 (2014)","DOI":"10.1145\/2656045.2656068"},{"key":"4_CR33","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":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-39721-9_5","volume-title":"Unifying Theories of Programming and Formal Engineering Methods","author":"N Zhan","year":"2013","unstructured":"Zhan, N., Wang, S., Zhao, H.: Formal modelling, analysis and verification of hybrid systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Unifying Theories of Programming and Formal Engineering Methods. LNCS, vol. 8050, pp. 207\u2013281. Springer, Berlin (2013). doi: 10.1007\/978-3-642-39721-9_5"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-29952-0_13","volume-title":"Theory and Applications of Models of Computation","author":"S Wang","year":"2012","unstructured":"Wang, S., Zhan, N., Guelev, D.: An assume\/guarantee based compositional calculus for hybrid CSP. In: Agrawal, M., Cooper, S.B., Li, A. (eds.) TAMC 2012. LNCS, vol. 7287, pp. 72\u201383. Springer, Berlin (2012). doi: 10.1007\/978-3-642-29952-0_13"},{"key":"4_CR36","unstructured":"Guelev, D., Wang, S., Zhan, N.: Hoare reasoning about HCSP in the duration calculus (2013, submitted)"},{"key":"4_CR37","volume-title":"Unifying Theories of Programming","author":"C Hoare","year":"1998","unstructured":"Hoare, C., He, J.: Unifying Theories of Programming, vol. 14. Prentice Hall, Englewood Cliffs (1998)"},{"key":"4_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-54108-7_14","volume-title":"Verified Software: Theories, Tools, Experiments","author":"L Zou","year":"2014","unstructured":"Zou, L., Lv, J., Wang, S., Zhan, N., Tang, T., Yuan, L., Liu, Y.: Verifying chinese train control system under a combined scenario by theorem proving. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 262\u2013280. Springer, Berlin (2014). doi: 10.1007\/978-3-642-54108-7_14"}],"container-title":["Lecture Notes in Computer Science","Unifying Theories of Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52228-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,17]],"date-time":"2019-09-17T05:56:55Z","timestamp":1568699815000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52228-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522272","9783319522289"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52228-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}