SYRF Project

Task 4/5.3: "Integrating synchrony & asynchrony: timing analysis"

Abstract of deliverable 4/5.3

Back to the SYRF Home Page



Foreword:

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.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?

Question 1 is non trivial, although it could probably be handled using timed automata techniques and related tools. Question 2 involves the asymptotic stationary behaviour of the architecture, it is (as far as we understand) not accessible to model checking type of techniques, even enhanced to timed automata. It is, however, accessible to the alternative formalisms we study in this task: so-called MaxPlus automata have been introduced in the ``MaxPlus'' community (cf. the Alapedes LTR project), let us sketch what they are.

Consider the regular language L=(ab*c)*. It is solution of the following system of fixpoint equations:

You can easily obtain (exercise!) this system of equations by 1/ drawing the two-states automaton recognizing L , 2/ putting symbol L on 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 system of fixpoint equations can also be regarded in the domain of Schützenberger formal power series in the non-commutative symbols {a,b,c} and boolean coefficients.

Aha! 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:

As for the perspective beyond paper work, we tend to rely on external work forces for the development of symbolic manipulation tools for MaxPlus automata & related formal power series, and would prefer to focus on linking such engines to one of our synchronous formalisms, à la hMM. As a deliverable, we have chosen to provide a slightly enhanced version of our slides for Concur'98.

Publications:

  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.