DocumentCode :
2112256
Title :
Locality-Based Normal Form Approach to Linking Algebraic Semantics and Operational Semantics for an Event-Driven System-Level Language
Author :
Zhu, Huibiao ; Zhao, Yongxin ; He, Jifeng
Author_Institution :
Shanghai Key Lab. of Trustworthy Comput., East China Normal Univ., Shanghai
fYear :
2009
fDate :
14-17 April 2009
Firstpage :
297
Lastpage :
306
Abstract :
As a system-level modeling language, SystemC possesses several novel features such as delayed notifications, notification canceling, notification overriding and delta-cycle. It is challenging to explore the formal semantics for SystemC. We have already explored the operational semantics and denotational semantics for SystemC. A set of algebraic laws has been explored based on these two semantics. In this paper, we study the linking theories of operational semantics and algebraic semantics for SystemC, where our approach is to derive the operational semantics from algebraic semantics. Firstly, we explore the algebraic laws for SystemC via the introduction of the concept of guarded choice, and explore the head normal form for every program. In order to index an instantaneous action to which exact component of a parallel process,the concept of location status (i.e., locality) is introduced. Based on this, every program can be represented in the form of guarded choice. Secondly, we provide the derivation strategy for deriving the operational semantics from the head normal form of each program. Using the derivation strategy, the transition system (i.e., operational semantics) for SystemC is derived by strict proof. Finally, we prove that the derivation strategy is equivalent with the derived operational semantics. This shows that our transition system is sound and complete with respect to the head normal form (or algebraic laws in general).
Keywords :
programming language semantics; specification languages; SystemC; algebraic semantics; event-driven system-level language; locality-based normal form approach; operational semantics; system-level modeling language; Australia; Delay; Formal verification; Hardware design languages; Helium; Joining processes; Kernel; Laboratories; Software engineering; Yarn; Algebraic Semantics; Head Normal Form; Operational Semantics; Semantic Linking; SystemC;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering Conference, 2009. ASWEC '09. Australian
Conference_Location :
Gold Coast, QLD
ISSN :
1530-0803
Print_ISBN :
978-0-7695-3599-9
Type :
conf
DOI :
10.1109/ASWEC.2009.20
Filename :
5076652
Link To Document :
بازگشت