Parcours À quoi ça sert

Topic outline

• Select topic General

  General

  Collapse all Expand all
  • Select activity gardons contact

    Gardons contact : vos questions pendant la formation

  • Select activity Annonces

    

    Annonces Forum
• Select topic Chapitre 7 : Méthodologie de construction

  Chapitre 7 : Méthodologie de construction
  • Select activity Introduction

    Ce chapitre 7 présente une méthodologie de modélisation adaptée aux SED.
    Pour suivre les séquences, vous pouvez vous appuyer sur le support : MTH_MM.pdf.

    
    

    
    

  • Select activity Équipe pédagogique

    Équipe pédagogique

    Contributeurs : Pascal Berruet, Gregory Faraut, Euriell Le Corronc, Pascale Marangé
    Intervenant.e.s :  Pascal Berruet, Gregory Faraut, Euriell Le Corronc
    

  • Select activity Introduction

    Completion

    Students must

    

    Mark as done

    Introduction

    
    

  • Select activity Qu'est-ce qu'un modèle ?

    Completion

    Students must

    

    Mark as done

    Qu'est-ce qu'un modèle ?

    
    

  • Select activity Méthodologie de construction d'un modèle

    Completion

    Students must

    

    Mark as done

    Méthodologie de construction d'un modèle

    
    

  • Select activity Vision globale du système

    Completion

    Students must

    

    Mark as done

    Vision globale du système

    
    

  • Select activity Vision comportementale du système

    Completion

    Students must

    

    Mark as done

    Vision comportementale du système

    
    

  • Select activity Illustration de cette méthodologie par un exemple

    Completion

    Students must

    

    Mark as done

    Illustration de cette méthodologie par un exemple

    
    

  • Select activity Quelques remarques pour conclure cette méthodologie

    Completion

    Students must

    

    Mark as done

    Quelques remarques pour conclure cette méthodologie

    
    

  • Select activity Conclusion sur la méthodologie

    Completion

    Students must

    

    Mark as done

    Conclusion sur la méthodologie

    
    

  • Select activity Différents besoins de modélisation

    Completion

    Students must

    

    Mark as done

    Différents besoins de modélisation

    
    

  • Select activity Quel modèle pour quel système et quel objectif ?

    Completion

    Students must

    

    Mark as done

    Quel modèle pour quel système et quel objectif ?

    
    

  • Select activity Conclusion

    Completion

    Students must

    

    Mark as done

    Conclusion

    
    

  • Select activity Pour aller plus loin

    Pour aller plus loin
    

    Pour aller plus loin, vous pouvez regarder les modélisations sont faites dans le cas du contrôle-commande via le chapitre 8, de la vérification avec le chapitre 9 et du  diagnostic via le chapitre 10.
    

  • Select activity Pour revenir en arrière

    Pour revenir en arrière
    

    Si les notions d'automates ne sont pas claires, vous pouvez suivre le chapitre 2 ou si les notions de réseaux de Petri ne sont pas claires, vous pouvez suivre le chapitre 3. Si les notions d'événements ou d'états ne sont pas claires, vous pouvez suivre le chapitre 1.
    

