More Web Proxy on the site http://driver.im/

research-article

Open access

Theoretical and Practical Approaches to the Denotational Semantics for MDESL based on UTP

Authors:

Jonathan P. BowenAuthors Info & Claims

Formal Aspects of Computing, Volume 32, Issue 2-3

Pages 275 - 314

https://doi.org/10.1007/s00165-020-00513-4

Published: 01 July 2020 Publication History

Abstract

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.

References

References

[1]

Arenas AE and Bicarregui J Applying unifying theories of programming to real-time programming Trans SDPS 2006 10 4 69-88

[2]

Adam C Certified programming with dependent types 2011 New York MIT Press

[3]

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–402. Springer

[4]

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–73

[5]

Bresciani R and Butterfield A A UTP approach towards probabilistic protocol verification Secur Commun Netw 2014 7 1 99-107

Digital Library

[6]

Butterfield A, Catháin A (2009) Concurrent models of flash memory device behaviour. In: The 12th Brazilian symposium on formal methods, pp 70–83, Brazil

[7]

Bertot Y, Castéran P (2013) Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Springer Science & Business Media

[8]

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–207. IEEE

[9]

Blazy S and Leroy X Mechanized semantics for the clight subset of the C language J Automat Reason 2009 43 3 263-288

[10]

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–32

[11]

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–100

[12]

Blech JO and Schätz B Towards a formal foundation of behavioral types for UML state-machines ACM SIGSOFT Softw Eng Notes 2012 37 4 1-8

Digital Library

[13]

Butterfield A (2008) Unifying theories of programming. Second international symposium, UTP 2008, Dublin, Ireland, September 8–10, 2008. Revised selected papers, volume 5713 of lecture notes in computer science. Springer

[14]

Butterfield A (2016) UTPCalc—a calculator for UTP predicates. In: The 6th international symposium on unifying theories of programming, pp 197–216

[15]

Butterfield A (2017) UTCP: compositional semantics for shared-variable concurrency. In: The 20th Brazilian symposium on formal methods: foundations and applications, pp 253–270

[16]

Bowen JP, Zhu H (2016) Unifying theories of programming. 6th international symposium, UTP 2016, Reykjavik, Iceland, June 4–5, 2016. Revised selected papers, volume 10134 of lecture notes in computer science. Springer

[17]

Chatzikyriakidis S, Luo Z (2016) Proof assistants for natural language semantics. In: The 9th international conference on logical aspects of computational linguistics, pp 85–98

[18]

Choi J, Vijayaraghavan M, Sherman B, Chlipala A, and Arvind Kami: a platform for high-level parametric hardware specification and its modular verification Proc ACM Program Lang 2017 1 24 1-30

Digital Library

[19]

Cavalcanti A, Wellings AJ, and Woodcock J The safety-critical java memory model formalised Formal Asp Comput 2013 25 1 37-57

Digital Library

[20]

Dimitrov J (2001) Operational semantics for Verilog. In: The 8th Asia-Pacific software engineering conference, pp 161–168. IEEE

[21]

Dunne S, Stoddart B (2006) Unifying Theories of Programming. First international symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5–7, 2006, revised selected papers. volume 4010 of lecture notes in computer science. Springer

[22]

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

[23]

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

[24]

Foster S, Zeyda F, Woodcock J (2014) Isabelle/UTP: a mechanised theory engineering framework. In: International Symposium on unifying theories of programming, pp 21–41. Springer

[25]

Gordon M (1995) The semantic challenge of verilog hdl. In: Proceedings of tenth annual IEEE symposium on logic in computer science, pp 136–145

[26]

Gordon MJC Relating event and trace semantics of hardware description languages Comput J 2002 45 1 27-36

[27]

Hansen MR and Chaochen Z Duration calculus: logical foundations Formal Asp Comput 1997 9 3 283-330

Digital Library

[28]

He J (2003) An algebraic approach to the Verilog programming. In: Formal methods at the crossroads. From Panacea to Foundational Support, pp 65–80. Springer

[29]

Hoare CAR, He J (1998) Unifying theories of programming. volume 14. Prentice Hall Englewood Cliffs

[30]

He J and Hoare CAR Linking theories in probabilistic programming Inf Sci 1999 119 3–4 205-218

[31]

Hoare CAR, He J, and Sampaio A Normal form approach to compiler design Acta Inform 1993 30 8 701-739

Digital Library

[32]

Huet G, Kahn G, Paulin-Mohring C (2004) The coq proof assistant a tutorial. Rapport Technique, 178

[33]

He J, Li X, and Liu Z rcos: A refinement calculus of object systems Theor Comput Sci 2006 365 1–2 109-142

Digital Library

[34]

Hoare T Laws of programming: The algebraic unification of theories of concurrency The 25th international conference on concurrency theory 2014 Rome Italy 1-6

