Newsgroups: fr.announce.seminaires
Distribution: fr
To: fr-sem@frmug.org
From: Nelly.Maloisel@inria.COUPER-CECI.fr
Organization: INRIA-Rocquencourt
Subject: SEM - INRIA : Coq - 15/10/99 - Paris - FR

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E
       ____               ____                             ___                
      /    _   _         /     __     __  /_  _   /       /   |  _   __   _   
     /    / \ / \  ___  /     /  | / /_  /   __| /  ___  /___/  __| /  | __|  
    |___  |_/ |_/      |____ /    / __/ |_  |_/ |_      /      |_/ /    |_/   
               /                                                              
              /                                                               
                          I N R I A - Rocquencourt, 
                       Salle de conference du Bat 11

                         Vendredi 15 octobre, 13h30

                              ---------------
                              Cornes Cristina
                              ---------------

                     Instituto de Computacion, Uruguay

                ============================================
                Théorie des types et Vérification de modèles
                ============================================

 En 1998 le projet Coq de l'INRIA et le groupe de Méthodes Formelles de 
l'Instituto de Computacion a Montevideo ont soumis un projet de 
collaboration scientifique (pour 2 ans) à l'Ambassade de France en Uruguay.
Le sujet du projet porte sur l'intégration de la Théorie des types 
et la Vérification de modèles pour la vérification de systèmes réactifs.
Dans cette exposé nous allons faire le rapport de l'état d'avancement de ce
projet. En particulier nous parlerons des activités suivantes qui sont en 
train d'être développées dans ce cadre:

-  Vérification de systèmes de temps réel en Théorie de types
   Cas d'étude: passage à niveau d'un train 

-  Vérification d'un stimulateur cardiaque avec le système Kronos

-  Vérification du code source C d'un stimulateur cardiaque avec le système
   Coq.

 La vérification du stimulateur cardiaque est faite en collaboration avec
l'entreprise Centro de Construccion de Cardioestimuladores del Uruguay. Cette
entreprise exporte des stimulateurs cardiaques et elle nous a fourni le 
code source C du stimulateur ainsi que la spécification à vérifier 
formellement.