{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T10:56:06Z","timestamp":1742986566418,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030912642"},{"type":"electronic","value":"9783030912659"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91265-9_1","type":"book-chapter","created":{"date-parts":[[2021,11,19]],"date-time":"2021-11-19T11:26:47Z","timestamp":1637321207000},"page":"3-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Translating a Large Subset of Stateflow to\u00a0Hybrid CSP with Code Optimization"],"prefix":"10.1007","author":[{"given":"Panhua","family":"Guo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bohua","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiong","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuling","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenhui","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,11,18]]},"reference":[{"issue":"11","key":"1_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11432-015-5346-2","volume":"58","author":"E Ahmad","year":"2015","unstructured":"Ahmad, E., Dong, Y., Larson, B.R., L\u00fc, J., Tang, T., Zhan, N.: Behavior modeling and verification of movement authority scenario of Chinese train control system using AADL. Sci. China Inf. Sci. 58(11), 1\u201320 (2015)","journal-title":"Sci. China Inf. Sci."},{"key":"1_CR2","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley Series in Computer Science. World Student Series Edition. Addison-Wesley, Boston (1986)"},{"issue":"6","key":"1_CR3","doi-asserted-by":"publisher","first-page":"653","DOI":"10.1007\/s10009-012-0235-0","volume":"14","author":"C Chen","year":"2012","unstructured":"Chen, C., Sun, J., Liu, Y., Dong, J.S., Zheng, M.: Formal modeling and validation of stateflow diagrams. Int. J. Softw. Tools Technol. Transf. 14(6), 653\u2013671 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-662-46681-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PS Duggirala","year":"2015","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68\u201382. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_5"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-41528-4_29","volume-title":"Computer Aided Verification","author":"C Fan","year":"2016","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.) CAV 2016. LNCS, vol. 9779, pp. 531\u2013538. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_29"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Hamon, G.: A denotational semantics for stateflow. In: Proceedings of the 5th ACM International Conference on Embedded Software EMSOFT 2005, Jersey City, NJ, USA, 18\u201322 September 2005, pp. 164\u2013172 (2005)","DOI":"10.1145\/1086228.1086260"},{"issue":"5\u20136","key":"1_CR7","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-007-0049-7","volume":"9","author":"G Hamon","year":"2007","unstructured":"Hamon, G., Rushby, J.M.: An operational semantics for stateflow. Int. J. Softw. Tools Technol. Transf. 9(5\u20136), 447\u2013456 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"1_CR8","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"1_CR9","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D Harel","year":"1996","unstructured":"Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293\u2013333 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1_CR10","unstructured":"Helke, S., Kamm\u00fcller, F.: Formalizing statecharts using hierarchical automata. Archive of Formal Proofs 2010 (2010)"},{"key":"1_CR11","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Hoboken (1985)"},{"issue":"2","key":"1_CR12","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/0304-3975(92)90053-I","volume":"101","author":"J Hooman","year":"1992","unstructured":"Hooman, J., Ramesh, S., de Roever, W.P.: A compositional axiomatization of statecharts. Theor. Comput. Sci. 101(2), 289\u2013335 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR13","unstructured":"Jifeng, H.: From CSP to Hybrid Systems, pp. 171\u2013189. Prentice Hall International (UK) Ltd., Great Britain (1994)"},{"issue":"6","key":"1_CR14","doi-asserted-by":"publisher","first-page":"1324","DOI":"10.1007\/s11390-020-0537-8","volume":"35","author":"Q Lin","year":"2020","unstructured":"Lin, Q., Wang, S., Zhan, B., Gu, B.: Modelling and verification of real-time publish and subscribe protocol using Uppaal and Simulink\/Stateflow. J. Comput. Sci. Technol. 35(6), 1324\u20131342 (2020)","journal-title":"J. Comput. Sci. Technol."},{"key":"1_CR15","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., et al.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1\u201315. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17164-2_1"},{"key":"1_CR16","unstructured":"MathWorks: Simulink\u00ae User\u2019s Guide (2018). http:\/\/www.mathworks.com\/help\/pdf_doc\/simulink\/sl_using.pdf"},{"key":"1_CR17","unstructured":"MathWorks: Stateflow\u00ae User\u2019s Guide (2018). http:\/\/www.mathworks.com\/help\/pdf_doc\/stateflow\/sf_ug.pdf"},{"key":"1_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-3-662-03811-6"},{"key":"1_CR19","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: Proceedings of the Fourth ACM International Conference on Embedded Software, EMSOFT 2004, Pisa, Italy, 27\u201329 September 2004, pp. 259\u2013268 (2004)","DOI":"10.1145\/1017753.1017795"},{"issue":"1","key":"1_CR20","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1109\/JPROC.2002.805818","volume":"91","author":"A Tiwari","year":"2003","unstructured":"Tiwari, A., Shankar, N., Rushby, J.M.: Invisible formal methods for embedded control systems. Proc. IEEE 91(1), 29\u201339 (2003)","journal-title":"Proc. IEEE"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-25423-4_25","volume-title":"Formal Methods and Software Engineering","author":"S Wang","year":"2015","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382\u2013399. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_25"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Yang, Y., Jiang, Y., Gu, M., Sun, J.: Verifying simulink stateflow model: timed automata approach. In: Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, 3\u20137 September 2016, pp. 852\u2013857 (2016)","DOI":"10.1145\/2970276.2970293"},{"key":"1_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47016-0","volume-title":"Formal Verification of Simulink\/Stateflow Diagrams, A Deductive Approach","year":"2017","unstructured":"Zhan, N., Wang, S., Zhao, H. (eds.): Formal Verification of Simulink\/Stateflow Diagrams, A Deductive Approach. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-47016-0"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1007\/978-3-319-06410-9_49","volume-title":"FM 2014: Formal Methods","author":"H Zhao","year":"2014","unstructured":"Zhao, H., Yang, M., Zhan, N., Gu, B., Zou, L., Chen, Y.: Formal verification of a descent guidance control program of a lunar lander. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 733\u2013748. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_49"},{"key":"1_CR25","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, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020972"},{"key":"1_CR26","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). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_33"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Zou, L., Zhan, N., Wang, S., Fr\u00e4nzle, M., Qin, S.: Verifying simulink diagrams via a hybrid hoare logic prover. In: Proceedings of the International Conference on Embedded Software, EMSOFT 2013, Montreal, QC, Canada, 29 September\u20134 October 2013, pp. 9:1\u20139:10 (2013)","DOI":"10.1109\/EMSOFT.2013.6658587"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91265-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,19]],"date-time":"2021-11-19T11:30:35Z","timestamp":1637321435000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91265-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030912642","9783030912659"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91265-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"18 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Beijing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/lcs.ios.ac.cn\/setta2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"39","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.05","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2.53","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}