********************************************************************* * 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 * ********************************************************************* Bonne anne'e a tous. *** Vendredi 8 janvier 1999 **** 14h00 ****************************** relache. *** Vendredi 15 janvier 1999 **** 14h00 ***************************** Semantique Equationnelle Loic CORRENSON (INRIA Rocquencourt) Re'sume' : Les transformations classiques de programmes fonctionnels s'appuient fortement sur leur semantique, operationnelle ou denotationnelle. Nous nous interessons particulierement a la deforestation, operation qui consiste a simplifier la composition de deux fonctions. En effet, si f et g sont compos'ees, la construction du resultat intermediaire construit par f et consomme' par g peut parfois etre evit'ee. Nous avons compare' les methodes de deforestation fonctionnelles et celles des Grammaires Attribuees. Si les secondes semblent plus puissantes que les premieres, leur pouvoir d'expression est cependant plus limite' que celui d'un language fonctionnel. En cherchant a rapprocher les deux formalismes et les deux methodes, nous avons defini une nouvelle maniere de coder un programme fonctionnel, a l'aide de systemes d'equations. Ce formalisme, appele' Semantique Equationnelle, est tres largement inspire' de la technologie des grammaires attribuees. C'est un language au meme titre que le lambda calcul, avec sa propre semantique, qui permet de definir des methodes de deforestation et d'evaluation partielle particulierement puissantes. *** Vendredi 22 janvier 1999 **** 14h00 ***************************** entations des activites Java Embarquees a l'Open Group Research Institute de Grenoble Vania JOLOBOFF (Open Group Research Institute de Grenoble) Re'sume' : L'Open Group Research Institute est un institut de recherche et developpement en logiciel fonctionnant avec des financements prives. Cet expose presentera une partie des activites du laboratoire de Grenoble (http://www.gr.opengroup.org/), a savoir les projets axes sur l'utilisation de code mobile Java pour les applications industrielles embarquees telles que la telephonie, les agendas electroniques, les fax et imprimantes, le controle de processus industriel, etc. Il ne s'agit pas d'une presentation formelle sur un point theorique particulier, mais de montrer quelques exemples d'applications dans un contexte industriel de resultats de recherche et de soulever les questions posees par les problemes nouveaux auxquels on s'adresse. Dans un premier temps on presente la problematique industrielle et economique qui impose les contraintes technologiques que l'on cherche a resoudre, ce qui entraine les choix faits dans la conception des logiciels presentes par la suite. On illustrera ces choix par la presentation de quelques exemples tires de plusieurs projets. Les problemes abordes en exemple s'articulent tous autour des techniques de compilation utilisees, soit pour du code mobile telecharge dans des appareils a faible capacite memoire, soit de code charge dans l'appareil des sa mise en vente. *** Jeudi 28 janvier 1999 ******************************************* ANALYSE STATIQUE DE LOGICIELS Du test exhaustif a la verification automatique voir *** Vendredi 29 janvier 1999 **** 14h00 ***************************** Test automatique de programmes reactifs Nicolas HALBWACHS (VERIMAG, Grenoble) Re'sume' : Nous nous interessons aux programmes reactifs dont la verification formelle est difficile, et pour lesquels le test reste une technique de validation particulierement importante. C'est le cas, en particulier, - des programmes presentant des aspects numeriques importants - des programmes dont le code source n'est pas completement disponible, ou qui sont implantes manuellement, par exemple sur des architectures distribuees. Notre approche consiste a utiliser des observateurs synchrones, deja mis en oeuvre dans les methodes de verification, pour decrire - le comportement attendu du programme, pour permettre le diagnostic du test ("oracle") - les proprietes connues de l'environnement, afin d'eviter la production de jeux de test irrealistes - les objectifs de test, par lesquels l'utilisateur peut guider la production des jeux de test. Nous developpons un outil de test, qui utilise des observateurs ecrits dans le langage synchrone Lustre: l'outil produit automatiquement des sequences de test realistes, et effectue le test en "boite noire" et son diagnostic. Le generateur de jeux de test utilise des BDDs pour les aspects logiques, et des polyedres convexes pour les aspects numeriques. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr WWW: http://www.dmi.ens.fr/~cousot/annonceseminaire.html *********************************************************************