Locality-based normal form approach to linking algebraic semantics and operational semantics for an event-driven system-level language

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 [8, 11]. 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).