[cedric] Sémainaire MeFoSyLoMa , journée du 24 Mars 2006

Veuillez excuser les réceptions multiples.


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

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

		    Vendredi 24 Mars 2006, 14h-17h
	   CEDRIC-CNAM, Salle 30 -1 03, 2 rue Conté, 75003 PARIS
======================================================================

Le séminaire MeFoSyLoMa  est animé conjointement par  les laboratoires
Cedric (Cnam), Lamsade (Univ. P9), Lip6 (UPMC), LIPN (Univ. P13), LTCI
(Enst). Son objet  est  de  permettre la confrontation  de  différents
approches  ou  points de  vu sur  l'utilisation 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.

L'originalité  de ce séminaire  réside dans  son choix  délibéré de ne
présenter   que des  travaux    provenant  ou impactant    directement
l'application de méthodes et d'outils  de conception ou d'analyse  sur
des exemples réels ou des études de cas significatives.

Par   cette approche, il  favorise   les échanges entre les différents
acteurs du domaine   et fournit l'opportunité aux  participants  moins
familiers des méthodes  formelles mais intéressés par l'application de
celles-ci de suivre les évolutions scientifiques du domaine.

La prochaine réunion se déroulera le vendredi 24 Mars 2006 à 14H00
dans les locaux du CNAM, 2 rue Conté, 75003 PARIS, en 30 -1 03
Vous trouverez un plan d'accès à l'url :

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


======================================================================
                     Exposés du 24 Mars 2006 :
======================================================================
Charles Lakos, University of Adelaide (Australia)

  "A Petri Net formalism for modelling and analysing mobile systems"

Abstract:

   Mobile systems explore the interplay between locality and
   connectivity.  A subsystem may have a connection to a remote
   subsystem and use this for communication. Alternatively, it may be
   necessary or desirable to move the subsystem close to the other in
   order to communicate. This talk presents a Petri Net formalisation
   of mobile systems so as to harness the intuitive graphical
   representation of Petri Nets and the long history of associated
   analysis techniques.

   The proposed formalism starts with modular Petri Nets, where a net
   is divided into modules which can interact via place and transition
   fusion. The first change is that the flat module structure is
   replaced by fully nested modules, called locations.  The nesting of
   locations provides a notion of locality while their fusion context
   determines their connectivity. The transitions constituting a
   location are constrained so that we can determine when a location
   is occupied by a subsystem, and when the subsystem shifts from one
   location to another.

   The above form of mobile systems has a number of parallels with
   object based systems.  Both these kinds of systems present
   particular challenges for state space exploration.  Objects can be
   dynamically created and discarded, and can be referenced via object
   identifiers. Consistent relabelling of object identifiers in a
   state leads to a state that is superficially different but
   behaviourally equivalent to the original. Similarly, object-based
   systems can include garbage which has no effect on subsequent
   behaviour but which results in unnecessary differentiation of
   states. Both of these factors can lead to state space explosion.

   This talk considers state space exploration for object-based
   systems based on the Petri Net formalism. It addresses the above
   issues by using both equivalence reduction and the sweep-line
   technique. Experimental results are presented for a simple case
   study of a communication protocol.


----------------------------------------------------------------------
Cecile Braunstein, UPMC/LIP6/ASIM

  "Abstraction de composants matériels par leur spécification en
   formule CTL"

Abstract:

   This talk present an incremental approach to design flow-control
   oriented hardware devices described by Moore machines.  The method
   is based on successive additions of new behaviours to a simple
   device in order to build a more complex one.  The new behaviours
   added must not override the previous ones.  A set of CTL formulae
   is assigned to each step of the design. The links between the
   formulae of two consecutive design steps are formalized as a set of
   formula-transformations F, stating that: for all CTL formula f with
   atomic propositions related to step i, f is satisfied on a design
   at step i, iff F(f) is satisfied on the design extended at step
   i+1.  This result extends the classical CTL property preservation
   results in a particular context. Moreover, it simplifies the
   writing of properties for a new device. This approach has been
   applied in the design of bus protocol converters. Finaly this talk
   show how the transformations were useful to perform non-regression
   analysis.


----------------------------------------------------------------------
Discusssions

   Point sur la préparation de FORTE'06
   Point sur le livre MeFoSyLoMa

==============================================================================
La prochaine réunion MeFoSyLoMa est fixée le :
   - 12 Mai 2006 (LIPN)
==============================================================================

======================================================================
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
======================================================================

_______________________________________________
Site WWW de l'association Ada-France: http://www.ada-france.org/
[email protected]
http://www.ada-france.org/mailman/listinfo/ada-france