Integrating system descriptions by clocked guarded actions

For the description of reactive systems, there is a large number of languages and formalisms, and depending on a particular application or design phase, one of them may be better suited than another one. In the design of reactive systems, their integration is a key issue for a system-wide simulation, analysis and verification. In this paper, we propose clocked guarded actions as a unified intermediate representation for several synchronous and asynchronous models in the design flow, which does not only provide an integrated description but it also allows designers to share common components of the tool infrastructure. Furthermore, we sketch how various models can be translated to this intermediate format, and how the intermediate format can be used for verification (by symbolic model checking) and integrated simulation (by SystemC).