Albert Benveniste, Benoit Caillaud, Luca Carloni, Paul Caspi,
and Alberto Sangiovanni-Vincentelli
We present an extension of a mathematical framework proposed by the
authors to deal with the composition of heterogeneous reactive systems.
Our extended framework encompasses diverse models of computation and communication
such as synchronous, asynchronous, causality-based partial orders, and
earliest execution times. We introduce an algebra of tag structures and
morphisms between tag sets to define heterogeneous parallel composition
formally and we use a result on pullbacks from category theory to handle
properly the case of systems derived by composing many heterogeneous components.
The extended framework allows us to establish theorems, from which design
techniques for correct-by-construction deployment of abstract specifications
can be derived. We illustrate
this by providing a complete formal support for correct-by-construction
distributed deployment of a synchronous design specification over an LTTA
medium.
Keywords : reactive systems, embedded systems, synchronous, asynchronous, GALS, formal methods, heterogeneous systems.