Next: Conclusions
Up: The
NonLinear World Previous: The
CANDEMAT case
The ONERACERT case
Communicated by A. Burgueño and ellaborated by L. GonzalezVega
and N. GonzalezCampos
The ONERACERT (Centre d'Études et de Recherche de l'École
Normale Supérieure de l'Aéronautique de l'Espace) is
a research laboratory at Toulouse which depends of the ``Office National
d'Études et de Recherches Aerospatiales".
One of the critical steps when they implement prototypes modelling slopeparametric
hybrid automata (see F. Boniol, A. Burgueño, O. Roux and V. Rosu:
Analysis of slopeparametric hybrid automata. Proc. of HART97,
Lecture Notes in Computer Science 1201, 7580, 1997) is the resolution
(real solutions) of a polynomial system of equalities and inequalities.
This must be done once for every automata and it can be considered as a
preprocessing step and, thus, the computing time it is not important. A
first system sent is the one given by the system of nonlinear inequalities


(1) 
The method used at ONERACERT to deal with this problem (a generalization
of the FourierMotzkin elimination method) provides the description of
a set containing the solutions looked for but also other points not interesting.
In this case the solution is presented in the following way


(2) 
But with the using of specific methods for Quantifier Elimination it is
posible to describe explicitely and exactly the solution set as


(3) 
This solution provides a much more useful information than the previous
solutions when trying to use these automatas to the development of communication
protocols (see P.H. Ho and H. WongToi: Automated analysis of an audio
control protocol. Proc. of CAV95, Lecture Notes in Computer Science
939, 381394, 1995). Next picture shows how the solution set looks like:
In the near future it is planned to integrate FRISCO Software and algorithms
inside the toolboxes designed at the ONERACERT to perform modelchecking
for slopeparametric hybrid automata and Testing for temporized automatas.
This will be used to study an important industrial case: the Philips Communication
Protocol.
Next: Conclusions
Up: The
NonLinear World Previous: The
CANDEMAT case