Ismail Assayad, Joseph Sifakis
A Methodology for Construction of Composable Formal Models from SystemC in BIP (2009)
A Methodology for Construction of Composable Formal Models from SystemC in BIP (2009)
TR-2009-9.pdf
Keywords: SystemC, BIP(Behavior-Interaction-Priority), PINAPA
Abstract: We present an approach that is intended to facilitate the integration of domain-specific languages and heterogeneous systems on a semantic level by mapping language constructs to concepts in an asynchronous formalism capable of describing heterogeneous systems. The approach is centered around the use of extended automata to model the behaviors, interactions to model the glue between the transitions of these automata, and finally priorities to choose amongst possible interactions. Using this approach, we present a methodology for modelling SystemC a widely used language for system-level modelling of heterogeneous system-on-chip processes. The methodology incrementally produces (a) readable results opening the way for enhanced verification, (b) models with understandable execution semantics, (c) composable formal models allowing consistent integration with potential domain-specific sub-systems. We show the feasibility of the approach through the simulation and verification of assertion and deadlock properties on a realistic complex system.
