caa a22 4500 60551612X CHVBK 20210128100712.0 cr unu---uuuuu 210128e20150101xx s 000 0 eng 10.1007/s00165-014-0309-8 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0309-8 Denotational semantics and its algebraic derivation for an event-driven system-level language [Elektronische Daten] [H. Zhu, Jifeng He, Shengchao Qin, Phillip Brooke] 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 etal. (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. British Computer Society, 2014 Denotational semantics nationallicence Algebraic semantics nationallicence Semantic linking nationallicence Head normal form nationallicence SystemC nationallicence Zhu H. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China aut He Jifeng Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China aut Qin Shengchao School of Computing, University of Teesside, Middlesbrough, UK aut Brooke Phillip School of Computing, University of Teesside, Middlesbrough, UK aut Formal Aspects of Computing Springer London 27/1(2015-01-01), 133-166 0934-5043 27:1<133 2015 27 165 https://doi.org/10.1007/s00165-014-0309-8 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0309-8 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Zhu H. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China aut NATIONALLICENCE 700 1- He Jifeng Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China aut NATIONALLICENCE 700 1- Qin Shengchao School of Computing, University of Teesside, Middlesbrough, UK aut NATIONALLICENCE 700 1- Brooke Phillip School of Computing, University of Teesside, Middlesbrough, UK aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/1(2015-01-01), 133-166 0934-5043 27:1<133 2015 27 165