********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 5 fevrier 1999 **** 14h00 ****************************** relache *** Vendredi 12 fevrier 1999 **** 14h00 ***************************** relache *** Vendredi 19 fevrier 1999 **** 14h00 ***************************** vacances *** Vendredi 26 fevrier 1999 **** 14h00 ***************************** Animation et analyse de specifications temporelles a l'aide de l'interpretation abstraite Dominique CANSELL & Dominique MERY (LORIA, Nancy) Re'sume' : Ce travail, developpe au sein de l'equipe MODEL du LORIA, s'inscrit dans le cadre du developpement d'outils pour le langage TLA+ de Leslie Lamport. Une animation d'une specification est obtenue en construisant des traces de predicats qui satisfont la specification et que l'utilisateur peut parcourir a sa guise. L'interpretation abstraite nous permet de passer d'un monde concret a un monde abstrait (en general fini). Nous l'avons utiliser pour une meilleure animation de specifications TLA+. Avec l'interpretation abstraite nous construisons des traces de predicats abstraits ce qui permet de regrouper un certain nombre de predicats (successeurs dans la trace) et en general si l'abstraction et bien choisie, nous pouvons construire un graphe fini de predicats abstrait pour representer l'ensemble des animations d'une specification. Ce graphe permet de prouver et de decouvrir des invariants. L'animateur a ete entierement ecrit a l'aide du Logic-Solver le langage de theories de l'Atelier B. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr WWW: http://www.dmi.ens.fr/~cousot/annonceseminaire.html *********************************************************************