Hermès science publications-Lavoisier
-
-
Disponible - 62.0 APP
Niveau 3 - Techniques
Approches formelles des systèmes embarqués communicants
Résumé
Examen des éléments concernant la problématique actuelle des systèmes embarqués, exposé des acquis de nouvelles directions de recherche sur les modèles et leur utilisation, et présentation des outils logiciels disponibles.
- Contributeur(s)
- Éditeur(s)
-
Date
- impr. 2008
-
Notes
- Notes bibliogr.
-
Langues
- Français
-
Description matérielle
- 1 vol. (268-XIII p.) : ill. ; 24 cm
- Collections
- Sujet(s)
-
ISBN
- 978-2-7462-1942-7
-
Indice
- 62.0 Automatique théorique
-
Quatrième de couverture
-
IC2 - Information, Commande, Communication répond au besoin de disposer d'un ensemble complet des connaissances et méthodes nécessaires à la maîtrise des systèmes technologiques.
Conçu volontairement dans un esprit d'échange disciplinaire, IC2 représente l'état de l'art dans les domaines suivants retenus par le comité scientifique :
Cognition et traitement de l'information
Information et sciences du vivant
Informatique et systèmes d'information
Management et gestion des STIC
Réseaux et télécoms
Signal et Image
Systèmes automatisés
Technologies et développement durable
Chaque ouvrage décrit aussi bien les aspects fondamentaux qu'expérimentaux. Une classification des différents articles contenus dans chacun, une bibliographie et un index détaillé orientent le lecteur vers ses points d'intérêt immédiats : celui-ci dispose ainsi d'un guide pour ses réflexions ou pour ses choix.
Les savoirs, théories et méthodes rassemblés dans chaque ouvrage ont été choisis pour leur pertinence dans l'avancée des connaissances ou pour la qualité des résultats obtenus dans le cas d'expérimentations réelles.
-
-
Tables des matières
-
Approches formelles des systèmes embarqués communicants
Lavoisier
- Préface 15
- Claude Jard et Olivier H. Roux
- Chapitre 1. Modéliser et vérifier les systèmes embarqués : pourquoi, comment ? 17
- Jean-Pierre Elloy
- 1.1. Principes et structure des systèmes embarqués17
- 1.1.1. Du particularisme des systèmes embarqués17
- 1.1.2. De la structure générale des systèmes embarqués18
- 1.1.3. De la constitution générale d'un système de pilotage19
- 1.1.4. De la constitution des contrôleurs d'un système de pilotage20
- 1.2. Les écueils à la sûreté de fonctionnement des systèmes pilotés21
- 1.2.1. De la complexité intrinsèque des systèmes de pilotage21
- 1.2.2. Qu'est-ce qu'un système piloté sûr de fonctionnement ?22
- 1.3. Les raisons qui peuvent provoquer un dysfonctionnement23
- 1.3.1. Les fautes de non-conformité23
- 1.3.2. Les erreurs non évitables25
- 1.3.3. Les erreurs incontrôlables27
- 1.3.4. Les fautes résiduelles27
- 1.3.4.1. Les spécifications sont restées incomplètes27
- 1.3.4.2. Les vérifications sont restées incomplètes28
- 1.3.4.3. L'analyse des risques est imparfaite28
- 1.4. Principes de représentation et d'analyse des systèmes de pilotage28
- 1.4.1. De la nécessité d'une représentation abstraite28
- 1.4.2. Du type de «structure logique» à modéliser30
- 1.5. La conception via la modélisation32
- 1.5.1. Du recours aux techniques formelles d'analyse32
- 1.5.2. Exhiber les composants élémentaires d'un système de pilotage36
- 1.5.3. La modélisation entre spécification et implantation37
- 1.6. Conclusion : modéliser l'ossature des composants du système de pilotage39
- 1.7. Bibliographie41
- Chapitre 2. Les modèles pour les systèmes temps réel embarqués 45
- Didier Lime et Olivier H. Roux
- 2.1. Introduction45
- 2.1.1. Les problèmes du model checking et du contrôle46
- 2.1.2. Les modèles temporisés47
- 2.2. Notations, langages et systèmes de transitions temporisés50
- 2.3. Modèles temporisés53
- 2.3.1. Automates temporisés53
- 2.3.2. Réseaux de Petri T-temporels55
- 2.3.3. Décidabilité des problèmes classiques58
- 2.3.4. Expressivité comparée de différentes classes de modèles temporisés59
- 2.3.4.1. Bisimulation et expressivité de modèles temporisés59
- 2.3.4.2. Expressivité comparée de différentes classes de TPN60
- 2.3.4.3. Expressivité : (...) versus T A61
- 2.4. Modèles à chronomètres62
- 2.4.1. Modèles formels pour l'ordonnancement62
- 2.4.1.1. Automates et ordonnancement62
- 2.4.1.2. Réseaux de Petri temporels et ordonnancement63
- 2.4.2. Automates à chronomètres64
- 2.4.3. Réseaux de Petri temporels à chronomètres66
- 2.4.4. Décidabilité des modèles à chronomètres70
- 2.5. Conclusion71
- 2.6. Bibliographie72
- Chapitre 3. Model checking temporisé 75
- Béatrice Bérard
- 3.1. Introduction75
- 3.2. Modèles temporisés76
- 3.2.1. Systèmes de transitions temporisés76
- 3.2.2. Automates temporisés78
- 3.2.3. D'autres modèles81
- 3.3. Logiques temporisées83
- 3.3.1. Les logiques temporelles CTL et LTL83
- 3.3.2. Extensions temporisées85
- 3.3.2.1. Extensions de CTL85
- 3.3.2.2. Extensions de LTL87
- 3.4. Model checking temporisé88
- 3.4.1. Model checking (non temporisé) de LTL et de CTL88
- 3.4.2. Automate des régions90
- 3.4.3. Model checking de TCTL93
- 3.4.4. Model checking de MTL95
- 3.4.5. Model checking efficace95
- 3.4.6. Model checking en pratique97
- 3.5. Conclusion98
- 3.6. Bibliographie98
- Chapitre 4. Contrôle des systèmes temporisés 105
- Franck Cassez et Nicolas Markey
- 4.1. Introduction105
- 4.1.1. Vérification des systèmes temporisés105
- 4.1.2. Le problème de la synthèse de contrôleur106
- 4.1.3. Du contrôle aux jeux107
- 4.1.4. Les différents objectifs de jeux108
- 4.1.5. Les différents types de jeux non temporisés108
- 4.2. Les jeux temporisés109
- 4.2.1. Jeux temporisés110
- 4.2.2. Déroulement du jeu et stratégies111
- 4.2.2.1. Exécutions d'un jeu temporisé111
- 4.2.2.2. Stratégies112
- 4.3. Calcul des états gagnants et des stratégies114
- 4.3.1. Prédécesseurs contrôlables115
- 4.3.2. Opérateurs symboliques117
- 4.3.3. Calcul symbolique des états gagnants117
- 4.3.4. Synthèse de stratégies gagnantes119
- 4.4. Stratégies «de Zénon»119
- 4.5. Implémentabilité121
- 4.5.1. Classes d'automates hybrides121
- 4.5.2. Existence de contrôleurs continus non implémentables122
- 4.5.3. Résultats récents et problèmes ouverts123
- 4.6. Spécification des objectifs de contrôle123
- 4.7. Contrôle optimal125
- 4.7.1. Automates temporisés à coûts125
- 4.7.2. Coût optimal dans les jeux temporisés127
- 4.7.3. Calcul du coût optimal129
- 4.7.4. Résultats récents et problèmes ouverts130
- 4.8. Algorithmes efficaces à la volée131
- 4.8.1. Algorithmes à la volée132
- 4.8.2. Résultats récents et problèmes ouverts133
- 4.9. Observation partielle134
- 4.10. Changeons les règles du jeu...135
- 4.11. Bibliographie137
- Chapitre 5. Diagnostic des systèmes temporisés 145
- Franck Cassez et Stavros Tripakis
- 5.1. Introduction145
- 5.2. Rappels sur les systèmes temporisés146
- 5.2.1. Mots temporisés et langages temporisés147
- 5.2.2. Automate temporisé147
- 5.2.3. Produit d'automates temporisés148
- 5.2.4. Automates temporisés pour le diagnostic149
- 5.3. Les problèmes de diagnostic150
- 5.3.1. Diagnostiqueur150
- 5.3.2. Problèmes de diagnostic151
- 5.3.3. Test de diagnosticabilité152
- 5.4. Diagnostic des systèmes à événements discrets152
- 5.4.1. Système à événements discrets pour le diagnostic153
- 5.4.2. Vérification de la diagnosticabilité154
- 5.4.3. Calcul du délai maximal de détection des fautes156
- 5.4.4. Synthèse d'un diagnostiqueur157
- 5.5. Diagnostic des systèmes temporisés158
- 5.5.1. Vérification de la diagnosticabilité158
- 5.5.2. Calcul du délai maximal de détection des fautes161
- 5.5.3. Synthèse d'un diagnostiqueur163
- 5.5.4. Diagnostic à l'aide d'automates temporisés déterministes164
- 5.6. Extensions et problèmes ouverts173
- 5.7. Bibliographie174
- Chapitre 6. Vérification quantitative de chaînes de Markov 177
- Susanna Donatelli et Serge Haddad
- 6.1. Introduction177
- 6.2. Evaluation de performance de modèles markoviens178
- 6.2.1. Un modèle stochastique de systèmes à événements discrets178
- 6.2.2. Chaînes de Markov à temps discret181
- 6.2.3. Chaînes de Markov à temps continu184
- 6.3. Vérification de chaînes de Markov à temps discret186
- 6.3.1. Logiques temporelles pour chaînes de Markov186
- 6.3.2. Vérification de PCTL188
- 6.3.3. Vérification de PLTL188
- 6.3.4. Vérification de PCTL*191
- 6.4. Vérification de chaînes de Markov à temps continu192
- 6.4.1. Limites des indices de performance standard192
- 6.4.2. Une logique temporelle pour les chaînes de Markov à temps continu192
- 6.4.3. Algorithme de vérification194
- 6.5. Panorama de la vérification quantitative de chaînes de Markov196
- 6.6. Bibliographie197
- Chapitre 7. Outils de Model Checking 199
- Alexandre David, Gerd Behrmann, Kim G. Larsen, Paul Pettersson, Jacob Illum Rasmussen, Wang Yi, Didier Lime, Morgan Magnin et Olivier H. Roux
- 7.1. Introduction199
- 7.2. Uppaal200
- 7.2.1. Automates temporisés et exploration symbolique200
- 7.2.1.1. Exemple203
- 7.2.2. Requêtes204
- 7.2.3. Architecture de l'outil206
- 7.2.4. Pipeline d'atteignabilité207
- 7.2.5. Pipeline de vivacité209
- 7.2.6. Pipeline de réponse bornée210
- 7.2.7. Réduction des horloges actives211
- 7.2.8. Techniques de réduction d'espace212
- 7.2.8.1. Eviter de stocker tous les états212
- 7.2.8.2. Partager les données212
- 7.2.8.3. Graphe minimal212
- 7.2.8.4. Réduction par symétrie213
- 7.2.9. Techniques d'approximation214
- 7.2.9.1. Surapproximation : enveloppe convexe214
- 7.2.9.2. Sous-approximation : hachage en bit des états214
- 7.2.10. Extensions215
- 7.2.10.1. Atteignabilité robuste215
- 7.2.10.2. Fusion de DBMs215
- 7.2.10.3. Chronomètres216
- 7.2.10.4. Autres extensions216
- 7.3. Uppaal-CORA216
- 7.3.1. Automates temporisés à coûts216
- 7.3.2. Exemple219
- 7.4. Uppaal-TIGA219
- 7.4.1. Automates de jeux temporisés219
- 7.4.2. Pipeline d'atteignabilité221
- 7.4.3. Optimalité temporelle223
- 7.4.4. Stratégies coopératives224
- 7.5. Roméo : un outil pour l'analyse des extensions temporelles des réseaux de Petri225
- 7.5.1. Modèles225
- 7.5.1.1. Réseaux de Petri temporels225
- 7.5.1.2. Réseaux de Petri temporels étendus à l'ordonnancement227
- 7.5.2. Architecture générale229
- 7.5.3. Modélisation de systèmes230
- 7.5.4. Vérification de propriétés230
- 7.5.4.1. Model checking en ligne230
- 7.5.4.2. Model checking hors ligne230
- 7.5.5. Comparaisons avec d'autres outils236
- 7.5.6. Cas d'étude236
- 7.5.6.1. Description236
- 7.6. Bibliographie238
- Chapitre 8. Outils pour l'analyse des modèles hybrides 245
- Thao Dang, Goran Frehse, Antoine Girard et Colas Le Guernic
- 8.1. Introduction245
- 8.2. Automates hybrides et le calcul d'atteignabilité246
- 8.3. Automates hybrides linéaires250
- 8.4. Systèmes hybrides affines par morceaux252
- 8.4.1. Discrétisation en temps253
- 8.4.1.1. Dynamique autonome253
- 8.4.1.2. Dynamique avec entrée254
- 8.4.2. Calcul d'atteignabilité en grande dimension255
- 8.4.2.1. Repésentation des états atteignables par des zonotopes255
- 8.4.2.2. Implantation efficace256
- 8.4.2.3. Traitement des transitions discrètes257
- 8.5. Techniques d'hybridisation pour le calcul d'atteignabilité259
- 8.5.1. Approximation par un automate hybride linéaire259
- 8.5.2. Hybridisation de systèmes continus non linéaires261
- 8.5.2.1. Propriétés d'approximation de l'ensemble atteignable262
- 8.5.2.2. Approximation par un système hybride affine par morceaux263
- 8.5.3. Hybridisation avec raffinement265
- 8.6. Bibliographie267
-
-
Origine de la notice:
- BNF
-
Disponible - 62.0 APP
Niveau 3 - Techniques
