{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T02:37:55Z","timestamp":1781836675963,"version":"3.54.5"},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T00:00:00Z","timestamp":1564358400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Key Research and Development Program of China","award":["2018YFB2101300"],"award-info":[{"award-number":["2018YFB2101300"]}]},{"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"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2019,7,31]]},"abstract":"<jats:p>Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. It contains interesting features such as event-driven computation and shared-variable concurrency. This article considers how the algebraic semantics links with the operational semantics for MDESL. Our approach is from both the theoretical and practical aspects. The link is proceeded by deriving the operational semantics from the algebraic semantics. First, we present the algebraic semantics for MDESL. We introduce the concept of head normal form. Second, we present the strategy of deriving operational semantics from algebraic semantics. We also investigate the soundness and completeness of the derived operational semantics with respect to the derivation strategy. Our theoretical approach is complemented by a practical one, and we use the theorem proof assistant Coq to formalize the algebraic laws and the derived operational semantics. Meanwhile, the soundness and completeness of the derived operational semantics is also verified via the mechanical approach in Coq. Our approach is a novel way to formalize and verify the correctness and equivalence of different semantics for MDESL in both a theoretical approach and a practical approach.<\/jats:p>","DOI":"10.1145\/3295699","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Theoretical and Practical Aspects of Linking Operational and Algebraic Semantics for MDESL"],"prefix":"10.1145","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0054-1398","authenticated-orcid":false,"given":"Feng","family":"Sheng","sequence":"first","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zongyuan","family":"Yang","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jonathan P.","family":"Bowen","sequence":"additional","affiliation":[{"name":"London South Bank University, London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/645395.757559"},{"key":"e_1_2_1_2_1","volume-title":"Interactive Theorem Proving and Program Development: Coq Art: The Calculus of Inductive Constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2004. Interactive Theorem Proving and Program Development: Coq Art: The Calculus of Inductive Constructions . Springer-Verlag . Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development: Coq Art: The Calculus of Inductive Constructions. Springer-Verlag."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2015.7168562"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2075679.2075687"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2237796.2237814"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/857176.857387"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1002\/sec.546"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0056"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_6"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0253-4"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_2_1_13_1","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","unstructured":"Adam Chlipala . 2013b. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant . MIT Press . Adam Chlipala. 2013b. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110268"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25423-4_26"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 14th International Conference of Rewriting Techniques and Applications (RTA\u201903)","author":"Clavel Manuel","unstructured":"Manuel Clavel , Francisco Dur\u00e1n , Steven Eker , Patrick Lincoln , Narciso Mart\u00ed-Oliet , Jos\u00e9 Meseguer , and Carolyn L. Talcott . 2003. The Maude 2.0 system . In Proceedings of the 14th International Conference of Rewriting Techniques and Applications (RTA\u201903) . 76--87. Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and Carolyn L. Talcott. 2003. The Maude 2.0 system. In Proceedings of the 14th International Conference of Rewriting Techniques and Applications (RTA\u201903). 76--87."},{"key":"e_1_2_1_17_1","volume-title":"de Vink","author":"de Bakker Jacobus W.","year":"1996","unstructured":"Jacobus W. de Bakker and Erik P . de Vink . 1996 . Control Flow Semantics. MIT Press . Jacobus W. de Bakker and Erik P. de Vink. 1996. Control Flow Semantics. MIT Press."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/872020.872385"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/788017.788782"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/45.1.27"},{"key":"e_1_2_1_21_1","volume-title":"Formal Methods at the Crossroads: From Panacea to Foundational Support","author":"Jifeng He.","unstructured":"Jifeng He. 2003. An algebraic approach to the VERILOG programming . In Formal Methods at the Crossroads: From Panacea to Foundational Support . Springer , 65--80. Jifeng He. 2003. An algebraic approach to the VERILOG programming. In Formal Methods at the Crossroads: From Panacea to Foundational Support. Springer, 65--80."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90219-Y"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0255(99)00015-8"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.10.009"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.034"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_2_1_27_1","volume-title":"Formalising Verilog. In Proceedings of the 7th IEEE International Conference on Electronics, Circuits and Systems (ICECS\u201900)","author":"He Jifeng","year":"2000","unstructured":"Jifeng He and Huibiao Zhu . 2000 . Formalising Verilog. In Proceedings of the 7th IEEE International Conference on Electronics, Circuits and Systems (ICECS\u201900) . Jifeng He and Huibiao Zhu. 2000. Formalising Verilog. In Proceedings of the 7th IEEE International Conference on Electronics, Circuits and Systems (ICECS\u201900)."},{"key":"e_1_2_1_28_1","volume-title":"Unifying Theories of Programming","author":"Hoare C. A. R.","unstructured":"C. A. R. Hoare and Jifeng He. 1998. Unifying Theories of Programming . Prentice Hall International Series in Computer Science. C. A. R. Hoare and Jifeng He. 1998. Unifying Theories of Programming. Prentice Hall International Series in Computer Science."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01191809"},{"key":"e_1_2_1_30_1","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","unstructured":"C. A. R. Hoare . 1985. Communicating Sequential Processes . Prentice-Hall . C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice-Hall."},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare Jifeng He and Augusto Sampaio. 2000. Algebraic derivation of an operational semantics. In Proof Language and Interaction Essays in Honour of Robin Milner. 77--98. C. A. R. Hoare Jifeng He and Augusto Sampaio. 2000. Algebraic derivation of an operational semantics. In Proof Language and Interaction Essays in Honour of Robin Milner. 77--98.","DOI":"10.7551\/mitpress\/5641.003.0008"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0249-0"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 14th International Conference of Relational and Algebraic Methods in Computer Science (RAMiCS\u201914)","author":"Hoare Tony","unstructured":"Tony Hoare , Stephan van Staden , Bernhard M\u00f6ller , Georg Struth , Jules Villard , Huibiao Zhu , and Peter W . O\u2019Hearn. 2014. Developments in concurrent Kleene algebra . In Proceedings of the 14th International Conference of Relational and Algebraic Methods in Computer Science (RAMiCS\u201914) . 1--18. Tony Hoare, Stephan van Staden, Bernhard M\u00f6ller, Georg Struth, Jules Villard, Huibiao Zhu, and Peter W. O\u2019Hearn. 2014. Developments in concurrent Kleene algebra. In Proceedings of the 14th International Conference of Relational and Algebraic Methods in Computer Science (RAMiCS\u201914). 1--18."},{"key":"e_1_2_1_35_1","volume-title":"The Coq proof assistant a tutorial. Rapport Technique 178","author":"Huet G\u00e9rard","year":"2004","unstructured":"G\u00e9rard Huet , Gilles Kahn , and Christine Paulin-Mohring . 2004. The Coq proof assistant a tutorial. Rapport Technique 178 ( 2004 ). G\u00e9rard Huet, Gilles Kahn, and Christine Paulin-Mohring. 2004. The Coq proof assistant a tutorial. Rapport Technique 178 (2004)."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_36"},{"key":"e_1_2_1_37_1","unstructured":"Xavier Leroy. 2010. Mechanized semantics - with applications to program proof and compiler verification. In Logics and Languages for Reliability and Security. 195--224. Xavier Leroy. 2010. Mechanized semantics - with applications to program proof and compiler verification. In Logics and Languages for Reliability and Security. 195--224."},{"key":"e_1_2_1_38_1","volume-title":"Formalising Verilog: Operational Semantics and Bisimulation. Technical Report.","author":"Li Yongjian","year":"2000","unstructured":"Yongjian Li and Jifeng He . 2000 . Formalising Verilog: Operational Semantics and Bisimulation. Technical Report. Yongjian Li and Jifeng He. 2000. Formalising Verilog: Operational Semantics and Bisimulation. Technical Report."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2902"},{"key":"e_1_2_1_40_1","volume-title":"Realtime Systems","author":"Nissanke Nimal","unstructured":"Nimal Nissanke . 1997. Realtime Systems . Prentice Hall series in computer science, Vol. 1 . Prentice Hall . Nimal Nissanke. 1997. Realtime Systems. Prentice Hall series in computer science, Vol. 1. Prentice Hall."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0052-5"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0044-5"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/648230.752639"},{"key":"e_1_2_1_44_1","volume-title":"A structural approach to operational semantics. J. Log. Algebr. Program. 60-61","author":"Plotkin Gordon D.","year":"2004","unstructured":"Gordon D. Plotkin . 2004. A structural approach to operational semantics. J. Log. Algebr. Program. 60-61 ( 2004 ), 17--139. Gordon D. Plotkin. 2004. A structural approach to operational semantics. J. Log. Algebr. Program. 60-61 (2004), 17--139."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939864.1939872"},{"key":"e_1_2_1_46_1","volume-title":"Verilog HDL: A Guide to Digital Design and Synthesis","author":"Samir Palnitkar","unstructured":"Palnitkar Samir . 2003. Verilog HDL: A Guide to Digital Design and Synthesis . Vol. 1 . Prentice Hall Professional . Palnitkar Samir. 2003. Verilog HDL: A Guide to Digital Design and Synthesis. Vol. 1. Prentice Hall Professional."},{"key":"e_1_2_1_47_1","unstructured":"Feng Sheng. 2018. Formalization of MDSEL. Retrieved from https:\/\/github.com\/shengfeng\/formalization_of_MDESL. Feng Sheng. 2018. Formalization of MDSEL. Retrieved from https:\/\/github.com\/shengfeng\/formalization_of_MDESL."},{"key":"e_1_2_1_48_1","volume-title":"Mechanized semantics and refinement of UML-Statecharts. Front. IT 8 EE 18, 11","author":"Sheng Feng","year":"2017","unstructured":"Feng Sheng , Liang Dou , and Zongyuan Yang . 2017. Mechanized semantics and refinement of UML-Statecharts. Front. IT 8 EE 18, 11 ( 2017 ), 1773--1783. Feng Sheng, Liang Dou, and Zongyuan Yang. 2017. Mechanized semantics and refinement of UML-Statecharts. Front. IT 8 EE 18, 11 (2017), 1773--1783."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0453-7"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM\u201904)","author":"Tang Xinbei","year":"2004","unstructured":"Xinbei Tang and Jim Woodcock . 2004 a. Towards mobile processes in unifying theories . In Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM\u201904) . 44--53. Xinbei Tang and Jim Woodcock. 2004a. Towards mobile processes in unifying theories. In Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM\u201904). 44--53."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27764-4_20"},{"key":"e_1_2_1_52_1","volume-title":"Thomas and Philip Moorby","author":"Donald","year":"1995","unstructured":"Donald E. Thomas and Philip Moorby . 1995 . The Verilog Hardware Description Language. Vol. 1 . Kluwer . Donald E. Thomas and Philip Moorby. 1995. The Verilog Hardware Description Language. Vol. 1. Kluwer."},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS\u201997)","author":"Turi Daniele","unstructured":"Daniele Turi and Gordon D. Plotkin . 1997. A formal executable semantics of the JavaCard platform . In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS\u201997) . 280--291. Daniele Turi and Gordon D. Plotkin. 1997. A formal executable semantics of the JavaCard platform. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS\u201997). 280--291."},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the 4th International Symposium on Unifying Theories of Programming (UTP\u201912)","author":"van Staden Stephan","year":"2012","unstructured":"Stephan van Staden and Tony Hoare . 2012 . Algebra unifies operational calculi . In Proceedings of the 4th International Symposium on Unifying Theories of Programming (UTP\u201912) . 88--104. Stephan van Staden and Tony Hoare. 2012. Algebra unifies operational calculi. In Proceedings of the 4th International Symposium on Unifying Theories of Programming (UTP\u201912). 88--104."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2010.12"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/872020.872420"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/647285.723106"},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of the 5th International Symposium on Unifying Theories of Programming (UTP\u201914)","author":"Wu Xiaofeng","year":"2014","unstructured":"Xiaofeng Wu , Huibiao Zhu , and Xi Wu . 2014 . Observation-oriented semantics for calculus of wireless systems . In Proceedings of the 5th International Symposium on Unifying Theories of Programming (UTP\u201914) . 105--124. Xiaofeng Wu, Huibiao Zhu, and Xi Wu. 2014. Observation-oriented semantics for calculus of wireless systems. In Proceedings of the 5th International Symposium on Unifying Theories of Programming (UTP\u201914). 105--124."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0467-1"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-013-3908-2"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90122-X"},{"key":"e_1_2_1_63_1","volume-title":"Proceedings of the International Conference on Software: Theory and Practice. 421--432","author":"Zhu Huibiao","year":"2000","unstructured":"Huibiao Zhu and Jifeng He . 2000 . A semantics of Verilog using duration calculus . In Proceedings of the International Conference on Software: Theory and Practice. 421--432 . Huibiao Zhu and Jifeng He. 2000. A semantics of Verilog using duration calculus. In Proceedings of the International Conference on Software: Theory and Practice. 421--432."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-008-0069-9"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0309-8"},{"key":"e_1_2_1_66_1","volume-title":"Proceedings of the 4th International Symposium on Unifying Theories of Programming (UTP\u201912)","author":"Zhu Huibiao","year":"2012","unstructured":"Huibiao Zhu , Peng Liu , Jifeng He , and Shengchao Qin . 2012 . Mechanical approach to linking operational semantics and algebraic semantics for Verilog using Maude . In Proceedings of the 4th International Symposium on Unifying Theories of Programming (UTP\u201912) . 164--185. Huibiao Zhu, Peng Liu, Jifeng He, and Shengchao Qin. 2012. Mechanical approach to linking operational semantics and algebraic semantics for Verilog using Maude. In Proceedings of the 4th International Symposium on Unifying Theories of Programming (UTP\u201912). 164--185."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3295699","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3295699","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:12:50Z","timestamp":1750201970000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3295699"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,29]]},"references-count":65,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,7,31]]}},"alternative-id":["10.1145\/3295699"],"URL":"https:\/\/doi.org\/10.1145\/3295699","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,29]]},"assertion":[{"value":"2018-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}