Denotational semantics and its algebraic derivation for an event-driven system-level language
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 60551612X | ||
| 003 | CHVBK | ||
| 005 | 20210128100712.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150101xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-014-0309-8 |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-014-0309-8 | ||
| 245 | 0 | 0 | |a Denotational semantics and its algebraic derivation for an event-driven system-level language |h [Elektronische Daten] |c [H. Zhu, Jifeng He, Shengchao Qin, Phillip Brooke] |
| 520 | 3 | |a 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. | |
| 540 | |a British Computer Society, 2014 | ||
| 690 | 7 | |a Denotational semantics |2 nationallicence | |
| 690 | 7 | |a Algebraic semantics |2 nationallicence | |
| 690 | 7 | |a Semantic linking |2 nationallicence | |
| 690 | 7 | |a Head normal form |2 nationallicence | |
| 690 | 7 | |a SystemC |2 nationallicence | |
| 700 | 1 | |a Zhu |D H. |u Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China |4 aut | |
| 700 | 1 | |a He |D Jifeng |u Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China |4 aut | |
| 700 | 1 | |a Qin |D Shengchao |u School of Computing, University of Teesside, Middlesbrough, UK |4 aut | |
| 700 | 1 | |a Brooke |D Phillip |u School of Computing, University of Teesside, Middlesbrough, UK |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/1(2015-01-01), 133-166 |x 0934-5043 |q 27:1<133 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-014-0309-8 |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-014-0309-8 |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Zhu |D H. |u Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a He |D Jifeng |u Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 200062, Shanghai, China |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Qin |D Shengchao |u School of Computing, University of Teesside, Middlesbrough, UK |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Brooke |D Phillip |u School of Computing, University of Teesside, Middlesbrough, UK |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/1(2015-01-01), 133-166 |x 0934-5043 |q 27:1<133 |1 2015 |2 27 |o 165 | ||