Integrating synchrony & asynchrony is a major issue for the practical use of the synchronous technology, this is why a WP is devoted to it. This WP and the present task summary is presented according to the new organization for the former two WP 4 and 5. Accordingly, a task called timing analysis was introduced in this reorganization, and we report its progresses now.

Approach:

As reported in Task 4/5.1 and 4/5.2, architecture profiling has been devloped by the way of automatically generating, from a given synchronous model of architecture, another synchronous program simulating its timing behaviour. Formally analysing this latter ``real-time model'' can be done easily for simple problems, e.g., ``how much time it takes to perform that particular sequence of actions?''. There are, however, more difficult problems, such as

1. what sequences of actions can happen within 10 time units?
2. what is the fastest possible throughput?

Consider the regular language L=(ab*c)*. It is solution of the following fixpoint equation:  L = l c, l = l b + L a .
You can easily obtain (exercise!) this system of equations by 1/ drawing the two-states automaton recognizing L, 2/ putting symbol Lon the marked state and l on the other state, 3/ interpreting the confluence of branches to states as the  +  of languages and the labelling of a branch by a symbol as the post-concatenation operation. This fixpoint equation can also be regarded in the domain of Schützenberger formal power series in the non-commutative symbols {a,b,c} and boolean coefficients.

Similar fixpoint equations are considered in the so-called MaxPlus semi-ring of formal power series for modelling time. In this semi-ring,  + is to be interpreted as a ordinary max , whereas the multiplication is to be interpreted as the ordinary  + ! In this way, timing models are constructed based on the synchronisation principle ``waiting for the latest input to come, then computing''. Diagrams are attached to such systems of fixpoint equations, exactly following the same principles as for regular languages and automata.

Achieved Results:

• We have remarked that the two types of diagrams can be blended into a unified one, encoding fixpoint equations in semi-rings of formal power series combining languages of actions, and quatitative time following the MaxPlus rules. Formally speaking, the blending is achieved by means of a tensor product. We call timed diagrams the so obtained diagrams. Timed diagrams allow us to represent and manipulate fixpoint equations, associated with power series corresponding to MaxPlus automata.
• We have shown how the formalism of hierarchical Mode Machines (hMM, cf. the work of F. Maraninchi on Mode Machines, in WP2) is structurally encoded into our timed diagrams. This opens the route of possibly efficient symbolic manipulations in this algebra, and requires further investigation.
• We have started a work to equip hMSC (high-level Message Sequence Charts) with time, and we show how to map hMSC enhanced with time into timed diagrams. This modelling approach has been illustrated on the alternate bit protocol, which we modelled using timed hMSC. This allows us to compute properties related to the long range timing behaviour of the protocol, by answering questions such as:
• what is the throughput of this protocol?
• will the buffers grow to infinity?

1. A. Benveniste, C. Jard, S. Gaubert. ``Algebraic techniques for timed systems''. 9th Concur'98, Nice, France, Sept. 98, Sangiorgi & de Simone Eds, LNCS 1466, 373-388, 1998.

 
2. A. Benveniste , S. Gaubert, C. Jard. ``Monotone rational series and max-plus algebraic models of real-time systems''. Wodes'98, August 1998.

 
3. Pierre Le Maigat, Loic Helouet. ``(Max,+), a new approach for time in Message Sequence Charts'',

Irisa Res. Rep., in preparation.