{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:44:57Z","timestamp":1761324297107,"version":"3.37.3"},"reference-count":74,"publisher":"Association for Computing Machinery (ACM)","issue":"2-3","license":[{"start":{"date-parts":[[2020,7,1]],"date-time":"2020-07-01T00:00:00Z","timestamp":1593561600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,7,1]],"date-time":"2020-07-01T00:00:00Z","timestamp":1593561600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61872145"],"award-info":[{"award-number":["61872145"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"National Key Research and Development Program of China","award":["2018YFB2101300"],"award-info":[{"award-number":["2018YFB2101300"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2020,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The hardware description language Verilog has been standardized and widely used in industry. Multithreaded Discrete Event Simulation Language (MDESL) is a Verilog-like language and it contains a rich variety of interesting features such as the event-driven computation and shared-variable concurrency as well as the realtime feature. In this paper, we present the denotational semantics for MDESL based on UTP. First a discrete time semantic model is proposed to describe the observation-oriented semantics for MDESL. The observations record the change of variables of atomic actions over time. Then the healthy formulae are defined to denote all different behaviors of programs and the semantics of programs is expressed in terms of healthy formulae. In addition, we demonstrate some interesting properties about the MDESL programs expressing as algebraic laws and their proofs are supported by our formalized denotational semantics. Our theoretical approach is complemented by a practical one, we use the theorem proof assistant Coq to formalize the UTP-based semantics for MDESL. The correctness of the algebraic laws is also verified via the mechanical approach in Coq. Our work provides a novel way to verify the correctness of UTP-based semantics forMDESL both in a theoretical approach and in a practical approach. It is also a new attempt for the application of Coq in the mechanized semantics.<\/jats:p>","DOI":"10.1007\/s00165-020-00513-4","type":"journal-article","created":{"date-parts":[[2020,6,17]],"date-time":"2020-06-17T18:04:11Z","timestamp":1592417051000},"page":"275-314","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Theoretical and Practical Approaches to the Denotational Semantics for MDESL based on UTP"],"prefix":"10.1145","volume":"32","author":[{"given":"Feng","family":"Sheng","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zongyuan","family":"Yang","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan P.","family":"Bowen","sequence":"additional","affiliation":[{"name":"London South Bank University, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"issue":"4","key":"e_1_2_1_2_1_2","first-page":"69","article-title":"Applying unifying theories of programming to real-time programming","volume":"10","author":"Arenas AE","year":"2006","journal-title":"Trans SDPS"},{"volume-title":"Certified programming with dependent types","year":"2011","author":"Adam C","key":"e_1_2_1_2_2_2"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Adam C (2013) The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. In: ACM SIGPLAN international conference on functional programming pp 391\u2013402. Springer","DOI":"10.1145\/2544174.2500592"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Blech JO Biha SO (2011) Verification of PLC properties based on formal semantics in coq. In: The 9th international conference software engineering and formal methods pp 58\u201373","DOI":"10.1007\/978-3-642-24690-6_6"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1002\/sec.546"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Butterfield A Cath\u00e1in A (2009) Concurrent models of flash memory device behaviour. In: The 12th Brazilian symposium on formal methods pp 70\u201383 Brazil","DOI":"10.1007\/978-3-642-10452-7_6"},{"key":"e_1_2_1_2_7_2","unstructured":"Bertot Y Cast\u00e9ran P (2013) Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Springer Science & Business Media"},{"key":"e_1_2_1_2_8_2","unstructured":"Bowen JP He J Xu Q (2000) An animatable operational semantics of the Verilog hardware description language. In: The 3rd IEEE international conference on formal engineering methods pp 199\u2013207. IEEE"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Bidmeshki M-M Makris Y (2015) Vericoq: a verilog-to-coq converter for proof-carrying hardware automation. In: 2015 IEEE international symposium on circuits and systems pp 29\u201332","DOI":"10.1109\/ISCAS.2015.7168562"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Butterfield A Mjeda A Noll J (2016) UTP semantics for shared-state concurrent context-sensitive process models. In: The 10th international symposium on theoretical aspects of software engineering pp 93\u2013100","DOI":"10.1109\/TASE.2016.22"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2237796.2237814"},{"key":"e_1_2_1_2_13_2","unstructured":"Butterfield A (2008) Unifying theories of programming. Second international symposium UTP 2008 Dublin Ireland September 8\u201310 2008. Revised selected papers volume 5713 of lecture notes in computer science. Springer"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Butterfield A (2016) UTPCalc\u2014a calculator for UTP predicates. In: The 6th international symposium on unifying theories of programming pp 197\u2013216","DOI":"10.1007\/978-3-319-52228-9_10"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Butterfield A (2017) UTCP: compositional semantics for shared-variable concurrency. In: The 20th Brazilian symposium on formal methods: foundations and applications pp 253\u2013270","DOI":"10.1007\/978-3-319-70848-5_16"},{"key":"e_1_2_1_2_16_2","unstructured":"Bowen JP Zhu H (2016) Unifying theories of programming. 6th international symposium UTP 2016 Reykjavik Iceland June 4\u20135 2016. Revised selected papers volume 10134 of lecture notes in computer science. Springer"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Chatzikyriakidis S Luo Z (2016) Proof assistants for natural language semantics. In: The 9th international conference on logical aspects of computational linguistics pp 85\u201398","DOI":"10.1007\/978-3-662-53826-5_6"},{"issue":"24","key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3110268","article-title":"Kami: a platform for high-level parametric hardware specification and its modular verification","volume":"1","author":"Choi J","year":"2017","journal-title":"Proc ACM Program Lang"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0253-4"},{"key":"e_1_2_1_2_20_2","unstructured":"Dimitrov J (2001) Operational semantics for Verilog. In: The 8th Asia-Pacific software engineering conference pp 161\u2013168. IEEE"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Dunne S Stoddart B (2006) Unifying Theories of Programming. First international symposium UTP 2006 Walworth Castle County Durham UK February 5\u20137 2006 revised selected papers. volume 4010 of lecture notes in computer science. Springer","DOI":"10.1007\/11768173"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Foster S Baxter J Cavalcanti A Woodcock J Zeyda F (2019) Unifying semantic foundations for automated verification tools in Isabelle\/UTP. CoRR arXiv:1905.05500","DOI":"10.1016\/j.scico.2020.102510"},{"key":"e_1_2_1_2_23_2","unstructured":"Foster S Zeyda F Nemouchi Y Ribeiro P Wolff B (2019) Isabelle\/UTP: mechanised theory engineering for unifying theories of programming. Archive of Formal Proofs 2019"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Foster S Zeyda F Woodcock J (2014) Isabelle\/UTP: a mechanised theory engineering framework. In: International Symposium on unifying theories of programming pp 21\u201341. Springer","DOI":"10.1007\/978-3-319-14806-9_2"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Gordon M (1995) The semantic challenge of verilog hdl. In: Proceedings of tenth annual IEEE symposium on logic in computer science pp 136\u2013145","DOI":"10.1109\/LICS.1995.523251"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/45.1.27"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211086"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"He J (2003) An algebraic approach to the Verilog programming. In: Formal methods at the crossroads. From Panacea to Foundational Support pp 65\u201380. Springer","DOI":"10.1007\/978-3-540-40007-3_5"},{"key":"e_1_2_1_2_29_2","unstructured":"Hoare CAR He J (1998) Unifying theories of programming. volume 14. Prentice Hall Englewood Cliffs"},{"issue":"3","key":"e_1_2_1_2_30_2","first-page":"205","article-title":"Linking theories in probabilistic programming","volume":"119","author":"He J","year":"1999","journal-title":"Inf Sci"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01191809"},{"key":"e_1_2_1_2_32_2","unstructured":"Huet G Kahn G Paulin-Mohring C (2004) The coq proof assistant a tutorial. Rapport Technique 178"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.034"},{"key":"e_1_2_1_2_34_2","first-page":"1","volume-title":"The 25th international conference on concurrency theory","author":"Hoare T","year":"2014"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_2_1_2_36_2","unstructured":"He J Xu Q (2000) An operational semantics of a simulator algorithm. In The proceedings of the PDPTA pp 26\u201329"},{"issue":"1","key":"e_1_2_1_2_37_2","first-page":"84","article-title":"Advanced features of duration calculus and their applications in sequential hybrid programs","volume":"15","author":"He J","year":"2003","journal-title":"Formal Asp Comput"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"He J Zhu H (2000) Formalising Verilog. In The 7th IEEE international conference on electronics circuits and systems vol 1 pp 412\u2013415. IEEE","DOI":"10.1109\/ICECS.2000.911568"},{"key":"e_1_2_1_2_39_2","unstructured":"IEEE (2001) IEEE standard hardware description language based on the Verilog hardware description language. IEEE Standard 1364-2001"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Andronick J Chetali B Ly O (2003) Using coq to verify java card tm applet isolation properties. In: International conference on theorem proving in higher order logics pp 335\u2013351. Springer","DOI":"10.1007\/10930755_22"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Krebbers R Leroy X Wiedijk F (2014) Formal C semantics: Compcert and the C standard. In: The 5th international conference on interactive theorem proving pp 543\u2013548","DOI":"10.1007\/978-3-319-08970-6_36"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Leroy X (2006) Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages pp 42\u201354","DOI":"10.1145\/1111320.1111042"},{"key":"e_1_2_1_2_43_2","unstructured":"Li Y He J (2000) Formalising verilog: Operational semantics and bisimulation. Technical report"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2902"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Meredith P Katelman M Meseguer J Ro\u015fu G (2010) A formal executable semantics of Verilog. In: The 8th IEEE\/ACM international conference on formal methods and models for codesign pp 179\u2013188. IEEE","DOI":"10.1109\/MEMCOD.2010.5558634"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Manna Z Pnueli A (1981) Verification of concurrent programs. Part I. The temporal framework. Technical report. Department of Computer Science Stanford University California","DOI":"10.21236\/ADA106750"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Manna Z Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer Science & Business Media","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Manna Z Pnueli A (1995) Temporal verification of reactive systems: safety. Springer Science & Business Media","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Naumann D (2014) Unifying theories of programming\u20145th international symposium UTP 2014 Singapore May 13 2014. Revised selected papers. volume 8963 of lecture notes in computer science. Springer","DOI":"10.1007\/978-3-319-14806-9"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0052-5"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0044-5"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Owre S Rushby JM Shankar N (1992) PVS: a prototype verification system. In 11th international conference on automated deduction pp 748\u2013752 USA","DOI":"10.1007\/3-540-55602-8_217"},{"key":"e_1_2_1_2_53_2","unstructured":"Palmskog K Gligoric M Pe\u00f1a L Moore B Rosu G (2018) Verification of casper in the coq proof assistant. Technical report"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Poernomo I Terrell J (2010) Correct-by-construction model transformations from partially ordered specifications in coq. In The 12th international conference on formal engineering methods pp 56\u201373","DOI":"10.1007\/978-3-642-16901-4_6"},{"key":"e_1_2_1_2_55_2","unstructured":"Qin S (2010) Unifying theories of programming\u2014third international symposium UTP 2010 Shanghai China November 15\u201316 2010. Proceedings. volume 6445 of Lecture notes in computer science. Springer"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Sieczkowski F Bizjak A Birkedal L (2015) ModuRes: a coq library for modular reasoning about concurrent higher-order imperative programming languages. In: The 6th international conference on interactive theorem proving pp 375\u2013390","DOI":"10.1007\/978-3-319-22102-1_25"},{"issue":"11","key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","first-page":"1773","DOI":"10.1631\/FITEE.1601196","article-title":"Mechanized semantics and refinement of UML-Statecharts","volume":"18","author":"Sheng F","year":"2017","journal-title":"Front Inf Technol Electron Eng"},{"key":"e_1_2_1_2_58_2","unstructured":"Sheng F (2018) Formalization of Verilog. https:\/\/github.com\/shengfeng\/formalization_of_MDESL\/blob\/master\/denotational_semantics.v"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Slind K Norrish M (2008) A brief overview of HOL4. In: The 21st international conference on theorem proving in higher order logics pp 28\u201332","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0453-7"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/3295699"},{"key":"e_1_2_1_2_62_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_2_63_2","unstructured":"Tang X Woodcock J (2004) Towards mobile processes in unifying theories. In: The 2nd international conference on software engineering and formal methods pp 44\u201353 Beijing"},{"key":"e_1_2_1_2_64_2","unstructured":"Woodcock J Cavalcanti A (2001) The steam boiler in a unified theory of Z and CSP. In The 8th Asia-Pacific software engineering conference pp 291\u2013298 China"},{"key":"e_1_2_1_2_65_2","doi-asserted-by":"crossref","unstructured":"Woodcock J Cavalcanti A (2002) The semantics of circus. In The 2nd International Conference of B and Z Users pp 84\u2013203 France","DOI":"10.1007\/3-540-45648-1_10"},{"key":"e_1_2_1_2_66_2","unstructured":"Wolff B Gaudel M-C Feliachi A (2012) Unifying theories of programming 4th international symposium UTP 2012 Paris France August 27\u201328 2012. Revised Selected Papers. volume 7681 of lecture notes in computer science. Springer"},{"key":"e_1_2_1_2_67_2","unstructured":"Wan H Song X Gu M (2012) Parameterized specification and verification of PLC systems in coq. In The 4th IEEE international symposium on theoretical aspects of software engineering pp 179\u2013182"},{"key":"e_1_2_1_2_68_2","doi-asserted-by":"crossref","unstructured":"Wu X Zhu H Wu X (2014) Observation-oriented semantics for calculus of wireless systems. In The 5th international symposium on unifying theories of programming pp 105\u2013124 Singapore","DOI":"10.1007\/978-3-319-14806-9_6"},{"key":"e_1_2_1_2_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0467-1"},{"key":"e_1_2_1_2_70_2","unstructured":"Zhu H He J (2000) A DC-based semantics for Verilog. In Proceedings of the ICS pp 421\u2013432. Citeseer"},{"key":"e_1_2_1_2_71_2","unstructured":"Zhu H He J (2000) A semantics of Verilog using Duration Calculus. In Proceedings of international conference on software: theory and practice pp 421\u2013432"},{"key":"e_1_2_1_2_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-008-0069-9"},{"key":"e_1_2_1_2_73_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90122-X"},{"key":"e_1_2_1_2_74_2","unstructured":"Zhu H (2005) Linking the semantics of a multithreaded discrete event simulation language. PhD thesis London South Bank University"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00513-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-020-00513-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00513-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-020-00513-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,7]],"date-time":"2024-08-07T21:05:45Z","timestamp":1723064745000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-020-00513-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7]]},"references-count":74,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2020,7]]}},"alternative-id":["10.1007\/s00165-020-00513-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-020-00513-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2020,7]]},"assertion":[{"value":"13 July 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 April 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 June 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}