*******************************************************************
*                   LIENS Ecole Normale Superieure                *
*                                                                 *
*                          Groupe de travail                      *
*              'Semantique et Interpretation Abstraite'           *
*                             P. Cousot                           *
*                                                                 *
*                        Vendredi, 10h--12h                       *
*                    Jean-Louis Verdier, passage vert             *
*                 ou  Salle Henri Cartan B, etage -2              *
*                   DMI ENS 45 rue d'Ulm 75005 Paris              *
*******************************************************************

*** Vendredi 2 avril 1993 *** Seminaire *** SALLE Henri Cartan B ***

"Model-checking" et syste`mes temps re'e'l.

Philippe Granger (LIENS)

Resume: Le "model-checking" est une technique de ve'rification des
circuits e'lectroniques et des protocoles de communication.
Pre'cisement, elle consiste a` ve'rifier qu'un syste`me de transitions 
a` nombre fini d'e'tats (repre'sentant un circuit ou un protocole)
satisfait une formule de logique temporelle fournie par l'utilisateur.
Cette technique a e'te' developpe'e inde'pendamment par Clarke et Emerson,
et Sifakis et Queille, au de'but des anne'es 80.

Dans un premier temps, on pre'sentera dans le de'tail l'algorithme
classique de "model-checking", ainsi que les diffe'rentes techniques
associe'es permettant de contrer l'explosion combinatoire susceptible
d'intervenir lors du calcul (emploi de BDD--diagrammes boole'ens de
de'cision, abstractions).

Puis on en de'crira l'extension a` des syste`mes temps re'e'l 
(c'est-a`-dire a` des syste`mes de transitions e'tiquetes par des 
contraintes temporelles sur des variables d'horloge), ainsi que notre 
recherche en cours sur ce sujet (re'alise'e conjointement avec Ed 
Clarke a` CMU).

*******************************************************************