Newsgroups: fr.announce.seminaires
Distribution: fr
To: fr-sem@frmug.org
From: Didier.Remy@inria.COUPER-CECI.fr
Organization: INRIA-Rocquencourt
Subject: SEM - INRIA : Coq - 1/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 1 octobre, 10h30

                                -----------
                                César Munoz
                                -----------

                             ICASE-NASA Langley

              ===============================================
              Structural Embedding: Mechanization with Method
              ===============================================

                    (Joint work with John Rushby (SRI))

   The  most  powerful  tools for analysis    of formal specifications  are
   general-purpose theorem provers and   model  checkers, but these   tools
   provide scant methodological support.  Conversely, those approaches that
   do   provide a well-developed    method   generally have  less  powerful
   automation.    It  is   natural,   therefore, to  try    to combine  the
   better-developed methods  with the more powerful  general-purpose tools.
   An obstacle   is  that the  methods   and the tools    often employ very
   different logics.

   We argue that  methods are separable  from their logics  and are largely
   concerned   with the structure  and  organization of specifications.  We
   propose a technique    called  structural  embedding that  allows    the
   structural elements  of a method to   be supported by  a general-purpose
   tool, while substituting the logic  of the tool for  that of the method.
   We  have   found this technique   quite  effective and we   provide some
   examples  of   its application.   We    also suggest how general-purpose
   systems could be restructured to support this activity better.