Journée du 22 Janvier 2010

Rubriques
Travaux en commun
Publications
Info. pratiques
Contacts
Séminaires
Le prochain

22/01/2010

04/12/2009
13/11/2009
02/10/2009
05/06/2009
03/04/2009
06/03/2009
23/01/2009

05/12/2008
14/11/2008
10/10/2008
30/05/2008
11/04/2008
21/03/2008
15/02/2008

Séminaires 2007

Séminaires 2006

Séminaires 2005


mod. 14-Fév-2010

Lieu

CNAM, salle 39.2.64: comment y aller

Programme

14h00-15h00: Zhiwu Li , School of Electro-Mechanical Engineering, Xidan University, "Deadlock Prevention for Flexible Manufacturing Systems: A Novel Petri Net Approach"

transparentsAbstract: Deadlocks are a highly undesirable phenomenon in automated flexible manufacturing systems, whose occurrences may deteriorate the productivity of a system or even lead to catastrophic results. The existing deadlock prevention policies suffer from a number of technical problems: computational complexity, structural complexity, and behavioral permissiveness. This talk presents a novel Petri net approach to design liveness-enforcing Petri net supervisors that are based on the concept of elementary siphons whose number is bounded by the size of a plant model. Deadlock can be prevented by the explicit control of elementary siphons in a Petri net model.

Behavioral permissiveness and computational complexity are also improved through the theory of regions and BDD (Binary Decision Diagrams), respectively. A number of FMS examples are demonstrated the approaches. This talk includes the recent progress in optimal deadlock prevention policies forÊflexible manufacturing systems.

15h00-15h30 : Etienne André, ENS de Cachan, "Synthesis of temporal parameters for the verification of hardware components"

transparentsAbstract: The adjustment of timing bounds is critical in the domain of hardware verification. We present an inverse method allowing to synthesize constraints on timing bounds (seen as parameters) in the framework of timed automata.

We take advantage of a given reference valuation of the parameters for which the system is known to behave properly, and we want to generalize this valuation. Our aim is to generate a constraint such that, under any valuation satisfying this constraint, the traces of the system (viewed as alternating sequences of locations and actions) are equivalent to the traces under the reference valuation. This is useful for safely relaxing some values of the reference valuation.

A tool, IMITATOR, was developed and was successfully applied to various examples of asynchronous circuits and protocols.

15h30-16h00: pause café

16h00-16h30: vie du groupe