Séminaires
Séminaire du 22 Janvier 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"
Abstract: 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"
Abstract: 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.