[35]

He J, Seidel K, and McIver A Probabilistic models for the guarded command language Sci Comput Program 1997 28 2–3 171-192

Digital Library

[36]

He J, Xu Q (2000) An operational semantics of a simulator algorithm. In The proceedings of the PDPTA, pp 26–29

[37]

He J and Xu Q Advanced features of duration calculus and their applications in sequential hybrid programs Formal Asp Comput 2003 15 1 84-99

[38]

He J, Zhu H (2000) Formalising Verilog. In The 7th IEEE international conference on electronics, circuits and systems, vol 1, pp 412–415. IEEE

[39]

IEEE (2001) IEEE standard hardware description language based on the Verilog hardware description language. IEEE Standard 1364-2001

[40]

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–351. Springer

[41]

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–548

[42]

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–54

[43]

Li Y, He J (2000) Formalising verilog: Operational semantics and bisimulation. Technical report

[44]

Miculan M On the formalization of the modal

μ

-calculus in the calculus of inductive constructions Inf. Comput. 2001 164 1 199-231

Digital Library

[45]

Meredith P, Katelman M, Meseguer J, Roşu G (2010) A formal executable semantics of Verilog. In: The 8th IEEE/ACM international conference on formal methods and models for codesign, pp 179–188. IEEE

[46]

Manna Z, Pnueli A (1981) Verification of concurrent programs. Part I. The temporal framework. Technical report. Department of Computer Science, Stanford University, California

[47]

Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer Science & Business Media

[48]

Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer Science & Business Media

[49]

Naumann D (2014) Unifying theories of programming—5th international symposium, UTP 2014, Singapore, May 13, 2014. Revised selected papers. volume 8963 of lecture notes in computer science. Springer

[50]

Oliveira M, Cavalcanti A, and Woodcock J A UTP semantics for Circus Formal Asp Comput 2009 21 1–2 3-32

Digital Library

[51]

Oliveira M, Cavalcanti A, and Woodcock J Unifying theories in ProofPower-Z Formal Asp Comput 2013 25 1 133-158

Digital Library

[52]

Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In 11th international conference on automated deduction, pp 748–752, USA

[53]

Palmskog K, Gligoric M, Peña L, Moore B, Rosu G (2018) Verification of casper in the coq proof assistant. Technical report

[54]

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–73

[55]

Qin S (2010) Unifying theories of programming—third international symposium, UTP 2010, Shanghai, China, November 15–16, 2010. Proceedings. volume 6445 of Lecture notes in computer science. Springer

[56]

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–390

[57]

Sheng F, Dou L, and Yang Z Mechanized semantics and refinement of UML-Statecharts Front Inf Technol Electron Eng 2017 18 11 1773-1783

[58]

Sheng F (2018) Formalization of Verilog. https://github.com/shengfeng/formalization_of_MDESL/blob/master/denotational_semantics.v

[59]

Slind K, Norrish M (2008) A brief overview of HOL4. In: The 21st international conference on theorem proving in higher order logics, pp 28–32

[60]

Shi L, Zhao Y, Liu Y, Sun J, Dong JS, and Qin S A UTP semantics for communicating processes with shared variables and its formal encoding in PVS Formal Asp Comput 2018 30 3–4 351-380

Digital Library

[61]

Sheng F, Zhu H, Yang Z, He J, and Bowen JP Theoretical and practical aspects of linking operational and algebraic semantics for mdesl ACM Trans Softw Eng Methodol 2019 28 3 1-46

Digital Library

[62]

Tarski A et al. A lattice-theoretical fixpoint theorem and its applications Pac J Math 1955 5 2 285-309

[63]

Tang X, Woodcock J (2004) Towards mobile processes in unifying theories. In: The 2nd international conference on software engineering and formal methods, pp 44–53, Beijing

[64]

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–298, China

[65]

Woodcock J, Cavalcanti A (2002) The semantics of circus. In The 2nd International Conference of B and Z Users, pp 84–203, France

[66]

Wolff B, Gaudel M-C, Feliachi A (2012) Unifying theories of programming, 4th international symposium, UTP 2012, Paris, France, August 27–28, 2012. Revised Selected Papers. volume 7681 of lecture notes in computer science. Springer,

[67]

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–182

[68]

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–124, Singapore

[69]

Xie W, Xiang S, and Zhu H A utp approach for rtimo Formal Asp Comput 2018 30 6 713-738

Digital Library

[70]

Zhu H, He J (2000) A DC-based semantics for Verilog. In Proceedings of the ICS, pp 421–432. Citeseer

[71]

Zhu H, He J (2000) A semantics of Verilog using Duration Calculus. In Proceedings of international conference on software: theory and practice, pp 421–432

[72]