• Select topic Chapitre 8 : Utilisation des SED pour la vérification

  Chapitre 8 : Utilisation des SED pour la vérification
  • Select activity Introduction

    Ce chapitre 8 présente l'utilisation des SED dans le cadre de la vérification formelle.
    La vérification est une méthode qui permet de vérifier si une spécification est respectée par un modèle.
    Pour suivre les séquences, vous pouvez vous appuyer sur le support : UTL_Verif.pdf

    
    

    
    

  • Select activity Équipe pédagogique

    Équipe pédagogique

    Contributeurs : Pascale Marangé, Alexandre Philippot et Olivier H. Roux
    Intervenante :  Pascale Marangé
    

  • Select activity Motivations pour faire de la vérification formelle

    Completion

    Students must

    

    Mark as done

    Motivations pour faire de la vérification formelle

    
    

  • Select activity Vérification formelle par model-checking

    Completion

    Students must

    

    Mark as done

    Vérification formelle par model-checking

    
    

  • Select activity Modélisation des propriétés

    Completion

    Students must

    

    Mark as done

    Modélisation des propriétés

    
    

  • Select activity Mise en application

    Mise en application
     
    A vous de mettre en application ce que vous venez d'apprendre sur un exemple en utilisant
    

    • le support : UTL_Verif.pdf, 
    • le logiciel ** UPPAAL **  https://uppaal.org/downloads/ - En version 4.1, 
    • les modèles : FRM_AT.zip et 
    • la vidéo :
      

    
    

    
    
  • Select activity Références

    Références
    

    Clarke E. et al (1994). Model checking and abstraction. ACM-TOPLAS,
    vol. 16, no 5.
    G. Behrmann, J. Bengtsson, A. David, K. Larsen, P. Petterson et Wang Yi.
    (2002) UPPAAL Implementation Secrets . Proc. FTRTFT 2002, Springer LNCS
    2469, pp. 3-22

  • Select activity Pour aller plus loin

    Pour aller plus loin
    

    Pour aller plus loin, vous pouvez regarder la présentation du diagnostic via le chapitre 10.
    

  • Select activity Pour revenir en arrière

    Pour revenir en arrière
    

    Si les notions d'automates temporisés ne sont pas claires, vous pouvez suivre les vidéos FRM_Motivation_AjoutTemps.mp4 et FRM_Aut_T_ModelisationTemps.mp4.
    

