Richard St-Denis
Professeur associé

Université de Sherbrooke
Département d'informatique
Université de Sherbrooke
2500, boulevard de l'Université
Sherbrooke (Québec) Canada
J1K 2R1

Courriel

Modèles Alloy pour plusieurs variantes de la théorie du contrôle supervisé

---

Nous avons développé plusieurs modules, écrits en Alloy, qui modélisent des variantes de la théorie du contrôle supervisé. Ils s'insèrent dans un projet, appelé MELODIES (.Modeling Environment for LOgical DIscrete Event Systems.), dont le but est de fournir un environnement de prototypage aux novices du domaine, lequel est en constante évolution. Cet environnement peut être aussi utilisé pour résoudre des problèmes de contrôle. Les variantes suivantes sont présentement disponibles dans MELODIES.

1. Théorie du contrôle basée sur les états
1. Observation totale (Module SBCDES_Total_Observation)
• Problème du chat et de la souris avec cinq chambres
• Problème du chat et de la souris avec huit chambres
• Problème des deux trains avec six sections
• Problème des deux trains avec huit sections
• Problème des deux trains avec dix sections
• Problème des deux trains (fonction de contrôle)
• Composante élémentaire jack211r (flèche)
• Composante élémentaire suction cup (pince)
• Injecteur de la cellule de livraison
• Grue de la cellule de livraison
• Cellule de livraison (définition en compréhension du prédicat)
• Cellule de livraison
2. Observation partielle (Module SBCDES_Partial_Observation)
• Problème des deux trains avec un tunnel
• Problème des deux trains avec deux tunnels
3. Systèmes paramétrés (contrôle en ligne de n processus)
2. Théorie du contrôle basée sur les langages (Module Automaton)
1. Les propriétés de base (Module BasicProperties)
1. Propriété de contrôlabilité
• Exemple simple
• Problème des deux trains
• Composante élémentaire jack211r (flèche)
• Composante élémentaire suction cup (pince)
• Injecteur de la cellule de livraison
• Grue de la cellule de livraison
• Cellule de livraison
2. Propriété de normalité
• Exemple simple
2. Architectures de contrôle décentralisé (Module DistributedArchitectures)
1. Module Automaton
2. Test pour le module Automaton
3. Module Generator
4. Test pour le module Generator
5. Simple propriété d'observabilité
6. Propriétés d'observabilité inconditionnelle
• Exemple tiré de DEDS, 12 (3), Prop. 3 avec H de Fig. 4b
• Exemple tiré de DEDS, 12 (3), Prop. 3 avec H de Fig. 6
• Exemple tiré de DEDS, 12 (3), Prop. 4 avec H de Fig. 8b
• Exemple tiré de DEDS, 12 (3), Prop. 5 avec H de Fig. 11b
7. Propriétés d'observabilité conditionnelle
• Exemple tiré de IEEE TAC, 49 (11), Th. 2 avec H de Fig. 7
• Exemple tiré de IEEE TAC, 49 (11), Th. 2 avec H de Fig. 9
• Exemple tiré de IEEE TAC, 49 (11), Th. 4 avec H de Fig. 12
• Exemple tiré de IEEE TAC, 49 (11), Prop. 1 avec H de Fig. 12
• Exemple tiré de IEEE TAC, 49 (11), Th. 2 avec H de Fig. 17
3. Architecture de contrôle hiérarchique (Module Component)
1. Condition sur la technologie de contrôle standard pour un agent
2. Cohérence du marquage
3. Propriété d'observateur (équivalence observationnelle)
• Exemple simple
• Problème des deux trains
• Flèche de grue
• Pince de la grue
• Injecteur de la cellule de livraison
• Grue de la cellule de livraison
• Cellule de livraison
4. Propriété de N-inférence coobservabilité (prise de décision décentralisée)
3. Contrôle supervisé de structures en arborescence d'états
• Connexion aux interfaces
• Superposition d'un holon et d'un super-état
• Cohérence d'un holon