Formalizing TLM with Communicating State Machines

11 years 5 months ago
Formalizing TLM with Communicating State Machines
Transaction Level Models are widely being used as high-level reference models during embedded systems development. High simulation speed and great modeling flexibility are the main reasons for the success of TLMs. While modeling flexibility is desirable for the TLM designer, it generates problems during analysis and verification of the model. In this paper we formalize the notion of Transaction Level Models by introducing a set of rules that allow the transformation of TLMs to a set of communicating state machines. SystemC being the most popular TLM language, we additionally present a finite state model of the SystemC scheduler. Finally, we demonstrate that using our modeling approach, a standard model checker can be employed to formally prove properties on the finite state model.
Bernhard Niemann, Christian Haubelt
Added 11 Jun 2010
Updated 11 Jun 2010
Type Conference
Year 2006
Where FDL
Authors Bernhard Niemann, Christian Haubelt
Comments (0)