SYRF Project
Task 3.1: "Symbolic abstraction of automata"
Abstract of deliverable 3.1.2
Achieved Results:
Automatic verification and model-checking rely on
precise formal semantics, as provided in synchronous reactive formalisms.
Then many avenues of analysis techniques can be applied, each relying
on some form of symbolic abstraction of the underlying reactive automata.
The deliverable contains contribution from three distinct sites (INRIA
Meije, INRIA Spectre, and INRIA Ep-Atr).
Work at INRIA Meije focused this year on the development of methods for
Compositional reduction of Boolean Equation Systems. Such systems form
a natural target for compilation from Esterel, and bear strong ties
with synchronous hardware circuits at RTL level. The topic of compositional
reduction methods is important here since these reductions can often be
drastic in practice, provided the description does not blow up in the middle
of the algorithm. Reducing components often helps a great deal. Annex 3.1.2.a is a presentation of the Xeve tool.
Work at INRIA Spectre focused on the formal definition of a new
property of interest, called stability. Stable systems are those which may not evolve forever, producing outputs, without further input events.
Technical material is provided as
annex 3.1.2.b.
Work at INRIA Ep-Atr focused on the study of
intensional Labeled Transition Systems as a representation model, and
the computation of bisimulation minimal forms on this representation and on
discrete event controller synthesis.
Technical material is provided as
annex 3.1.2.c and
annex 3.1.2.d.