[ada-france] MeFoSyLoMa : Séminaire du 27 Avril 2007 à 14h au CNAM salle 11.A3.34

[Jean-François Peyre]

======================================================================
			 Séminaire MeFoSyLoMa
		      http://mefosyloma.cnam.fr

		 Méthodes Formelles pour Les Systèmes
			Logiciels et Matériels

		    Vendredi 27 Mars 2007, 14h-17h
     CEDRIC-CNAM, Salle 11.A3.34, 292 rue St Martin, 75003 PARIS
======================================================================

Le séminaire MeFoSyLoMa est  animé conjointement par  les laboratoires
Cedric (Cnam), IBISC  (Univ.  Evry),  Lamsade (Univ.  Paris-Dauphine),
LIP6 (UPMC), LIPN (Univ. P13), LTCI (Enst). Son objet est de permettre
la confrontation de différentes approches  ou points de vue sur l'uti-
lisation des méthodes formelles dans  les domaines du génie  logiciel,
de la conception  de circuit, des   systèmes répartis ou des  systèmes
d'informations.   Il s'organise  autour  de réunions bimestrielles  où
sont exposés des travaux de recherche récents sur le thème.

La prochaine réunion se déroulera le vendredi 27 Avril 2007 à 14H00
dans les locaux du CNAM, 292 rue Saint Martin, 75003 PARIS,

       salle 11.A3.34.

Vous trouverez un plan d'accès à l'url :

http://www.cnam.fr/home/Infos_pratiques/plan_image.htm


======================================================================
                     Exposés du 27 Avril 2007 :
======================================================================

Gianfranco Ciardo, Department of Computer Science and Engineering
University of California, Riverside

     The Importance of Being Structural (better decision diagram
		 algorithms for asynchronous systems)

Abstract:

   Symbolic algorithms based on binary-decision diagrams (BDDs) are
   routinely employed to verify complex VLSI designs with enormous
   state spaces.  Such methods, however, have initially been applied
   mostly to synchronous circuits, because it has long been believed
   that they are not well suited to the analysis of asynchronous
   systems such as distributed software, Petri nets, and protocols. A
   few years ago, we introduced the Saturation algorithm, which not
   only can cope, but actually benefits from the interleaving behavior
   and locality of events in asynchronous systems.  For such systems,
   Saturation has been shown in practice to have time and memory
   requirements that are several orders of magnitude lower than
   traditional breadth-first symbolic algorithms.

   In this talk, we give a brief survey of the current state-of-the
   art on the use of Saturation in different settings and
   applications, and of the classes of decision diagrams that can be
   used in such settings.  Then, we discuss two specific topics in
   depth.  The first one is a version of Saturation that uses
   edge-valued decision diagrams to compute distance information; this
   is useful to generate minimum-length witnesses in symbolic model
   checking, or to perform a bounded version of symbolic model
   checking.  The second one is the use of structural information to
   heuristically derive a good static order for the decision diagram
   variables of arbitrary asynchronous systems and, in particular, of
   Petri nets.

---------------------------------------------------------------------

Arnaud Sangnier, PhD student at LSV ENS Cachan

     From Time Petri Nets to Timed Automata: an Untimed Approach

Abstract:

   Time Petri Nets (TPN) and Timed Automata (TA) are widely-used
   formalisms for the modeling and analysis of timed systems.  A
   recently-developed approach for the analysis of TPNs concerns their
   translation to TAs, at which point efficient analysis tools for TAs
   can then be applied. One feature of much of this previous work has
   been the use of timed reachability analysis on the TPN in order to
   construct the TA. We present a method for the translation from TPNs
   to TAs which bypasses the timed reachability analysis step.
   Instead, our method relies on the reachability graph of the
   underlying untimed Petri net. We show that our approach is
   competitive for the translation of a wide class of TPNs to TAs in
   comparison with previous approaches, both with regard to the time
   required to perform the translation, and with regard to the number
   of locations and clocks of the produced TA.


=====================================================================
La prochaine réunion MeFoSyLoMa est fixée le :
   - 08 Juin 2007 au LIPN (Univ. Paris Nord) -
======================================================================

======================================================================
Jean-François Pradat-Peyre  Laboratoire Cedric
Tel: 01 40 27 26 06         Conservatoire National des Arts et Métiers
Fax: 01 40 27 28 45         2 rue Conté, 75003 PARIS, FRANCE

       http://quasar.cnam.fr
======================================================================