2000-2001
Groupe de travail
Modélisation, Vérification et Tests des systèmes informatisés
&
Petite école pour la vérification
Le jeudi de 10h45 à 12h
Salle G.T. 2, LaBRI, Rez-de-chaussée
Programme du jeudi 14 juin 2001
- Intervenant: Joaquim ESPELETA( C.P.S. Universidad de Zaragoza)
- Titre :
Deadlock prevention and avoidance for classes of production system
- Resumé:
The talk focuses on the problem of deadlocks in classes of Flexible
Manufacturing Systems (FMS). Usually, a FMS is intended for the
concurrent manufacturing of several types of products. Each raw material
needs to follow a specific sequence of operations in order to obtain the
finished product. In a manufacturing system, each operation (machining,
storage, transportation, etc.) needs the use of one or more "system
resources". By resource we mean a system component able to handle or
transform a material: work-stations, automated guided vehicles, robots,
buffers, storage facilities, tools for machining, pallets, etc. The
concurrent nature of this kind of systems (a set of parts is being
processed at a given time) generates competition relations for the use
of
the system resources that can cause deadlock problems: situations in
which
some parts whose processing started cannot be finished; this parts will
stay (forever) in the system consuming resources and decreasing the
system
performances. In order to deal with deadlock problems, it is necessary
to
characterize such "bad" situations, and then to control the system in
order to ensure that the processing of each part that enters the system
can be executed. These systems are rather complex. Therefore, in order
to
control the use of some formal model is necessary. Among the different
models used for concurrent systems, Petri nets is a family of good
adapted
formalisms. In terms of Petri nets, good behavior can be interpreted as
model liveness: a deadlock situation will imply a non-live Petri net.
The
talk will present a class of nets that appear in the modeling of a wide
class of flexible manufacturing systems. Deadlock problems will be
characterized in terms of structural components of the Petri net model,
and dealock prevention/avoidance control policies will be formulated.
The
aim of such control policies will be constraining the system evolutions
in
order to ensure a live behavior.
Prévisions
Le groupe de travail
MVTsi Prévisions.
MVTsi Propositions.
Réunions précédentes
- 14 juin: Joaquim ESPELETA( C.P.S. Universidad de Zaragoza)
- Titre : Deadlock prevention and avoidance for classes of production system
- 7 juin: Sébastien Grivet (Labri)
- Titre : Dépliages de réseaux de Petri produits symétriques
- 15 mars: Yves DUTUIT (LAP)
- Titre : Autour de la Surêté de Fonctionnement
- 8 mars: Remi MORIN (Institut fuer Algebra Technische
Universitaet Dresden)
- Titre : Sur la verification de specifications en HMSC:
quelques resultats recents.
- 1 mars: Jean-Michel Couvreur (LaBRI)
- Titre: DDD
- 25 janvier: Patricia Bouyer (LSV - ENS de Cachan)
- Titre: Automates temporisés avec assignations
- 18 janvier. Rodolphe Pueyo
- Titre: Formalisation en PVS d'une sémantique pour un
sous-ensemble du langage de spécification de types de données
ASN.1.
- 11 janvier. Patrick Félix (LaBRI)
- Titre: Autour de CALIFE
- 21 décembre. Macha NIKOLSKAIA (LaBRI)
- Titre: Réseaux d'Interaction dans la Bioinformatique
- 14 décembreAnne Dicky (LaBRI)
- Titre: Automates Quantiques
- 23 novembre. Philippe Thomas (LaBRI)
- Titre: Hévéa : Gestionnaire d'arbre de défaillances
couplé à Aralia.
- 9 novembre. François Dufour (LaBRI)
- Titre: Un Point de vue en Automatique
- 26 octobre. André Arnold (LaBRI) dans le cadre de la Petite
école
- Titre: Synthèse de Contrôleur (1 ère partie)
- 19 octobre. Aymeric Vincent (LaBRI)
- Titre: Résolution des jeux de parité par amélioration successive de stratégies.
- 12 octobre. Relâche
- 5 octobre. Réunion de rentrée
-
- Rapide présentation des projets en cours
- Futures voies de recherche
- Préparation du programme du 1er semestre
- Questions diverses
Années précédentes
Navigation
Equipe
Modélisation, Vérification et Test des systèmes informatisés
Contact
K. Musumbu
pour toute information.
Last modified: Thu Sep 27 12:16:25 MEST 2001