These results have been mainly obtained in the framework of the project COLUMBUS IST-2002-38314.
Today, designers face a much diversified landscape when it comes to methodologies, supporting tools, and engineering best practices. This would not necessarily be a problem if it were not for the fact that transitioning between tools that are based on different paradigms is increasingly becoming a design productivity bottleneck. A solution to this problem would be to impose a "homogeneous'' design policy, such as the fully synchronous approach.
However, heterogeneity will naturally manifest itself at the component level where different models of computation may be used to represent component operation and, more frequently, at different levels of abstraction, where, for example, a synchronous-language specification of the design may be refined into a globally asynchronous locally synchronous (GALS) architecture. Combining non functional aspects with functional ones further increases heterogeneity.
Having a sound framework for the heterogeneous modeling of reactive systems gives freedom of choice between different synchronization policies at different stages of the design process, allows to smoothly integrating non functional features, and provides a solid foundation to handle formally communication and coordination among heterogeneous components. This problem can be addressed from both semantic and syntactic sides.
Regarding semantic aspects of heterogeneity, heterogeneous systems are ultimately composed of homogeneous sub-systems or components having different Models of Computation and Communication (MoCC)s. What does the word composed mean in this context? What kind of mathematical parallel composition can give a meaning to this informal statement? This aspect of heterogeneity is referred in our report as "horizontal heterogeneity".
"Vertical heterogeneity" is encountered when traversing the design flow with its different tools. What does it mean to map a design based on a certain MoCC to an architecture based on a different MoCC? What if the design and the architecture are heterogeneous themselves? How can we claim correct-by-construction deployment in these situations?
Our work addresses semantic aspects of heterogeneity in a comprehensive and systematic way.
The following "library" of MoCCs has been explored while developing this theory, and is supported by our approach: synchronous, asynchronous, causalities, scheduling requirements or priorities, timed (in the sense of timed automata), timed (in the sense of performance evaluation), and combinations of these.
Then, the parallel composition of systems with different MoCCs is formally defined. For example, we can precisely state what the parallel composition of a synchronous and an asynchronous system or of a timed and an untimed system, etc., mean.
This figure shows two traces of two different tagged systems, say P and Q. The first systems involves variables X,Y,U and the second one X,Y,V. The common variables X,Y carry the interaction. For each variable, the successive black patches indicate the sequence of values that occurs in the considered trace, call it a signal. Thus, each individual signal is a sequence of ordered values for the associated variable.
A trace composed of a tuple of such signals (one for each variable) is our model of asynchrony: different signals are not mutually synchronized at all. Now, the numbers (e.g., 3, 5, 7, 12) that label the events are tags. For this example, they indicate the reaction index to which the considered event belongs. Therefore, taking these tags into account yields the model of a synchronous trace. As the reader can notice, moving from asynchrony to synchrony is performed by adding one tag component.
The same picture also illustrates how parallel composition can be parameterized. Consider first the two traces shown, and check if they can be combined to form a trace of the parallel composition P || Q, where P and Q are regarded as synchronous systems and the parallel composition is synchronous too. For this case, we need to unify the sequences of values carried by the signals with identical names as well as their associated tags (events for unification must belong to identical reactions). Assume that the sequence of values for shared signals properly unify. As the reader can check, unification is still not possible since the tags differ.
Still, if we ignore tags, we can unify these two traces since we have assumed that shared signals have unifiable sequences of values. This is precisely our model for a Globally Asynchronous Locally Synchronous (GALS) parallel composition, of two synchronous traces using an asynchronous communication medium - an asynchronous medium just ignores tags from synchrony. In the same way, we could also consider an asymmetric parallel composition in which P is synchronous (as shown here) and Q is asynchronous (just remove tags on the second trace), for unification by ignoring tags.
It shows a time-triggered bus to which various subsystems are connected, namely: an asynchronous & timed subsystem, a synchronous & timed subsystem, and a purely asynchronous system. Heterogeneous parallel composition is used to model the network consisting of the bus and its connected subsystems. Of course, this example is somewhat extreme and looks bizarre. But it illustrates the flexibility of modeling.
Then, the following question arises: Which properties of the specification can be preserved at deployment?
Preserving properties is a shared responsibility of the execution infrastructure and the application. In our paper [BCCCSV2004], we formally study what the respective contributions of the infrastructure and the application should be, for preserving semantics at deployment. For example, we were able to prove the correctness of the loosely-time-triggered architecture in use at some aircraft manufacturers. On the other hand, this study opens the possibility to automatically generate, in the specification, proper adaptors that will ensure its robustness at the deployment phase.
[BCCSV2003] A. Benveniste, L. Carloni, P. Caspi, A. Sangiovanni-Vincentelli. ``Heterogeneous Reactive Systems Modeling and Correct-by-Construction Deployment''. Proc. of EMSOFT'2003, R. Alur and I. Lee Eds., Oct. 2003. Extended version available as IRISA Res. Rep.
[BC&al2002]
A. Benveniste, P. Caspi, P. Le Guernic, H. Marchand, J-P. Talpin, and S.
Tripakis. ``A Protocol for Loosely Time-Triggered Architectures''.
In Proc. of 2002 Conference on Embedded Software, EMSOFT'02, J.
Sifakis and A. Sangiovanni-Vincentelli, Eds, LNCS vol 2491, 252--265, Springer
Verlag.