To: seminaire@pauillac.inria.fr
From: Bruno.Barras@inria.fr
Subject: SEM - INRIA : LogiCal - 28/06/02 - Paris - FR

      Vous pouvez maintenant vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html


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

                          Vendredi 28 juin, 10h30

                             -----------------
                             Patrick Loiseleur
                             -----------------


              ===============================================
              logiques	temporelles pour les objets distribués
              ===============================================


    Les objets offrent un bon  moyen de gérer la complexité des programmes
    concurrents  et   distribués.  En  ajoutant  des   invariants  et  des
    pré/post-conditions  aux  interfaces   IDL,  on  peut  spécifier  leur
    comportement.

    Dans un précédent exposé, j'ai abordé les techniques qui permettent de
    prouver  qu'une implémentation  objet satisfait  sa  spécification, en
    ré-utilisant au maximum les techniques pour les programmes séquentiels
    (la logique de Hoare).

    La question qui se pose maintenant est: 'comment prouver la correction
    d'un système d'objets en composant  des objets certifiés ?' La réponse
    tient  dans  l'existence  d'une   bisimulation  entre  le  système  de
    transition abstrait - généré par les spécifcationsd des objets - et le
    système   de   transition    concret,   c'est-à-dire   la   sémantique
    opérationelle.   Je   présenterai   deux   théorèmes   de   simulation
    (correspondant  à   deux  niveaux  d'abstraction   différentes)et  les
    conditions suffisantes pour que ça soit des bisimulations.