Abstract
As a system-level modelling language, SystemC possesses several novel features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. It also has real-time and shared-variable features. Previously we have studied an operational semantics for SystemC Peng et al. (An operational semantics of an event-driven system-level simulator, pp 190–200, 2006) and bisimulation has been introduced based on some aspects of reasonable abstractions. The denotational method is another approach to studying the semantics of a programming language. It provides the mathematical meaning to programs and can predict the behaviour of programs. Due to the novel features of SystemC, it is challenging to study the denotational semantics for SystemC. In this paper, we apply Unifying Theories of Programming (abbreviated as UTP) Hoare and He (Unifying theories of programming, 1998) in exploring the denotational semantics. Two trace variables are introduced, one to record the state behaviours and another to record the event behaviours. The timed model is formalized in a threedimensional structure. A set of algebraic laws is explored, which can be proved via the presented denotational semantics. In this paper, we also consider the linking between denotational semantics and algebraic semantics. The linking is obtained by deriving the denotational semantics from algebraic semantics for SystemC. A complete set of parallel expansion laws is explored, where the location status of an instantaneous action is studied. The location status indicates an instantaneous action is due to which exact parallel component. We introduce the concept of head normal form for each program and every program is expressed in the form of guarded choice with location status. Based on this, the derivation strategy for deriving denotational semantics from algebraic semantics is provided.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Bresciani R, Butterfield A (2012) A UTP semantics of pGCL as a homogeneous relation. In: Proceedings of IFM 2012: 9th International Conference on integrated formal methods, Pisa, Italy, June 18–21, 2012, volume 7321 of lecture notes in computer science. Springer, pp 191–205
Bresciani R, Butterfield A (2013) From distributions to probabilistic reactive programs. In: Proceedings of ICTAC 2013: 10th International Colloquium on theoretical aspects of computing, Shanghai, China, September 4–6, 2013, volume 8049 of lecture notes in computer science. Springer, pp 94–111
Bresciani R, Butterfield A (2013) A probabilistic theory of designs based on distributions. In: Proceedings of UTP 2012: 4th International Symposium, on unifuying theories of programming, Paris, France, 27–28 August, 2012, volume 7681 of lecture notes in computer science. Springer, pp 105–123
Börger E, Stärk R (2003) Abstract state machines: a method for high-level system design and analysis. Springer, London
Cimatti A, Griggio A, Micheli A, Narasamdya I, Roveri M (2011) Kratos—a software model checker for systemc. In: Proceedings of CAV 2011: 23rd International Conference on computer aided verification, Snowbird, UT, USA, July 14–20, 2011, volume 6806 of lecture notes in computer science, pp 310–316
Cimatti A, Micheli A, Narasamdya I, Roveri M (2010) Verifying SystemC: A software model checking approach. In: Proceedings of FMCAD 2010: 10th International Conference on formal methods in computer-aided design. IEEE Computer Society, pp 51–59
Cavalcanti A, Wellings AJ, Woodcock J: The safety-critical Java memory model formalised. Formal Aspects Comput 25(1), 37–57 (2013)
Desharnais J, Gupta V, Jagadeesan R, Panangaden P: Metrics for labelled Markov processes. Theor Computer Sci 318(3), 323–354 (2004)
Gawanmeh A, Habibi A, Tahar S (2004) An executable operational semantics for SystemC using abstract state machines. Technical report, Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada
He J (1994) Provably correct systems: modelling of communication languages and design of optimized compilers. The McGraw-Hill International Series in Software Engineering
Hoare CAR, He J: From algebra to operational semantics. Inf Process Lett 45, 75–80 (1993)
Hoare CAR, He J (1998) Unifying theories of programming. Prentice Hall International Series in Computer Science
Hoare CAR, Hayes IJ, He J, Morgan C, Roscoe AW, Sanders JW, Sørensen IH, Spivey JM, Sufrin B: Laws of programming.. Commun ACM 38(8), 672–686 (1987)
Hoare CAR, He J, Sampaio A: Normal form approach to compiler design. Acta Inf 30, 701–739 (1993)
Hoare CAR, He J, Sampaio A (1997) Algebraic derivation of an operational semantics. In: Plotkin G, Stirling C, Tofte M (eds) Proof, language and interaction: essays in honour of Robin Milner, foundations of computer science series. The MIT Press, London
He J, Li X, Liu Z: rCOS: a refinement calculus of object systems. Theor Computer Sci 365(1-2), 109–142 (2006)
Hoare CAR (1985) Communicating sequential processes. Prentice Hall International Series in computer science
Hoare CAR (2011) Algebra of concurrent programming. In: Meeting 52 of WG 2.3
He J, Seidel K, McIver A: Probabilistic models for the guarded command language. Sci Computer Progr 28(2–3), 171–192 (1997)
Habibi A, Tahar S: SystemC fixpoint semantics. Department of Electrical and Computer Engineering, Technical report (2005)
Hoare T, van Staden S: In praise of algebra. Formal Aspects Comput 24(4–6), 423–431 (2012)
Hoare T, van Staden S, Möller B, Struth G, Villard J, Zhu H, O’Hearn P (2014) Developments in concurrent kleene algebra. In: Proceedings of RAMiCS 2014: 14th International Conference on Relational and Algebraic Methods in Computer Science, Marienstatt im Westerwald, Germany 28 April–1 May 2014, volume 8428 of lecture notes in computer science. Springer, pp 1–18
Jones RB (1992) Methods and tools for the verification of critical properties. In: Proceedings of the 5th Refinement Workshop, organised by BCS-FACS. Springer, London, pp 88–118
McIver A, Morgan C (2004) Abstraction, refinement and proof of probability systems. Monographs in computer science. Springer
Oliveira M, Cavalcanti A, Woodcock J: A UTP semantics for Circus. Formal Aspects Comput 21(1–2), 3–32 (2009)
Oliveira M, Cavalcanti A, Woodcock J: Unifying theories in ProofPower-Z. Formal Aspects Comput 25(1), 133–158 (2013)
Open SystemC Initiative (OSCI) (2001) Functional specification for SystemC 2.0
Open SystemC Initiative (OSCI) (2003) SystemC 2.0.1 language reference manual
Owre S, Shankar N, Rushby JM, Stringer-Calvert DWJ: PVS language reference. Computer Science Laboratory, SRI International (1999)
Owre S, Shankar N, Rushby JM, Stringer-Calvert DWJ: PVS system guide. Computer Science Laboratory, SRI International (1999)
Plotkin G (2004) A structural approach to operational semantics. Technical Report 19, University of Aahus, 1981. J Logic Alg Progr 60–61:17–139
Peng X, Zhu H, He J, Jin N (2006) An operational semantics of an event-driven system-level simulator. In: Proceedings of SEW-30: The 30th IEEE/NASA software engineering workshop, Columbia, Maryland, USA. IEEE Computer Society Press, pp 190–200
Ruf J, Hoffmann DW, Gerlach J, Kropf T, Rosenstiel W, Müller W (2001) The simulation semantics of SystemC. In: DATE ’01: Proceedings of the conference on design, automation and test in Europe. IEEE Press, Piscataway, pp 64–70
Salem A (2003) Formal semantics of synchronous SystemC. In: Proceedings of Date’03: design, automation and test in Europe Conference and exposition. IEEE Computer Society, pp 10376–10381
Sampaio A (1997) An algebraic approach to compiler design. World Scientific
Sherif A, Cavalcanti A, He J, Sampaio A: A process algebraic framework for specification and validation of real-time systems. Formal Aspects Comput 22(2), 153–191 (2010)
Shankar N, Owre S, Rushby JM, Stringer-Calvert DWJ (1999) PVS prover guide. Computer Science Laboratory, SRI International, Menlo Park
Stoy J: Denotational semantics: the Scott–Strachey approach to programming language. MIT Press, New York (1977)
Swan S. Producer consumer example. http://forums.accellera.org/topic/1215-systemc-examples/
Verilog (2001) IEEE standard hardware description language based on the Verilog hardware description language, volume IEEE Standard 1364-2001. IEEE
van Staden S, Hoare T (2013) Algebra unifies operational calculi. In: Proceedings of UTP 2012: 4th International Symposium, on unifuying theories of programming, Paris, France, 27–28 August, 2012, volume 7681 of lecture notes in computer science. Springer, pp 88–104
Watt D: Programming language syntax and semantics. Prentice Hall, London (1991)
Woodcock J, Cavalcanti A (2001) The steam boiler in unified theory of Z and CSP. In: Proceedings of APSEC 2001: 8th Asia-Pacific software engineering conference. IEEE Computer Society Press, pp 291–298
Woodcock J, Cavalcanti A (2002) The semantics of Circus. In: Proceedings of ZB 2002: 2nd International Conference of B and Z Users, Grenoble, France, January 23–25, 2002, volume 2272 of lecture notes in computer science. Springer, pp 184–203
Zhang W. Verds tool. http://lcs.ios.ac.cn/~zwh/verds/index.html
Zhu H, He J, Peng X, Jin N (2010) Denotational approach to event-driven system level language. In: Proceedings of UTP 2008: 2nd International Symposium on unifying theories of programming, Dublin, Ireland, 8–10 September, 2008, volume 5713 of lecture notes in computer science. Springer, pp 258–278
Zhu H (2005) Linking the semantics of a multithreaded discrete event simulation language. PhD thesis, London South Bank University
Zhu H, Yang F, He J (2010) Generating denotational semantics from algebraic semantics for event-driven system-level language. In: Proceedings of UTP 2010: 3rd International Symposium on unifying theories of programming, Shanghai, China, 15–16 November, 2010, volume 6445 of lecture notes in computer science. Springer, pp 286–308
Zeng N, Zhang W (2013) A SystemC semantics in guarded assignment systems and its applications with verds. In: Proceedings of APSEC 2013: 20th Asia-Pacific software engineering conference. IEEE Computer Society Press, pp 371–379
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Zhu, H., He, J., Qin, S. et al. Denotational semantics and its algebraic derivation for an event-driven system-level language. Form Asp Comp 27, 133–166 (2015). https://doi.org/10.1007/s00165-014-0309-8
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-014-0309-8