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

    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: Fri Jun 8 10:45:17 MEST 2001