• Select topic Chapitre 9 : Utilisation des SED pour le contrôle commande

  Chapitre 9 : Utilisation des SED pour le contrôle commande
  • Select activity Introduction

    Ce chapitre 9 présente l'utilisation des SED dans le cadre du contrôle-commande.
    Le contrôle-commande est une méthode qui permet de contraindre un modèle pour qu'il respecte une spécification. 
    Quatre approches de contrôle commande sont présentées dans ce chapitre :
    

    • la théorie du contrôle des systèmes maxplus, 
    • la synthèse de contrôleur par réseaux de Petri, 
    • la théorie de la commande par supervision avec les automates à états, 
    • la synthèse algébrique via l'algèbre de Boole.
      

    Pour suivre la séquence d'introduction de ce chapitre, vous pouvez vous appuyer sur le support : UTL_CTRL_Intro.pdf.

    
    

    
    

  • Select activity Équipe pédagogique

    Équipe pédagogique

    Intervenante :  Euriell Le Corronc
    

  • Select activity Introduction au contrôle commande

    Completion

    Students must

    

    Mark as done

    Introduction au contrôle commande

    
    

  • Select activity Introduction

    La théorie du contrôle des systèmes maxplus :

    
    

    L'objectif de contrôle-commande des SED peut être atteint en utilisant la théorie du contrôle des systèmes maxplus.
    Pour suivre les séquences, vous pouvez vous appuyer sur le support : UTL_CTRL_MaxP.pdf.

    
    

    
    

  • Select activity Équipe pédagogique

    Équipe pédagogique

    Contributeurs : Bertrand Cottenceau, Guilherme Espindola-Winck, Mehdi Lhommeau, Sébastien Lahaye, Claude Martinez
    Intervenant :  Guilherme Espindola-Winck
    

  • Select activity Commande en juste-à-temps

    Completion

    Students must

    

    Mark as done

    Commande en juste-à-temps

    
    

  • Select activity Commande en boucle fermée

    Completion

    Students must

    

    Mark as done

    Commande en boucle fermée

    
    

  • Select activity Poursuite de modèle - retour d'état

    Completion

    Students must

    

    Mark as done

    Poursuite de modèle - retour d'état

    
    

  • Select activity Conclusion

    Completion

    Students must

    

    Mark as done

    Conclusion

    
    

  • Select activity Mise en application

    Mise en application
     
    A vous de mettre en application ce que vous venez d'apprendre en utilisant
    

    • le logiciel  ** Script MinMaxGDJS ** https://perso-laris.univ-angers.fr/~lhommeau/minmaxgd.html et 
    • le lien : UTL_CTRL_Maxplus.txt
  • Select activity Pour aller plus loin

    Pour aller plus loin
    

    Prochaines éditions des écoles SED ...
    

  • Select activity Pour revenir en arrière

    Pour revenir en arrière
    

    Si les notions sur l'algèbre maxplus ne sont pas claires, vous pouvez suivre les vidéos : FRM_MaxP_ConceptsBase.mp4 et FRM_MaxP_SystemesMaxP.mp4. Si vous voulez revoir l'introduction à la commande des systèmes maxplus : FRM_MaxP_IntroCommande.mp4
    

  • Select activity Introduction

    La synthèse de contrôleur par réseaux de Petri :

    
    

    L'objectif de contrôle-commande des SED peut être atteint en utilisant les réseaux de Petri.
    Pour suivre les séquences, vous pouvez vous appuyer sur le support : UTL_CTRL_RdP.pdf.

    
    

    
    

  • Select activity Équipe pédagogique

    Équipe pédagogique

    Contributeurs :  Isabel Demongodin et Olivier H. Roux
    Intervenant :  Isabel Demongodin
    

  • Select activity Illustration 1/2

    Completion

    Students must

    

    Mark as done

    Illustration 1/2

    
    

  • Select activity Illustration 2/2

    Completion

    Students must

    

    Mark as done

    Illustration 2/2

    
    

  • Select activity Mise en application

    Mise en application
    
    A vous de mettre en application ce que vous venez d'apprendre sur un exemple en utilisant la vidéo :
    
    

    
    
  • Select activity Références

    Références
    

    Yamalidou, K., Moody, J., Lemmon, M., and Antsaklis, P. (1996).
    Feedback control of Petri nets based on place invariants.
    Automatica, 32(1) :15–28.

  • Select activity Pour aller plus loin

    Pour aller plus loin
    

    Prochaines éditions des écoles SED ...
    

  • Select activity Pour revenir en arrière

    Pour revenir en arrière
    

    Si les notions de réseau de Petri ne sont pas claires, vous pouvez suivre les vidéos : FRM_RdP_StructureStatique.mp4, FRM_RdP_StructureDynamique.mp4, FRM_RdP_Constructions.mp4 et FRM_RdP_EquationsEtat.mp4
    

  • Select activity Introduction

    La théorie de la commande par supervision avec les automates à états :

    
    

    L'objectif de contrôle-commande des SED peut être atteint en utilisant la théorie de la commande supervisée et les automates à états.
    Pour suivre les séquences, vous pouvez vous appuyer sur le support : UTL_CTRL_CS.pdf

    
    

    
    

  • Select activity Équipe pédagogique

    Équipe pédagogique

    Contributeurs :  Pascale Marangé, Alexandre Philippot, Laurent Piétrac
    Intervenants :  Laurent Piétrac, Alexandre Philippot
    

  • Select activity Théorie du contrôle par supervision - Introduction

    Completion

    Students must

    

    Mark as done

    Théorie du contrôle par supervision - Introduction

    
    

  • Select activity Modèles

    Completion

    Students must

    

    Mark as done

    Modèles

    
    

  • Select activity Propriétés utilisées

    Completion

    Students must

    

    Mark as done

    Propriétés utilisées

    
    

  • Select activity Problème 1 : existe-t-il un procédé sous contrôle ?

    Completion

    Students must

    

    Mark as done

    Problème 1 : existe-t-il un procédé sous contrôle ?

    
    

  • Select activity Exemple

    Completion

    Students must

    

    Mark as done

    Exemple

    
    

  • Select activity Problème 2 : ce procédé sous contrôle existe-t-il ?

    Completion

    Students must

    

    Mark as done

    Problème 2 : ce procédé sous contrôle existe-t-il ?

    
    

  • Select activity Mise en application

    Mise en application
     
    A vous de mettre en application ce que vous venez d'apprendre sur un exemple en utilisant
    

    • le support : UTL_CTRL_CS.pdf, 
    • le logiciel** SUPREMICA ** Lien de téléchargement , 
    • les modèles : UTL_CTRL_CS.zip et 
    • la vidéo :
      

    
    

    
    

    
    
  • Select activity Références

    Références
    

    Benoît Caillaud et al., éd. Synthesis and control of discrete event systems.
    Kluwer Academic Publishers, 2010.
    [2] Christos G Cassandras et Stéphane Lafortune.
    Introduction to Discrete Event Systems. Springer, 2008.
    [3] W. Murray Wonham et Kai Cai. « Supervisory control of discrete-event
    systems ». notes de cours, departement of Electrical and Computer
    Engineering, University of Toronto. 2018. url :
    https://www.researchgate.net/publication/319434005_Supervisory_Control_of_Discrete-Event_Systems_v20170901

  • Select activity Pour aller plus loin

    Pour aller plus loin
    

    Prochaines éditions des écoles SED ...
    

  • Select activity Pour revenir en arrière

    Pour revenir en arrière
    

    Si les notions d'automates à états et langages ne sont pas claires, vous pouvez suivre les vidéos : FRM_Aut_AutomatesAEtats.mp4 et  FRM_Aut_AutLangages.mp4 et FRM_Aut_AutOperations.mp4.
    

  • Select activity Introduction

    La synthèse algébrique via l'algèbre de Boole :

    
    

    L'objectif de contrôle-commande des SED peut être atteint en utilisant la synthèse algébrique. Pour suivre les séquences, vous pouvez vous appuyer sur le support : UTL_CTRL_SA.pdf.

    
    

    
    

  • Select activity Équipe pédagogique

    Équipe pédagogique

    Contributeurs :  Gregory Faraut, Dimitri Renard, Bernard Riera et Jean Marc Roussel
    Intervenants :  Gregory Faraut et Bernard Riera
    

  • Select activity Introduction - Synthèse algébrique

    Completion

    Students must

    

    Mark as done

    Introduction - Synthèse algébrique

    
    

  • Select activity Rappels

    Completion

    Students must

    

    Mark as done

    Rappels

    
    

  • Select activity Intérêt

    Completion

    Students must

    

    Mark as done

    Intérêt

    
    

  • Select activity Principe de résolution

    Completion

    Students must

    

    Mark as done

    Principe de résolution

    
    

  • Select activity La meilleure solution

    Completion

    Students must

    

    Mark as done

    La meilleure solution

    
    

  • Select activity Conclusion

    Completion

    Students must

    

    Mark as done

    Conclusion

    
    

  • Select activity Mise en application

    Mise en application
    
    

    A vous de mettre en application ce que vous venez d'apprendre sur un exemple en utilisant 

    • le support: UTL_CTRL_SA_Application.pdf  , 
    • le logiciel ** Factory I/O **  https://realgames.b-cdn.net/fio/factoryio-installer-latest.exe  Ce logiciel ne fonctionne que sous PC Windows (machine virtuelle possible sous Linux ou Mac). , 
    • les modèles : UTL_CTRL_SA.zip  et 
    • la vidéo :
      

    
    

    
    
  • Select activity Références

    Références
    

    Hietter, Y. Synthèse algébrique de lois de commande pour les systèmes à évènements discrets logiques. Automatique / Robotique. École normale supérieure de Cachan - ENS Cachan, 2009.
    Français. ⟨NNT : ⟩. ⟨tel-00402699⟩
    • Leroux, H. and Roussel, J.-M. Algebraic synthesis of logical controllers with optimization criteria. 6th International Workshop on Verification and Evaluation of Computer and Communication
    Systems VECOS 2012, Aug 2012, Paris, France. pp. 103-114. ⟨hal-00734840⟩
    • Ranger, T. Approche par synthèse algébrique et filtre logique pour la commande des systèmes manufacturiers cyber-physiques. Automatique. Université de Reims Champagne Ardenne, 2023. Français. ⟨NNT : ⟩. ⟨tel-04255722⟩
    • Ranger, T., Philippot, A. and Riera, B. Manufacturing Tasks Synchronization by Algebraic Synthesis. IFAC Conference on Embedded Systems, Computational Intelligence and Telematics in Control
    (CESCIT), 2021, Valenciennes, France. ⟨10.1016/j.ifacol.2021.10.038⟩. ⟨hal-03404408⟩
    • Roussel, J.-M. and Lesage, J.-J. (2014). Design of

  • Select activity Pour aller plus loin (copie)

    Pour aller plus loin
    

    Prochaines éditions des écoles SED ...
    

