Séminaires
Séminaire du 24 Mars 2006
Lieu
Programme
14h00-15h00: harles 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.
15h00-15h30 : 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.