To: seminaire@pauillac.inria.fr
From: Didier.Remy@inria.fr
Subject: SEM - INRIA : Mosvova - 06/07/01 - 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 6 juillet, 10h30

                                -----------
                                K. Gopinath
                                -----------

                     IISc - Indian Institute of Science

       ==============================================================
       Verification of Highly Available Local Leader Election Service
                       in Timed Asynchronous Systems
       ==============================================================


   Distributed  systems  can be  broadly  characterized  as synchronous  or
   asynchronous.  Synchronous systems involve strict timing constraints and
   bounded failure  frequency assumptions while  asynchronous systems based
   on time-free model do not  involve any timing bounds. Essential services
   like  consensus,  election or  membership  have  been  shown to  be  not
   implementable.  The  Timed Asynchronous  System (TAS) model  of Cristian
   and Fetzer  or the  timed model involves  much simpler  assumptions than
   synchronous model but  still strong enough to serve  as a foundation for
   the construction of dependable applications.

   In this talk, we will study  the verification of the correctness of some
   basic distributed services in TAS.  First, TAS is modelled and then some
   important properties  of two basic  services, FADS (Fail  Aware Datagram
   Service) and HALL (Highly  Available Local Leader Election Service), are
   formally verified.   The PVS  theorem prover is  used for  modelling and
   verification of  the algorithms.   We will then  contrast this  with the
   verification of properties in time-triggered systems.