{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,28]],"date-time":"2026-09-28T21:41:45Z","timestamp":1790631705434,"version":"4.1.0"},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,1,31]],"date-time":"2023-01-31T00:00:00Z","timestamp":1675123200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["61625206, 62192732, 62032024, 61972385, and 61732001"],"award-info":[{"award-number":["61625206, 62192732, 62032024, 61972385, and 61732001"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Inria\u2019s joint research project CONVEX"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2023,1,31]]},"abstract":"<jats:p>\n            Model-based design has become the predominant approach to the design of hybrid and cyber-physical systems (CPSs). It advocates the use of mathematically founded models to capture heterogeneous digital and analog behaviours from domain-specific formalisms, allowing all engineering tasks of verification, code synthesis, and validation to be performed within a single semantic body. Guaranteeing the consistency among the different views and heterogeneous models of a system at different levels of abstraction, however, poses significant challenges. To address these issues, Hoare and He\u2019s Unifying Theories of Programming (UTP) proposes a calculus to capture domain-specific programming and modelling paradigms into a unified semantic framework. Our goal is to extend UTP to form a semantic foundation for CPS design.\n            <jats:italic>Higher-order UTP<\/jats:italic>\n            (HUTP) is a conservative extension to Hoare and He\u2019s theory that supports the specification of discrete, real-time, and continuous dynamics, concurrency and communication, and higher-order quantification. Within HUTP, we define a calculus of\n            <jats:italic>normal hybrid designs<\/jats:italic>\n            to model, analyse, compose, refine, and verify heterogeneous hybrid system models. In addition, we define respective formal semantics for Hybrid Communicating Sequential Processes and Simulink using HUTP.\n          <\/jats:p>","DOI":"10.1145\/3517192","type":"journal-article","created":{"date-parts":[[2022,4,23]],"date-time":"2022-04-23T11:22:32Z","timestamp":1650712952000},"page":"1-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Semantics Foundation for Cyber-physical Systems Using Higher-order UTP"],"prefix":"10.1145","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4236-9992","authenticated-orcid":false,"given":"Xiong","family":"Xu","sequence":"first","affiliation":[{"name":"SKLCS, Institute of Software, Chinese Academy of Sciences, China and Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shuling","family":"Wang","sequence":"additional","affiliation":[{"name":"SKLCS, Institute of Software, Chinese Academy of Sciences, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bohua","family":"Zhan","sequence":"additional","affiliation":[{"name":"SKLCS, Institute of Software &amp; UCAS, Chinese Academy of Sciences, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[{"name":"State Key Lab. of Computer Science and Science &amp; Technology on Integrated Information Science Lab., Institute of Software &amp; UCAS, Chinese Academy of Sciences, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,2,13]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30885-7_13"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57318-6_30"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45352-0_17"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1561\/1000000053"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.04.019"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461348"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2009.57"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-44896-1_5"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.02.001"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3448270"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31038-7_7"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-43520-2_7"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.09.017"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2018.02.017"},{"key":"e_1_3_3_18_2","series-title":"Proceedings of the 6th International Symposium on Unifying Theories of Programming (UTP\u201916)","first-page":"44","volume":"10134","author":"Foster S.","year":"2016","unstructured":"S. Foster, B. Thiele, A. Cavalcanti, and J. Woodcock. 2016. Towards a UTP semantics for Modelica. In Proceedings of the 6th International Symposium on Unifying Theories of Programming (UTP\u201916)(Lecture Notes in Computer Science, Vol. 10134). Springer, Reykjavik, Iceland, 44\u201364."},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0504-8"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.41"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2009.07.002"},{"key":"e_1_3_3_23_2","first-page":"171","volume-title":"A Classical Mind: Essays in Honour of C. A. R. Hoare","author":"He J.","year":"1994","unstructured":"J. He. 1994. From CSP to hybrid systems. In A Classical Mind: Essays in Honour of C. A. R. Hoare. Prentice Hall International, UK, 171\u2013189."},{"key":"e_1_3_3_24_2","series-title":"Lecture Notes in Computer Science","first-page":"124","volume-title":"Concurrency, Security, and Puzzles\u2014Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday","author":"He J.","year":"2017","unstructured":"J. He and Q. Li. 2017. A hybrid relational modelling language. In Concurrency, Security, and Puzzles\u2014Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday. Number 10160 in Lecture Notes in Computer Science. Springer, 124\u2013143."},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.05.022"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8596-5"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45351-2_24"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_3_29_2","volume-title":"Unifying Theories of Programming","author":"Hoare C. A. R.","year":"1998","unstructured":"C. A. R. Hoare and J. He. 1998. Unifying Theories of Programming. Prentice Hall, Englewood Cliffs, NJ."},{"key":"e_1_3_3_30_2","series-title":"Proceedings of the 4th International School on Advanced Functional Programming (AFP\u201902)","first-page":"159","volume":"2638","author":"Hudak P.","year":"2002","unstructured":"P. Hudak, A. Courtney, H. Nilsson, and J. Peterson. 2002. Arrows, robots, and functional reactive programming. In Proceedings of the 4th International School on Advanced Functional Programming (AFP\u201902)(Lecture Notes in Computer Science, Vol. 2638). Springer, Oxford, UK, 159\u2013187."},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-53733-7_8"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_1"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934555"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2017.16"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_22"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00067-1"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428202"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/SOSCYPS.2016.7580000"},{"key":"e_1_3_3_39_2","series-title":"Proceedings of the REX Workshop on Real-Time: Theory in Practice","first-page":"447","volume":"600","author":"Maler O.","year":"1991","unstructured":"O. Maler, Z. Manna, and A. Pnueli. 1991. From timed to hybrid systems. In Proceedings of the REX Workshop on Real-Time: Theory in Practice(Lecture Notes in Computer Science, Vol. 600). Springer, 447\u2013484."},{"key":"e_1_3_3_40_2","volume-title":"Simulink User\u2019s Guide","year":"2013","unstructured":"MathWorks. 2013. Simulink User\u2019s Guide. Retrieved from http:\/\/www.mathworks.com\/help\/pdf_doc\/simulink\/sl_using.pdf."},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.5555\/1140956.1709621"},{"key":"e_1_3_3_42_2","volume-title":"Modeling and Analyzing Hybrid Systems with Sphinx","author":"Mitsch S.","year":"2013","unstructured":"S. Mitsch. 2013. Modeling and Analyzing Hybrid Systems with Sphinx. Carnegie Mellon University\/Johannes Kepler University."},{"key":"e_1_3_3_43_2","volume-title":"Modelica\u2014A Unified Object-Oriented Language for Systems Modeling (Language Specification) (version 3.3 revision, 1st ed.)","year":"2014","unstructured":"Modelica. 2014. Modelica\u2014A Unified Object-Oriented Language for Systems Modeling (Language Specification) (version 3.3 revision, 1st ed.). Modelica Association."},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/11783596_20"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_28"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.5555\/3288063.3288082"},{"key":"e_1_3_3_47_2","volume-title":"Yale FRP User\u2019s Manual","author":"Peterson J.","year":"2001","unstructured":"J. Peterson, Z. Wan, P. Hudak, and H. Nilsson. 2001. Yale FRP User\u2019s Manual. Department of Computer Science, Yale University. Retrieved from http:\/\/www.haskell.org\/frp\/manual.html."},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/2817824"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0"},{"key":"e_1_3_3_52_2","first-page":"109","volume-title":"Proceedings of the 17th Annual Symposium on Foundations of Computer Science (FOCS\u201976)","author":"Pratt V. R.","year":"1976","unstructured":"V. R. Pratt. 1976. Semantical considerations on Floyd-Hoare logic. In Proceedings of the 17th Annual Symposium on Foundations of Computer Science (FOCS\u201976). IEEE Computer Society, 109\u2013121."},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2351672"},{"key":"e_1_3_3_54_2","series-title":"Proceedings of the 5th International Workshop on Hybrid Systems (Hybrid Systems V)","first-page":"304","volume":"1567","author":"R\u00f6nkk\u00f6 M.","year":"1997","unstructured":"M. R\u00f6nkk\u00f6 and A. P. Ravn. 1997. Action systems with continuous behaviour. In Proceedings of the 5th International Workshop on Hybrid Systems (Hybrid Systems V)(Lecture Notes in Computer Science, Vol. 1567). Springer, 304\u2013323."},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.5555\/550448"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737166.2737167"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3322484"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"issue":"8","key":"e_1_3_3_59_2","first-page":"1111","article-title":"Modelling and verifying communication failure of hybrid systems in HCSP","volume":"60","author":"Wang S.","year":"2017","unstructured":"S. Wang, F. Nielson, H. R. Nielson, and N. Zhan. 2017. Modelling and verifying communication failure of hybrid systems in HCSP. Comput. J. 60, 8 (Aug.2017), 1111\u20131130.","journal-title":"Comput. J."},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0421-7"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360002"},{"key":"e_1_3_3_62_2","series-title":"Proceedings of the 4th International Symposium on Unifying Theories of Programming (UTP\u201912)","first-page":"204","volume":"7681","author":"Zeyda F.","year":"2012","unstructured":"F. Zeyda and A. Cavalcanti. 2012. Higher-Order UTP for a theory of methods. In Proceedings of the 4th International Symposium on Unifying Theories of Programming (UTP\u201912)(Lecture Notes in Computer Science, Vol. 7681). Springer, Paris, France, 204\u2013223."},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_42"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS52030.2021.00051"},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47016-0"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_49"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90122-X"},{"key":"e_1_3_3_68_2","series-title":"Proceedings of the DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems, Hybrid Systems III: Verification and Control","first-page":"511","volume":"1066","author":"Zhou C.","year":"1995","unstructured":"C. Zhou, J. Wang, and A. P. Ravn. 1995. A formal description of hybrid systems. In Proceedings of the DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems, Hybrid Systems III: Verification and Control(Lecture Notes in Computer Science, Vol. 1066). Springer, 511\u2013530."},{"key":"e_1_3_3_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_33"},{"key":"e_1_3_3_70_2","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2013.6658587"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3517192","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3517192","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:31:29Z","timestamp":1750188689000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3517192"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,31]]},"references-count":69,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1,31]]}},"alternative-id":["10.1145\/3517192"],"URL":"https:\/\/doi.org\/10.1145\/3517192","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,31]]},"assertion":[{"value":"2021-03-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-02-07","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-02-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}