Conclusions  The Non-Linear World  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

 

$$\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}$$ (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

$$\matrix{a_1 &=& 0\cra_2 &\geq& 0\crt &\geq& 40\crk &\leq& 1\cr}$$ (2)

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

$$\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.$$ (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:

$\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.