{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:39:17Z","timestamp":1761323957616,"version":"3.40.4"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2015,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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\u00a0al. (An operational semantics of an event-driven system-level simulator, pp 190\u2013200,<jats:xref ref-type=\"bibr\">2006<\/jats:xref>) 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<jats:italic>Unifying Theories of Programming<\/jats:italic>(abbreviated as<jats:italic>UTP<\/jats:italic>) Hoare and He (Unifying theories of programming,<jats:xref ref-type=\"bibr\">1998<\/jats:xref>) 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.<\/jats:p>","DOI":"10.1007\/s00165-014-0309-8","type":"journal-article","created":{"date-parts":[[2014,8,12]],"date-time":"2014-08-12T06:15:34Z","timestamp":1407824134000},"page":"133-166","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Denotational semantics and its algebraic derivation for an event-driven system-level language"],"prefix":"10.1145","volume":"27","author":[{"given":"H.","family":"Zhu","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[{"name":"School of Computing, University of Teesside, Middlesbrough, UK"}]},{"given":"Phillip J.","family":"Brooke","sequence":"additional","affiliation":[{"name":"School of Computing, University of Teesside, Middlesbrough, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"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\u201321 2012 volume 7321 of lecture notes in computer science. Springer pp 191\u2013205","DOI":"10.1007\/978-3-642-30729-4_14"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"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\u20136 2013 volume 8049 of lecture notes in computer science. Springer pp 94\u2013111","DOI":"10.1007\/978-3-642-39718-9_6"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"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\u201328 August 2012 volume 7681 of lecture notes in computer science. Springer pp 105\u2013123","DOI":"10.1007\/978-3-642-35705-3_5"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"B\u00f6rger E St\u00e4rk R (2003) Abstract state machines: a method for high-level system design and analysis. Springer London","DOI":"10.1007\/978-3-642-18216-7"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Cimatti A Griggio A Micheli A Narasamdya I Roveri M (2011) Kratos\u2014a software model checker for systemc. In: Proceedings of CAV 2011: 23rd International Conference on computer aided verification Snowbird UT USA July 14\u201320 2011 volume 6806 of lecture notes in computer science pp 310\u2013316","DOI":"10.1007\/978-3-642-22110-1_24"},{"key":"e_1_2_1_2_6_2","unstructured":"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\u201359"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0253-4"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.09.013"},{"key":"e_1_2_1_2_9_2","unstructured":"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"},{"key":"e_1_2_1_2_10_2","unstructured":"He J (1994) Provably correct systems: modelling of communication languages and design of optimized compilers. The McGraw-Hill International Series in Software Engineering"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90219-Y"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR He J (1998) Unifying theories of programming. Prentice Hall International Series in Computer Science","DOI":"10.1007\/BFb0002714"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/27651.27653"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01191809"},{"key":"e_1_2_1_2_15_2","unstructured":"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"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.034"},{"key":"e_1_2_1_2_17_2","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice Hall International Series in computer science"},{"key":"e_1_2_1_2_18_2","unstructured":"Hoare CAR (2011) Algebra of concurrent programming. In: Meeting 52 of WG 2.3"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"volume-title":"SystemC fixpoint semantics","year":"2005","author":"Habibi A","key":"e_1_2_1_2_20_2"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0249-0"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Hoare T van Staden S M\u00f6ller B Struth G Villard J Zhu H O\u2019Hearn 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\u20131 May 2014 volume 8428 of lecture notes in computer science. Springer pp 1\u201318","DOI":"10.1007\/978-3-319-06251-8_1"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"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\u2013118","DOI":"10.1007\/978-1-4471-3550-0_6"},{"key":"e_1_2_1_2_24_2","unstructured":"McIver A Morgan C (2004) Abstraction refinement and proof of probability systems. Monographs in computer science. Springer"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0052-5"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0044-5"},{"key":"e_1_2_1_2_27_2","unstructured":"Open SystemC Initiative (OSCI) (2001) Functional specification for SystemC 2.0"},{"key":"e_1_2_1_2_28_2","unstructured":"Open SystemC Initiative (OSCI) (2003) SystemC 2.0.1 language reference manual"},{"volume-title":"PVS language reference","year":"1999","author":"Owre S","key":"e_1_2_1_2_29_2"},{"volume-title":"PVS system guide","year":"1999","author":"Owre S","key":"e_1_2_1_2_30_2"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Plotkin G (2004) A structural approach to operational semantics. Technical Report 19 University of Aahus 1981. J Logic Alg Progr 60\u201361:17\u2013139","DOI":"10.1016\/j.jlap.2004.05.001"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"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\u2013200","DOI":"10.1109\/SEW.2006.10"},{"key":"e_1_2_1_2_33_2","unstructured":"Ruf J Hoffmann DW Gerlach J Kropf T Rosenstiel W M\u00fcller W (2001) The simulation semantics of SystemC. In: DATE \u201901: Proceedings of the conference on design automation and test in Europe. IEEE Press Piscataway pp 64\u201370"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Salem A (2003) Formal semantics of synchronous SystemC. In: Proceedings of Date\u201903: design automation and test in Europe Conference and exposition. IEEE Computer Society pp 10376\u201310381","DOI":"10.1109\/DATE.2003.1253637"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Sampaio A (1997) An algebraic approach to compiler design. World Scientific","DOI":"10.1142\/2870"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0119-6"},{"key":"e_1_2_1_2_37_2","unstructured":"Shankar N Owre S Rushby JM Stringer-Calvert DWJ (1999) PVS prover guide. Computer Science Laboratory SRI International Menlo Park"},{"volume-title":"Denotational semantics: the Scott\u2013Strachey approach to programming language","year":"1977","author":"Stoy J","key":"e_1_2_1_2_38_2"},{"key":"e_1_2_1_2_39_2","unstructured":"Swan S. Producer consumer example. http:\/\/forums.accellera.org\/topic\/1215-systemc-examples\/"},{"key":"e_1_2_1_2_40_2","unstructured":"Verilog (2001) IEEE standard hardware description language based on the Verilog hardware description language volume IEEE Standard 1364-2001. IEEE"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"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\u201328 August 2012 volume 7681 of lecture notes in computer science. Springer pp 88\u2013104","DOI":"10.1007\/978-3-642-35705-3_4"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.5555\/120468"},{"key":"e_1_2_1_2_43_2","unstructured":"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\u2013298"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"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\u201325 2002 volume 2272 of lecture notes in computer science. Springer pp 184\u2013203","DOI":"10.1007\/3-540-45648-1_10"},{"key":"e_1_2_1_2_45_2","unstructured":"Zhang W. Verds tool. http:\/\/lcs.ios.ac.cn\/~zwh\/verds\/index.html"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"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\u201310 September 2008 volume 5713 of lecture notes in computer science. Springer pp 258\u2013278","DOI":"10.1007\/978-3-642-14521-6_15"},{"key":"e_1_2_1_2_47_2","unstructured":"Zhu H (2005) Linking the semantics of a multithreaded discrete event simulation language. PhD thesis London South Bank University"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"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\u201316 November 2010 volume 6445 of lecture notes in computer science. Springer pp 286\u2013308","DOI":"10.1007\/978-3-642-16690-7_15"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"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\u2013379","DOI":"10.1109\/APSEC.2013.57"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-014-0309-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-014-0309-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-014-0309-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T04:25:13Z","timestamp":1746332713000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-014-0309-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1]]}},"alternative-id":["10.1007\/s00165-014-0309-8"],"URL":"https:\/\/doi.org\/10.1007\/s00165-014-0309-8","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2015,1]]}}}