Zhu H, He J, and Bowen JP From algebraic semantics to denotational semantics for Verilog Innov Syst Softw Eng 2008 4 4 341-360

[73]

Zhou C, Hoare CAR, and Ravn AP A calculus of durations Inf Process Lett 1991 40 5 269-276

[74]

Zhu H (2005) Linking the semantics of a multithreaded discrete event simulation language. PhD thesis, London South Bank University

Cited By

Zhao HZhu HSheng FHe JBowen J(2024)Theoretical and Practical Approach to the Soundness and Completeness of Operational Semantics based on Denotational Semantics for MDESLFormal Aspects of Computing10.1145/3696432Online publication date: 25-Sep-2024
https://dl.acm.org/doi/10.1145/3696432
Li RZhu HBanach R(2024)An algebraic approach to simulation and verification for cyber-physical systems with shared-variable concurrencyJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100973139(100973)Online publication date: Jun-2024
https://doi.org/10.1016/j.jlamp.2024.100973
Butterfield A(2024)Towards an Algebra for Unifying Theories of Concurrent Programming (UTCP)The Application of Formal Methods10.1007/978-3-031-67114-2_9(203-232)Online publication date: 1-Sep-2024
https://doi.org/10.1007/978-3-031-67114-2_9
Show More Cited By

Recommendations

Theoretical and Practical Aspects of Linking Operational and Algebraic Semantics for MDESL

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 ...
Theoretical and Practical Approach to the Soundness and Completeness of Operational Semantics based on Denotational Semantics for MDESL
Verilog is a hardware description language (HDL) that has become an industry-standard HDL of IEEE. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. Previously, we have studied the operational semantics and denotational ...
Linking denotational semantics with operational semantics for web services

Web Services have become more and more important in these years, and BPEL4WS (BPEL) is a de facto standard for the web service composition and orchestration. It contains several distinct features, including the scope-based compensation and fault ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 32, Issue 2-3

Jul 2020

203 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2020.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 July 2020

Accepted: 10 April 2020

Received: 13 July 2019

Published in FAC Volume 32, Issue 2-3

Author Tags

Qualifiers

Research-article

Funding Sources

National Natural Science Foundation of China (CN)
National Key Research and Development Program of China

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
152
Total Downloads

Downloads (Last 12 months)60
Downloads (Last 6 weeks)10

Reflects downloads up to 18 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhao HZhu HSheng FHe JBowen J(2024)Theoretical and Practical Approach to the Soundness and Completeness of Operational Semantics based on Denotational Semantics for MDESLFormal Aspects of Computing10.1145/3696432Online publication date: 25-Sep-2024
https://dl.acm.org/doi/10.1145/3696432
Li RZhu HBanach R(2024)An algebraic approach to simulation and verification for cyber-physical systems with shared-variable concurrencyJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100973139(100973)Online publication date: Jun-2024
https://doi.org/10.1016/j.jlamp.2024.100973
Butterfield A(2024)Towards an Algebra for Unifying Theories of Concurrent Programming (UTCP)The Application of Formal Methods10.1007/978-3-031-67114-2_9(203-232)Online publication date: 1-Sep-2024
https://doi.org/10.1007/978-3-031-67114-2_9
Li XZhang QWang GShi ZGuan Y(2023)A unified proof technique for verifying program correctness with big-step semanticsJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2022.102820136:COnline publication date: 1-Mar-2023
https://dl.acm.org/doi/10.1016/j.sysarc.2022.102820
Butterfield ATuong F(2023)Applying Formal Verification to an Open-Source Real-Time Operating SystemTheories of Programming and Formal Methods10.1007/978-3-031-40436-8_13(348-366)Online publication date: 8-Sep-2023
https://doi.org/10.1007/978-3-031-40436-8_13
Bowen JZhu H(2023)Jifeng He at Oxford and Beyond: An AppreciationTheories of Programming and Formal Methods10.1007/978-3-031-40436-8_1(3-18)Online publication date: 8-Sep-2023
https://doi.org/10.1007/978-3-031-40436-8_1
Xiao LZhu H(2022)UTP semantics for the MCA ARMv8 architectureJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2022.102438125:COnline publication date: 1-Apr-2022
https://dl.acm.org/doi/10.1016/j.sysarc.2022.102438
Xiao LZhu HXu Q(2021)Trace Semantics and Algebraic Laws for Total Store Order Memory ModelJournal of Computer Science and Technology10.1007/s11390-021-1616-136:6(1269-1290)Online publication date: 1-Dec-2021
https://dl.acm.org/doi/10.1007/s11390-021-1616-1
Li XZhang QWang GShi ZGuan Y(2021)Reasoning About Iteration and Recursion Uniformly Based on Big-Step SemanticsDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-030-91265-9_4(61-80)Online publication date: 25-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-91265-9_4

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents