next up previous contents
Next: Conclusions Up: The Non-Linear World Previous: The CANDEMAT case

The ONERA-CERT case

Communicated by A. Burgueño and ellaborated by L. Gonzalez-Vega and N. Gonzalez-Campos
 
 

The ONERA-CERT (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 slope-parametric hybrid automata (see F. Boniol, A. Burgueño, O. Roux and V. Rosu: Analysis of slope-parametric hybrid automata. Proc. of HART-97, Lecture Notes in Computer Science 1201, 75-80, 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 non-linear inequalities

 
 \begin{displaymath}\matrix{0&\leq& a_1\cr0&\leq& a_2\cr0&\leq& t\cr40&\l... ...,k&\leq& t\,(1-k)-a_2\cr30\,k-30&\leq& a_2\,k+t\,k(k-1)\cr}\end{displaymath} (1)
The method used at ONERA-CERT to deal with this problem (a generalization of the Fourier-Motzkin 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
\begin{displaymath}\matrix{a_1 &=& 0\cra_2 &\geq& 0\crt &\geq& 40\crk &\leq& 1\cr}\end{displaymath} (2)
But with the using of specific methods for Quantifier Elimination it is posible to describe explicitely and exactly the solution set as
\begin{displaymath}\left\{\matrix{a_1=0\hfill\cr0\leq k\leq3/4\hfill\crt\geq... ...\hfill\crk=1\hfill\crt\geq 40\hfill\cra_2=0\hfill\cr}\right.\end{displaymath} (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. Wong-Toi: Automated analysis of an audio control protocol. Proc. of CAV-95, Lecture Notes in Computer Science 939, 381-394, 1995). Next picture shows how the solution set looks like:

\psfig {figure=aufinal.ps,height=11cm,width=12cm}$\qquad\qquad$
In the near future it is planned to integrate FRISCO Software and algorithms inside the toolboxes designed at the ONERA-CERT to perform model-checking for slope-parametric hybrid automata and Testing for temporized automatas. This will be used to study an important industrial case: the Philips Communication Protocol.


next up previous contents
Next: Conclusions Up: The Non-Linear World Previous: The CANDEMAT case