SYRF Project
Task 4/5.3: "Integrating synchrony
& asynchrony: timing analysis"
Abstract of deliverable
4/5.3
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
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:
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 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: