********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h--16h * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 25 mars 1994 ***************************** relache ***** *** Vendredi 1er avril 1994 ***************************************** Les Syste`mes hybrides - Une approche informatique Joseph SIFAKIS (VERIMAG, Grenoble) Re'sume' : Les syste`mes hybrides sont des syste`mes ayant des composantes discre`tes et continues. Un syste`me de commande temps re'el avec son environnement continu peut e^tre conside're' comme un syste`me hybride ; il doit produire des re'ponses temps-re'el a` des stimuli qui changent de fac,on continue. Le the`me des syste`mes hybrides devient tre`s actif en Informatique car des travaux re'cents montrent que des re'sultats et techniques utilise's pour la ve'rification et la spe'cification des syste`mes re'actifs et des programmes en ge'ne'ral peuvent e^tre adapte's aux syste`mes hybrides. Les re'sultats pre'sente's concernent deux directions de recherche comple'mentaires de'veloppe'es dans le projet Spectre : -- La de'finition d'un mode`le pour les syste`mes hybrides dont la se'mantique est exprime'e en termes de syste`mes de transitions. Nous discuterons quelques questions importantes pour la de'finition de ce mode`le et plus particulie`rement les proble`mes de l'interaction entre e'volution continue et changements discrets, de la composition des syste`mes hybrides et de la de'finition d'e'quivalences comportementales approprie'es. -- L'e'tude de me'thodes de ve'rification permettant la comparaison d'un syste`me hybride a` des proprie'te's de'crites d'habitude par des formules d'une logique temporelle. Deux approches importantes sont de'crites: - La premie`re cherche a` identifier des sous-classes de syste`mes hybrides pour lesquelles certaines proprie'te's sont de'cidables. Les re'sultats existants concernent des sous-classes simples comme les automates temporise's et les graphes d'inte'grateurs pour lesquelles des me'thodes de ve'rification et des outils associe's sont de'ja` disponibles. - La seconde cherche a` appliquer des me'thodes d'analyse ge'ne'rales se'mi-de'cidables. Ces me'thodes actuellement en e'tude, peuvent e^tre automatise'es et comprennent des techniques d'analyse approche'e et d'interpre'tation abstraite. *** Vendredi 8 avril 1994 ******************************************* Raffinement de programmes \'equitables \`a partir du raffinement d'actions Dominique ME'RY (CRIN-CNRS & INRIA Lorraine) Re'sume' : Les travaux de Back et de la communaut\'e travaillant sur les transformateurs de pr\'edicats ont montr\'e que le raffinement des actions s'apparente \`a une relation de d\'eduction au sens g\'en\'eral. Comme cette approche repose essentiellement sur la d\'efinition d'une s\'emantique fond\'ee sur les transformateurs de pr\'edicats, son extension \`a des classes de programmes plus exotiques passe par l'\'etude des transformateurs dans le cas de cette classe de programmes. Ce travail repose sur deux transformateurs de pr\'edicats assez anciens mais dont les propri\'et\'es li\'ees \`a l'objectif du raffinement ont permis de mettre en \'evidence des transformations ou des lois de raffinement pour des programmes \'equitables. L'expos\'e s'attachera \`a pr\'esenter la relation de raffinement pour le cas de programmes justes et pour le cas de programmes \'equitables. Ces r\'esultats permettent d'\'etendre le calcul de Morgan, afin de raffiner des programmes justes ou \'equitables \`a partir de sp\'ecifications de la forme pre-post. Ce travail montre aussi que le raffinement de programmes justes ou \'equitables doit maintenir ou assurer la correction des programmes propri\'et\'es d'invariance et de fatalit\'e. Le raffinement selon les transformateurs de pr\'edicats peut alors \^etre caract\'eris\'e comme une relation maintenant les propri\'et\'es d\'ej\`a d\'emontr\'ees dans un syst\`eme de preuves {\it ad hoc \/} et reposant sur les transformateurs. Quelques applications seront donn\'ees et un cadre plus g\'en\'eral pour le raffinement sera esquiss\'e. *** Vendredi 15 avril 1994 ****************************************** Analyse interprocedurale d'alias existentiels; alias universels et logique temporelle Alain DEUTSCH (INRIA, Rocquencourt) Re'sume' : Cet expose fait suite a nos travaux precedents sur l'analyse d'alias pour langages a donnees structurees et pointeurs, et aux travaux recents de M. Burke, L. Hendren et W. Landi. Nous presenterons trois algorithmes interproceduraux d'analyse d'alias existentiels: un algorithme global, un algorithme modulaire, un algorithme semi-modulaire. Nous comparons la puissance respective de ces methodes ainsi que leur complexite. Des resultats experimentaux indiquent que la methode semi-modulaire est en pratique preferable. Nous evoquerons les relations entre analyse semi-modulaire et inference de types. L'analyse d'alias universels pour pointeurs simples ou passage par reference est un probleme resolu: il existe des algorithmes precis et polynomiaux. Par contre, l'analyse d'alias universels avec pointeurs a plusieurs niveaux est un probleme ouvert, qui n'est pas directement le dual de l'analyse existentielle. Nous presentons d'une part une formalisation semantique (en logique temporelle), et d'autre part une methode d'analyse d'alias universels. *** Vendredi 22 avril 1994 ***************************** Relache **** *********************************************************************