• Select topic Chapitre 10 : Utilisation des SED pour le diagnostic

  Chapitre 10 : Utilisation des SED pour le diagnostic
  • Select activity Introduction (copie)

    Ce chapitre 10 présente l'utilisation des SED dans le cadre du diagnostic. Le diagnostic est une méthode qui permet d'identifier, de localiser et analyser un défaut par rapport à un comportement normal. Cette séquence présente des approches proches du diagnostic telle que l'opacité et autres extensions. Pour suivre les séquences, vous pouvez vous appuyer sur le support : UTL_Diag.pdf
    

    
    

    
    

  • Select activity Équipe pédagogique (copie)

    Équipe pédagogique

    Contributeurs : Mohamed Ghazel, Dimitri Lefevre, Hervé Marchand, Ramla Saddem, Armand Toguyéni
    Intervenant :  Ramla Saddem, Armand Toguyéni
    

  • Select activity Introduction

    Completion

    Students must

    

    Mark as done

    Introduction
    

    
    

  • Select activity Entraves à la sûreté de fonctionnement

    Completion

    Students must

    

    Mark as done

    Entraves à la sûreté de fonctionnement

    
    

  • Select activity Moyens pour la tolérance aux fautes

    Completion

    Students must

    

    Mark as done

    Moyens pour la tolérance aux fautes

    
    

  • Select activity Diagnostiqueur

    Completion

    Students must

    

    Mark as done

    Diagnostiqueur

    
    

  • Select activity Diagnosticabilité

    Completion

    Students must

    

    Mark as done

    Diagnosticabilité

    
    

  • Select activity Vérification de la diagnosticabilité

    Completion

    Students must

    

    Mark as done

    Vérification de la diagnosticabilité

    
    

  • Select activity Pronostic

    Completion

    Students must

    

    Mark as done

    Pronostic

    
    

  • Select activity Opacité

    Completion

    Students must

    

    Mark as done

    Opacité

    
    

  • Select activity Diagnostic des SED basés sur les Réseaux de Petri

    Completion

    Students must

    

    Mark as done

    Diagnostic des SED basés sur les Réseaux de Petri

    
    

  • Select activity Extensions de la diagnosticabilité

    Completion

    Students must

    

    Mark as done

    Extensions de la diagnosticabilité

    
    

  • Select activity Mise en application

    Mise en application
    
    A vous de mettre en application ce que vous venez d'apprendre sur un exemple en utilisant
    

    • le logiciel ** DESUMA ** lien de téléchargement

    • les modèles : UTL_Diag.zip

    • et la vidéo :
      

    
    

    
    
  • Select activity Références

    Références
    

    Laprie J.-C. (1995) . Guide de la sûreté de fonctionnement, Cépaduès, 369 pages, Toulouse, mai 1995,
    Li, B., Basilio, J. C., Khlif-Bouassida, M., & Toguyéni, A. (2017). Polynomial time verification of modular
    diagnosability of discrete event systems. IFAC-PapersOnLine, 50(1), 13618-13623.
    Liu, B. (2014). An Efficient Approach for Diagnosability and Diagnosis of DES Based on Labeled Petri Nets,
    Untimed and Timed Contexts (Doctoral dissertation, Ecole Centrale de Lille).
    Moreira, M. V., Jesus, T. C., & Basilio, J. C. (2011). Polynomial time verification of decentralized
    diagnosability of discrete event systems. IEEE Transactions on Automatic Control, 56(7), 1679-1684
    Saboori, A., & Hadjicostis, C. N. (2007, December). Notions of security and opacity in discrete event
    systems. In 2007 46th IEEE Conference on Decision and Control (pp. 5056-5061). IEEE.
    Zaytoon J., On Fault Diagnosis Methods of Discrete Event Systems, Plenière
    https://unidad.gdl.cinvestav.mx/wodes-12/downloads/slides/plenaryProfZaytoon.pdf
    Zwingelstein G (1995). Diagnostic des défaillances : théorie et pratique pour les systèmes industriels,
    Edition Hermès, Traité des Nouvelles Technologies “Série Diagnostic et Maintenance”, 601 pages, Paris, 1995,

  • Select activity Pour aller plus loin

    Pour aller plus loin
    

    Prochaines éditions des écoles SED ...
    

  • Select activity Pour revenir en arrière

    Pour revenir en arrière
    

    Si les notions d'automates à états et langages ne sont pas claires, vous pouvez suivre les vidéos : FRM_Aut_AutomatesAEtats.mp4, FRM_Aut_AutLangages.mp4 et FRM_Aut_AutOperations.mp4. Si les notions d'automates temporisés ne sont pas claires, vous pouvez suivre les vidéos : UTL_Verif_Modelchecking.mp4 et UTL_Verif_Proprietes.mp4.
    

  • Select activity Formation et École soutenues par :

    Formation et École soutenues par :