Systèmes temps réel 1: Techniques de description et de vérification (Traité IC2, série Informatique et systèmes d
379 pages
Français
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Systèmes temps réel 1: Techniques de description et de vérification (Traité IC2, série Informatique et systèmes d'information)

-

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
379 pages
Français

Description

Aujourd'hui, les systèmes informatiques temps réel sont présents dans de multiples secteurs d'activités : contrôle des systèmes automatisés de production, aide à la conduite des véhicules ou gestion des flux d'information sur des réseaux locaux et sur l'Internet. Au cours des 30 dernières années, le temps réel s'est progressivement établi comme une discipline à part entière qui rassemble une forte communauté issue à la fois du monde académique et de l'industrie. Ce traité en deux volumes a pour objectif de mieux faire connaître cette discipline : ses enjeux, les méthodes et formalismes qui lui sont spécifiques, les outils existants, les résultats connus et, naturellement, les recherches encore à mener. Ce second tome est consacré aux mécanismes exécutifs permettant l'obtention d'une ""qualité de service"" temps réel. En particulier, seront largement étudiés les stratégies d'ordonnancement de tâches ainsi que les réseaux et protocoles de communication temps réel.
Réseaux de petri temporels : méthodes d'analyse et vérifications avec TINA -B. Berthomieu, F. Vernadat. Combinaison entre vérification et test pour la validation de systèmes réactifs -C. Constant, Th. Jéron, H. Marchand, V. Rusu. Model checking : éléments de base -S. Merz. Vérification par automates temporisés -P. Bouyer, F. Laroussinie. Modélisation et analyse de systèmes asynchrones avec CADP -R. Mateescu. Vérification de programmes synchrones avec Lustre/Lesar -P. Raymond. Lucid Synchrone, un langage de programmation des systèmes réactifs -P. Caspi, G. Hamon, M. Pouzet. Vérification de systèmes probabilisés : méthodes et outils -S. Haddad, P. Moreaux. La boîte à outils IF pour la modélisation et la vérification de systèmes temps réels -M. Bozga, S. Graf, L. Mounier, I. Ober. Description d'architectures pour le temps réel : l'approche AADL -A.-M. Déplanche, S. Faucou. Index.

Sujets

Informations

Publié par
Date de parution 16 juin 2006
Nombre de lectures 123
EAN13 9782746237445
Langue Français
Poids de l'ouvrage 6 Mo

Informations légales : prix de location à la page 0,0892€. Cette information est donnée uniquement à titre indicatif conformément à la législation en vigueur.

Exrait








Systèmes temps réel 1





































© LAVOISIER, 2006
LAVOISIER
11, rue Lavoisier
75008 Paris

www.hermes-science.com
www.lavoisier.fr

ISBN 2-7462-1303-6


Le Code de la propriété intellectuelle n'autorisant, aux termes de l'article L. 122-5, d'une part,
que les "copies ou reproductions strictement réservées à l'usage privé du copiste et non
destinées à une utilisation collective" et, d'autre part, que les analyses et les courtes citations
dans un but d'exemple et d'illustration, "toute représentation ou reproduction intégrale, ou
partielle, faite sans le consentement de l'auteur ou de ses ayants droit ou ayants cause, est
illicite" (article L. 122-4). Cette représentation ou reproduction, par quelque procédé que ce
soit, constituerait donc une contrefaçon sanctionnée par les articles L. 335-2 et suivants du
Code de la propriété intellectuelle.
Tous les noms de sociétés ou de produits cités dans cet ouvrage sont utilisés à des fins
d’identification et sont des marques de leurs détenteurs respectifs.


Printed and bound in England by Antony Rowe Ltd, Chippenham, June 2006.





Systèmes temps réel 1



techniques de description et de vérification






sous la direction de
Nicolas Navet





















Il a été tiré de cet ouvrage
35 exemplaires hors commerce réservés
aux membres du comité scientifique,
aux auteurs et à l’éditeur
numérotés de 1 à 35
Systèmes temps réel 1
sous la direction de Nicolas Navet
fait partie de la série INFORMATIQUE ET SYSTÈMES D’INFORMATION
dirigée par Jean-Charles Pomerol





TRAITÉ IC2 INFORMATION – COMMANDE – COMMUNICATION
sous la direction scientifique de Bernard Dubuisson

Le traité 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, le traité
IC2 est l'état de l'art dans les domaines suivants retenus par le comité
scientifique :
Réseaux et télécoms
Traitement du signal et de l'image
Informatique et systèmes d'information
Systèmes automatisés et productique
Management et gestion des STICS
Cognition et traitement de l’information
Chaque ouvrage présente 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.



















Liste des auteurs



Grégoire HAMON Bernard BERTHOMIEU
Chalmers University of Technology LAAS
Göteborg Toulouse
Suède
Patricia BOUYER
Thierry JÉRON LSV
IRISA-INRIA École normale supérieure
Rennes Cachan

François LAROUSSINIE Marius BOZGA
LSV VERIMAG
École normale supérieure Gières
Cachan
Paul CASPI
Hervé MARCHAND VERIMAG
IRISA-INRIA Gières
Rennes
Camille CONSTANT
Radu MATEESCU IRISA-INRIA
INRIA Rhône-Alpes Rennes
École normale supérieure
Lyon Anne-Marie DÉPLANCHE
IRCCyN
Stephan MERZ Nantes
LORIA-INRIA
Vandœuvre-lès-Nancy Sébastien FAUCOU
IRCCyN
Patrice MOREAUX Nantes
LISTIC
Université de Savoie Susanne GRAF
Annecy VERIMAG
Gières
Laurent MOUNIER
Serge HADDAD VERIMAG
LAMSADE Gières
Université Paris-Dauphine
Nicolas NAVET Pascal RAYMOND
LORIA-INRIA VERIMAG
Vandœuvre-lès-Nancy Gières

Iulian OBER Vlad RUSU
Laboratoire GRIMM IRISA-INRIA
IUT de Blagnac Rennes

Marc POUZET François VERNADAT
LRI LAAS
Université Paris-Sud Toulouse
Orsay




























Table des matières
Préface.................................................... 19
Nicolas NAVET
Chapitre 1. Réseaux de Petri temporels : méthodes d’analyse
et vérification avec TINA...................................... 25
Bernard BERTHOMIEU et François VERNADAT
1.1. Introduction .......................................... 25
1.2. Les réseaux de Petri temporels ............................. 26
1.2.1. Réseaux temporels .................................. 26
1.2.2. États et relation d’accessibilité.......................... 27
1.2.3. Illustration ........................................ 28
1.2.4. Quelques théorèmes généraux 29
1.3. Graphes de classes préservant marquages et propriétés LTL......... 30
1.3.1. Classes d’états ..................................... 30
1.3.2. Illustration 31
1.3.3. Vérification à la volée du caractère borné.................. 32
1.3.4. Variantes ......................................... 34
1.3.4.1. Sensibilisations multiples......................... 34
1.3.4.2. Préservation des seuls marquages ................... 34
1.4. Graphes de classes préservant états et propriétés LTL............. 35
1.4.1. Domaines d’horloges ................................ 35
1.4.2. Construction du SSCG ............................... 36
1.4.3. Variantes 37
1.5. Graphes de classes préservant états et propriétés CTL............. 37
1.6. Calculs d’échéanciers .................................... 40
1.6.1. Systèmes d’échéanciers .............................. 40
1.6.2. Délais (dates relatives) et dates (absolues) ................ 41
1.6.3. Illustration ........................................ 41















10 Systèmes temps réel – Volume 1
1.7. Mise en œuvre, l’environnement Tina........................ 42
1.8. La vérification de formules SE–LTL dans Tina ................. 43
1.8.1. La logique temporelle SE–LTL ......................... 44
1.8.2. Préservation des propriétés LTL par les constructions de Tina...... 46
1.8.3. selt : le vérificateur SE–LTL de Tina ................... 46
1.8.3.1. Technique de vérification 46
1.8.3.2. La logique de selt ............................. 47
1.9. Quelques exemples d’utilisation de selt...................... 49
1.9.1. John et Fred ....................................... 49
1.9.1.1. Énoncé ...................................... 49
1.9.1.2. Les contraintes temporelles figurant dans ce scénario
sont-elles consistantes ? ............................... 49
1.9.1.3. Est-il possible que Fred ait pris le bus et que John ait
utilisé le covoiturage ? ................................ 51
1.9.1.4. A quels horaires Fred a pu partir ? .................. 51
1.9.2. Le protocole du bit alterné ............................ 52
1.10. Conclusion .......................................... 54
1.11. Bibliographie ......................................... 55
Chapitre 2. Combinaison entre vérification et test pour la validation
de systèmes réactifs........................................ 59
Camille CONSTANT, Thierry JÉRON, Hervé MARCHAND et Vlad RUSU
2.1. Introduction........................................... 59
2.2. Le modèle des IOSTS.................................... 62
2.2.1. Syntaxe des IOSTS.................................. 62
2.2.2. Sémantique des IOSTS. ............................. 63
2.2.3. Produit parallèle 65
2.2.4. Blocage et IOSTS suspendu ........................... 66
2.2.5. IOSTS déterministe et déterminisation .................... 67
2.3. Vérification et test de conformité pour des IOSTS ............... 67
2.3.1. Vérification ....................................... 67
2.3.1.1. Vérification de propriétés de sûreté .................. 68
2.3.1.2. Vérification de propriétés d’accessibilité .............. 70
2.3.1.3. Combinaisons d’observateurs ...................... 71
2.3.2. Test de conformité .................................. 72
2.4. Génération de tests et conformité............................ 73
2.5. Sélection des tests ...................................... 77
2.6. Étude de cas .......................................... 80
2.6.1. Spécification 80
2.6.2. Propriétés ........................................ 80
2.6.3. Génération du cas de test.............................. 82
2.6.3.1. Suspension................................ 82


























Table des matières 11
2.6.3.2. Déterminisation et testeur canonique ............. 82
2.6.3.3. Sélection ................................. 82
2.7. Conclusion et travaux connexes............................. 83
2.8. Bibliographie.......................................... 87
Chapitre 3. Model checking : éléments de base ................... 89
Stephan MERZ
3.1. Introduction........................................... 89
3.2. Exemple : contrôle d’un ascenseur........................... 90
3.3. Systèmes de transition et leurs exécutions ..................... 93
3.3.1. Modèles sémantiques de systèmes ....................... 93
3.3.2. Vérification d’invariants .............................. 94
3.4. Logiques temporelles .................................... 96
3.4.1. La logique temporelle linéaire .......................... 96
3.4.2. Les logiques temporelles arborescentes ................... 98
3.4.3. ω-automates ...................................... 101
3.4.4. Automates et PTL................................... 103
3.5. Algorithmes de model checking............................. 106
3.5.1. Algorithme local pour PTL ............................ 106
3.5.2. Algorithme global pour CTL ........................... 108
3.5.3. Algorithmes symboliques............................. 110
3.6. Quelques sujets actuels 113
3.7. Bibliographie.......................................... 115
Chapitre 4. Vérification par automates temporisés................... 121
Patricia BOUYER et François LAROUSSINIE
4.1. Introduction........................................... 121
4.2. Automates temporisés, exemples et sémantique ................. 122
4.2.1. Quelques notations .................................. 122
4.2.2. Automates temporisés, syntaxe et sémantique............... 123
4.2.3. Composition parallèle................................ 124
4.3. Décidabilité de l’accessibilité .............................. 125
4.4. Autres problèmes de vérification ............................ 128
4.4.1. Vérification et langages temporisés ...................... 128
4.4.2. Logique de temps arborescent .......................... 129
4.4.3. Logique de temps linéaire ............................. 130
4.4.4. Logiques modales avec points fixes 131
4.4.5. Automates de test................................... 131
4.4.6. Équivalences comportementales ........................ 131
4.5. Quelques extensions des automates temporisés.................. 132


























12 Systèmes temps réel – Volume 1
4.5.1. Les contraintes « diagonales » .......................... 132
4.5.2. Les contraintes additives.............................. 133
4.5.3. Les actions internes ................................. 135
4.5.4. Les mises à jour .................................... 135
4.5.5. Les automates hybrides linéaires ........................ 137
4.6. Quelques sous-classes des automates temporisés................. 138
4.6.1. Automates event-recording ............................ 138
4.6.2. Automates à une ou deux horloges....................... 138
4.6.3. Modèles à temps discret .............................. 140
4.7. Algorithmique de la vérification 140
4.7.1. Les zones, une représentation symbolique
pour les automates temporisés 141
4.7.2. Analyse en arrière des automates temporisés ............... 141
4.7.3. Analyse en avant des automates temporisés ................ 142
4.7.4. Les DBM, une structure de donnée pour les systèmes temporisés .... 144
4.8. L’outil Uppaal ........................................ 145
4.9. Bibliographie.......................................... 146
Chapitre 5. Modélisation et analyse de systèmes asynchrones avec CADP.... 151
Radu MATEESCU
5.1. Introduction........................................... 151
5.2. La boîte à outils CADP................................... 152
5.2.1. Le langage LOTOS ................................. 153
5.2.2. Systèmes de transitions étiquetées ....................... 153
5.2.3. Quelques outils de vérification ......................... 154
5.3. Modélisation d’une unité de perçage 158
5.3.1. Architecture....................................... 161
5.3.2. Dispositifs physiques et contrôleurs locaux................. 163
5.3.2.1. Table rotative.................................. 163
5.3.2.2. Verrou 164
5.3.2.3. Perceuse ..................................... 165
5.3.2.4. Testeur ...................................... 165
5.3.3. Contrôleur principal – Version séquentielle ................ 166
5.3.4. Contrôleur principal – Version parallèle ................... 168
5.3.5. Environnement 169
5.4. Analyse du fonctionnement de l’unité de perçage 170
5.4.1. Vérification par équivalences .......................... 170
5.4.2. Vérification par logiques temporelles..................... 173
5.5. Conclusion et travaux futurs ............................... 175
5.6. Bibliographie.......................................... 177





























Table des matières 13
Chapitre 6. Vérification de programmes synchrones avec Lustre/Lesar .. 181
Pascal RAYMOND
6.1. Approche synchrone..................................... 182
6.1.1. Le domaine des systèmes réactifs ....................... 182
6.1.2. L’approche synchrone ............................... 182
6.1.3. Les langages synchrones.............................. 183
6.2. Le langage Lustre....................................... 183
6.2.1. Principes ......................................... 183
6.2.2. Exemple du compteur de balises ........................ 184
6.3. Vérification de programme ................................ 185
6.3.1. Notion de propriété temporelle ......................... 185
6.3.2. Sûreté et vivacité ................................... 185
6.3.3. Exemple du compteur de balises 186
6.3.4. Machine à mémoire ................................. 186
6.3.5. Automate explicite .................................. 186
6.3.6. Principe du model-checking ........................... 187
6.3.7. Exemple d’abstraction ............................... 187
6.3.8. Abstraction conservative et propriétés de sûreté ............. 188
6.4. Expression des propriétés 189
6.4.1. Le schéma général du model-checking .................... 189
6.4.2. Model-checking des programmes synchrones ............... 190
6.4.3. Observateurs ...................................... 190
6.4.4. Exemples......................................... 190
6.4.5. Hypothèses ....................................... 191
6.4.6. Model-checking des programmes synchrones ............... 191
6.5. Algorithmique 192
6.5.1. Automate booléen .................................. 192
6.5.2. Automate explicite associé ............................ 192
6.5.3. Fonctions « pre » et « post » ........................... 193
6.5.4. Les états remarquables ............................... 193
6.5.5. Principe de l’exploration.............................. 193
6.6. Algorithme énumératif ................................... 194
6.7. Méthodes symboliques et graphes binaires de décision ............ 195
6.7.1. Notations......................................... 195
6.7.2. Manipulation de prédicats ............................. 196
6.7.3. Représentation des prédicats ........................... 196
6.7.3.1. Décomposition de Shannon........................ 196
6.7.3.2. Graphe binaire de décision 198
6.7.4. Interface typique d’une librairie de BDDs ................. 198
6.7.5. Implémentation de BDDs 199
6.7.6. Opérations sur les BDDs.............................. 199
6.7.6.1. Négation ..................................... 199




































14 Systèmes temps réel – Volume 1
6.7.6.2. Opérations binaires.............................. 199
6.7.6.3. Cofacteurs et quantificateurs ....................... 200
6.7.7. Notes sur la complexité des BDDs 201
6.7.8. Graphes de décision typés ............................. 202
6.7.8.1. Fonctions positives 202
6.7.8.2. TDG ........................................ 203
6.7.8.3. Implémentation des TDGs......................... 203
6.7.8.4. Gain engendré par les TDGs ....................... 203
6.7.9. Espace d’intérêt et cofacteur généralisé ................... 204
6.7.9.1. Opérations « sachant que » ........................ 204
6.7.9.2. Cofacteur généralisé ............................. 204
6.7.9.3. Restriction .................................... 205
6.7.9.4. Propriétés algébriques du cofacteur généralisé .......... 205
6.8. Exploration symbolique en avant............................ 206
6.8.1. Schéma général 206
6.8.2. Implémentation détaillée.............................. 206
6.8.3. Calcul symbolique d’image 207
6.8.4. Calcul optimisé d’image 209
6.8.4.1. Principes..................................... 209
6.8.4.2. Image universelle ............................... 209
6.8.4.3. Cas d’une seule fonction de transition ................ 210
6.8.4.4. Décomposition de Shannon de l’image 210
6.9. Exploration symbolique en arrière ........................... 211
6.9.1. Schéma général .................................... 211
6.9.2. Calcul d’image inverse 212
6.9.3. Comparaisons entre les deux méthodes ................... 213
6.10. Conclusion et travaux en relation 213
6.11. Démonstrations ....................................... 214
6.11.1. Lemme : propriété fondamentale du co-facteur ............. 214
6.12. Bibliographie ......................................... 215
Chapitre 7. Lucid Synchrone, un langage de programmation
des systèmes réactifs 217
Paul CASPI, Grégoire HAMON et Marc POUZET
7.1. Introduction........................................... 217
7.1.1. Langages pour les systèmes réactifs ...................... 217
7.1.1.1. Les langages synchrones .......................... 218
7.1.1.2. Développement par modèle ........................ 220
7.1.1.3. Des besoins convergents 221
7.1.2. Lucid Synchrone ................................... 221
7.2. Lucid Synchrone ....................................... 223































Table des matières 15
7.2.1. Un Langage à la ML sur des flots ....................... 224
7.2.1.1. Les flots comme objets de base ..................... 224
7.2.1.2. Opérations temporelles : décalage et initialisation ........ 224
7.2.2. Fonctions de flots................................... 225
7.2.3. Systèmes multi-horloges.............................. 227
7.2.3.1. L’opérateur d’échantillonnage when ................. 228
7.2.3.2. L’opération de combinaison merge .................. 229
7.2.3.3. Sur-échantillonnage ............................. 230
7.2.3.4. Contraintes d’horloges et synchronisme ............... 232
7.2.4. Valeurs statiques 233
7.2.5. Types de données et filtrage ........................... 234
7.2.6. Une construction pour partager la mémoire ................ 235
7.2.7. Signaux .......................................... 236
7.2.7.1. Les signaux vus comme des abstractions d’horloges ...... 237
7.2.7.2. Tester la présence et filtrer des signaux ............... 237
7.2.8. Machines à états et systèmes mixtes...................... 239
7.2.8.1. Préemption faible et préemption forte................. 239
7.2.8.2. ABRO et la réinitialisation modulaire 240
7.2.8.3. Définitions locales à un état........................ 241
7.2.8.4. Communication entre états et mémoires partagées........ 242
7.2.8.5. Actions par défaut et le rôle particulier de l’état initial..... 242
7.2.8.6. Réinitialiser ou prolonger un état .................... 243
7.2.9. Machines d’états paramétrées .......................... 244
7.2.10. Machines d’états et signaux........................... 245
7.2.11. Traits d’ordre supérieur.............................. 246
7.2.12. Deux exemples classiques ............................ 248
7.2.12.1. Le pendule inversé ............................. 248
7.2.12.2. Un contrôleur de chaudière ....................... 250
7.3. Discussion............................................ 252
7.3.1. Programmation fonctionnelle pour le réactif ou la description
de circuits ............................................. 253
7.3.2. Types, horloges et analyses statiques ..................... 253
7.3.3. Définition de systèmes mixtes .......................... 254
7.4. Conclusion ........................................... 255
7.5. Remerciements ........................................ 256
7.6. Bibliographie.......................................... 256
Chapitre 8. Vérification de systèmes probabilisés : méthodes et outils .... 261
Serge HADDAD et Patrice MOREAUX
8.1. Introduction 261
8.2. Évaluation de performance de modèles markoviens .............. 262


























16 Systèmes temps réel – Volume 1
8.2.1. Un modèle stochastique de systèmes à événements discrets ..... 262
8.2.2. Chaînes de Markov à temps discret ...................... 264
8.2.2.1. Présentation ................................... 264
8.2.2.2. Comportement transitoire et stationnaire d’une DTMC .... 265
8.2.3. Chaînes de Markov à temps continu 267
8.2.3.1. Présentation 267
8.2.3.2. Comportement transitoire et stationnaire d’une CTMC .... 267
8.3. Modèles stochastiques de haut niveau ........................ 269
8.3.1. Les réseaux de Petri à lois générales ..................... 269
8.3.1.1. Politique de choix............................... 270
8.3.1.2. Politique de service.............................. 271
8.3.1.3. Politique de mémoire ............................ 271
8.3.2. Les réseaux de Petri à lois exponentielles .................. 272
8.3.3. Indices de performance des réseaux de Petri ................ 272
8.3.4. Panorama des modèles et des méthodes d’évaluation
de performance ........................................ 273
8.3.5. L’outil GreatSPN ................................... 274
8.3.5.1. Les modèles supportés ........................... 275
8.3.5.2. Analyse qualitative des réseaux de Petri ............... 275
8.3.5.3. Analyse de performance des réseaux de Petri stochastiques . . 275
8.3.5.4. Architecture logicielle............................ 275
8.4. Vérification probabiliste des chaînes de Markov................. 275
8.4.1. Limites des indices de performance standard ............... 276
8.4.2. Une logique temporelle pour les chaînes de Markov .......... 276
8.4.3. Algorithme de vérification 278
8.4.4. Panorama de la vérification probabiliste des chaînes de Markov . . . 279
8.4.5. L’outil ETMCC .................................... 280
8.4.5.1. Langage des modèles de systèmes ................... 281
8.4.5.2. Langage des propriétés ........................... 281
8.4.5.3. Résultats calculés ............................... 281
8.4.5.4. Architecture logicielle............................ 281
8.5. Les processus de décision markoviens ........................ 281
8.5.1. Présentation des processus de décision markoviens ........... 281
8.5.2. Une logique temporelle pour les processus de décision markoviens . . . 282
8.5.3. Algorithme de vérification 283
8.5.4. Panorama de la vérification des processus de décision markoviens . . . 287
8.5.5. L’outil PRISM..................................... 288
8.5.5.1. Langage des modèles de systèmes ................... 288
8.5.5.2. Langage des propriétés ........................... 288
8.5.5.3. Résultats calculés ............................... 288
8.5.5.4. Architecture logicielle............................ 288
8.6. Bibliographie.......................................... 289


























Table des matières 17
Chapitre 9. La boîte à outils IF pour la modélisation et la vérification
de systèmes temps réel ....................................... 293
Marius BOZGA, Susanne GRAF, Laurent MOUNIER et Iulian OBER
9.1. Motivation............................................ 294
9.2. Architecture globale de la boîte à outils ....................... 296
9.2.1. Le niveau langage utilisateur........................... 296
9.2.2. Le niveau de description intermédiaire (IF) ............... 297
9.2.3. Les niveaux plate-forme d’exploration et graphe d’états ....... 298
9.3. La notation IF ......................................... 298
9.3.1. Modélisation des aspects fonctionnels .................... 299
9.3.2. Modélisation des aspects non fonctionnels ................. 301
9.3.3. Expression de propriétés à l’aide d’observateurs ............. 303
9.4. Les outils............................................. 304
9.4.1. Les composants noyaux .............................. 304
9.4.2. Les outils d’analyse statique ........................... 308
9.4.3. Les outils de validation............................... 309
9.4.4. L’outil de transformation depuis UML vers IF .............. 309
9.4.4.1. La modélisation avec UML ........................ 310
9.4.4.2. Les principes de transformation ..................... 310
9.5. Etude de cas : le programme de vol d’Ariane 5. ................ 312
9.5.1. Aperçu du programme de vol d’Ariane 5. ................. 312
9.5.2. Vérification de propriétés fonctionnelles .................. 314
9.5.3. Vérification de propriétés non fonctionnelles ............... 318
9.5.4. Vérification modulaire et utilisation d’abstractions ........... 320
9.6. Discussion............................................ 320
9.7. Bibliographie.......................................... 322
Chapitre 10. Description d’architectures pour le temps réel :
l’approche AADL 327
Anne-Marie DÉPLANCHE et Sébastien FAUCOU
10.1. Introduction 327
10.2. Principes généraux des langages de description d’architecture ...... 330
10.3. ADL et systèmes temps réel .............................. 331
10.3.1. Analyse des besoins ................................ 331
10.3.2. Vues architecturales 334
10.3.3. Tour d’horizon de l’existant .......................... 336
10.4. Le langage AADL ..................................... 337
10.4.1. Le langage en bref ................................. 338
10.4.2. Les outils associés 340
10.4.2.1. Outils d’analyse offerts par OSATE ................. 341
10.4.3. Cahier des charges de l’exemple ....................... 342

























18 Systèmes temps réel – Volume 1
10.4.4. Description d’une architecture ......................... 342
10.4.4.1. Organisation du modèle 342
10.4.4.2. Éléments de la plate-forme ....................... 343
10.4.4.3. Éléments de l’architecture logicielle................. 344
10.4.4.4. Construction de l’architecture opérationnelle .......... 346
10.4.5. Analyse de l’architecture candidate ..................... 350
10.4.5.1. Analyse d’ordonnançabilité 350
10.4.5.2. Analyse des latences entrées/sorties ................. 351
10.4.6. Quelques compléments .............................. 354
10.4.6.1. Modes de fonctionnement ........................ 354
10.4.6.2. Description des mécanismes de tolérance aux fautes ..... 355
10.4.6.3. Mécanismes d’extension du langage................. 355
10.5. Conclusion .......................................... 357
10.6. Bibliographie ......................................... 359
Index ..................................................... 363













Préface


Au cours des trente dernières années, le temps réel s’est progressivement établi
comme une discipline à part entière qui rassemble aujourd’hui une forte
communauté issue à la fois du monde académique et de l’industrie. Ce traité en deux
volumes a pour objectif de mieux faire connaître cette discipline : ses enjeux, les
méthodes et formalismes qui lui sont spécifiques, les outils existants, les résultats
connus et, naturellement, les recherches encore à mener.
L’informatique temps réel est une discipline qui concerne le contrôle ou le suivi
de systèmes qui évoluent dynamiquement. Ces systèmes peuvent être des
équipements de production ou de transport de produits, de matières, d’énergie ou
d’informations. A ce sens, indubitablement, le temps réel entretient des liens étroits
avec d’autres disciplines : l’automatique qui définit les cahiers des charges
sousjacents, la recherche opérationnelle pour les techniques de maîtrise et d’organisation
de systèmes discrets, l’ingénierie du logiciel pour la mise en œuvre d’un
développement sûr et de qualité, les processus stochastiques en raison de la
connaissance le plus souvent incomplète ou imparfaite des systèmes et de leur
environnement. En fait, ce qui fait l’essence de l’informatique temps réel est une
exigence de garantir le niveau de performances temporelles requis par la dynamique
et la sûreté des systèmes contrôlés ou surveillés : les résultats doivent non seulement
être corrects en valeur mais ils doivent aussi être produits et délivrés aux bons
instants. Le plus souvent cette exigence se traduira en des contraintes sur les dates
de fin d’exécution des activités, on parle alors de contraintes d’échéances. Garantir 20 Systèmes temps réel – Volume 1

le respect de ces contraintes repose sur un ensemble de techniques de vérification
formelle dont la plupart sont présentées dans ce premier tome du traité.
Les systèmes temps réel sont généralement « embarqués », c’est-à-dire situés à
l’intérieur même de l’environnement avec lequel ils doivent interagir, comme un
calculateur dans une voiture ou un avion. En plus des exigences de performances
temporelles, ils sont alors assujettis à de fortes contraintes d’encombrement, de coût
et parfois d’énergie, ce qui limite d’autant la puissance de calcul et l’espace
mémoire disponibles et constitue une différence fondamentale avec l’informatique
traditionnelle où globalement les ressources disponibles augmentent
exponentiellement au rythme de la loi de Moore.
Les domaines d’applications intégrant de manière concrète l’informatique temps
réel sont nombreux et de natures variées : contrôle de systèmes automatisés de
production, surveillance de systèmes, aide au pilotage de véhicules, comme par
exemple des systèmes électroniques de freinage offrant une meilleure sécurité, ou
contrôle de flux dans les réseaux tels l’internet pour des applications critiques de
télécommande, etc. Et l’on voit que le temps réel est loin d’être une discipline
désincarnée de la réalité et qu’il peut être source de progrès dans notre quotidien.
Ce traité est organisé en deux volumes et vingt et un chapitres, rédigés pour la
plupart par des conférenciers de la quatrième École d’été Temps Réel 2005
(ETR’05). Cette manifestation, soutenue par le GDR ARP (Architecture, Réseau et
système, Parallélisme) du CNRS et l’INRIA, est un événement phare pour la
communauté temps réel francophone qui a rassemblé, lors de sa dernière édition à
Nancy, 110 chercheurs et industriels du 13 au 16 septembre 2005.
Le second volume du traité, intitulé Systèmes Temps Réel : Ordonnancement,
Réseaux, Qualité de Service, est consacré aux mécanismes exécutifs permettant
l’obtention d’une « qualité de service » temps réel. En particulier, le problème
crucial du choix, de la configuration et de l’implémentation des stratégies
d’ordonnancement de tâches est largement traité. Une seconde partie du tome 2 est
dédiée aux réseaux et protocoles de communication temps réel qui permettent à des
entités distantes d’un même système de s’échanger des informations dans des délais
contraints.
Ce premier volume du traité, intitulé Systèmes Temps Réel : Techniques de
Description et de Vérification, a pour objet de faire connaître les principaux
formalismes, et les outils logiciels associés, qui offrent des solutions pour spécifier
un système temps réel et vérifier, avant le déploiement du système, le respect des
propriétés attendues. Les méthodes formelles constituent à l’évidence un facteur de
progrès considérables vers une informatique « sûre de fonctionnement » mais leur
utilisation ne pourra se faire à grande échelle que si les outils logiciels Préface 21


correspondants sont développés. C’est pourquoi ce premier tome est délibérément
orienté « outils » de façon à proposer des solutions concrètes à l’utilisateur potentiel
de méthodes formelles. Au-delà des outils, le but est également de faire mieux
connaître les formalismes sous-jacents et, c’est notre souhait, de montrer comment
les méthodes formelles peuvent améliorer la qualité et la sûreté des systèmes.
Classiquement, on distingue deux grandes familles de techniques pour vérifier
formellement la correction d’un système. En premier lieu, les techniques de preuve
(theorem proving) qui sont des démonstrations mathématiques au sens classique du
terme où la vérification des propriétés est effectuée par déduction à partir d’un
ensemble d’axiomes et de règles d’inférences. Si l’utilisateur est généralement aidé
par un assistant logiciel de preuve, l’automatisation n’en reste pas moins que très
partielle et des résultats un tant soit peu complexes ne peuvent être généralement
obtenus sans de fortes compétences mathématiques de la part de l’utilisateur.
La seconde famille de techniques est appelée vérification de modèles, ou
modelchecking, et consiste à construire, à partir d’une description formelle d’un système,
l’espace des états atteignables puis, en parcourant l’ensemble de ces états, à vérifier
le respect des propriétés attendues du système. Le model-checking est une technique
de vérification automatique, ou « presse-bouton », ce qui explique sans doute en
partie le succès grandissant qu’il rencontre dans l’industrie depuis une vingtaine
d’années. Une des principales limites de cette approche réside en l’explosion
combinatoire du nombre des états du système mais nous verrons au travers des
différents chapitres de ce livre qu’il existe toute une panoplie de stratégies qui
permettent souvent de limiter efficacement la taille de l’ensemble des états à
considérer.
La vérification débute par la phase de description formelle du système, par
exemple à l’aide de réseaux de Petri temporels (chapitre 1) ou d’automates
temporisés (chapitre 4). Ensuite vient la phase de spécification des propriétés de bon
fonctionnement que le système doit respecter. Ces propriétés relèvent de deux
grandes catégories : les « propriétés de sûreté », c’est-à-dire intuitivement le fait
qu’aucun événement indésirable ne se produira pendant toute la durée de vie du
système (par exemple une contrainte d’échéance non respectée) et les « propriétés de
vivacité » qui expriment qu’un comportement attendu se produira nécessairement
(comme le fait que le système continuera à évoluer pendant toute sa durée de vie
sans jamais être bloqué par des spécifications contradictoires). Typiquement pour
des systèmes temps réel, les propriétés sont exprimées dans des logiques temporelles
ou par des automates temporisés. Enfin, la troisième phase est l’étape de
vérification à proprement parler où des algorithmes de parcours de l’espace des états
permettent de décider ou non du respect des propriétés, et le cas échéant, de mettre
en évidence des contre-exemples. 22 Systèmes temps réel – Volume 1

L’essentiel de ce premier volume du traité sera consacré à la vérification par
model-checking et, comme nous pourrons le constater au travers des différentes
contributions, la communauté francophone est très active dans ce domaine que ce
soit sur les aspects théoriques ou la réalisation d’outils logiciels.
Le premier chapitre, rédigé par Bernard Berthomieu et François Vernadat, porte
sur la vérification de systèmes modélisés sous forme de réseaux de Petri temporels.
La forte expressivité de ce formalisme et la complémentarité des différentes
techniques de vérification sont illustrées sur des exemples traités à l’aide de l’outil
logiciel Tina.
Dans le second chapitre, Camille Constant, Thierry Jéron, Hervé Marchand et
Vlad Rusu proposent une approche méthodologique de validation couplant
vérification de la spécification du système et tests de son implantation sur
plateforme réelle d’exécution. Le test est en pratique éminemment complémentaire de la
vérification sur modèles. En effet, d’une part, le test est indispensable pour nous
renseigner sur la correction d’une implantation, et, parfois, vérifier la spécification
ne permet que de conclure partiellement quant au respect des propriétés de bon
fonctionnement. C’est le cas en particulier lorsque la complexité des modèles
nécessite l’emploi de techniques de résolutions approchées.
En partant de l’exemple de la vérification du contrôleur d’un ascenseur, Stephan
Merz, dans le chapitre 3, présente les fondements du model-checking : formalismes
de transition d’états pour la modélisation, logiques temporelles pour la spécification
des propriétés, algorithmes de vérification, classes de complexité des problèmes,
stratégies pour maîtriser l’explosion combinatoire du nombre des états et, enfin,
thématiques de recherche actuelles. Le chapitre 4, rédigé par Patricia Bouyer et
François Laroussinie, poursuit cette problématique du model-checking dans le cas
où les systèmes sont modélisés sous forme d’automates temporisés, qui permettent
de manipuler des contraintes de temps explicites dans un cadre sémantique bien
défini. Les propriétés qu’il est possible de vérifier et les algorithmes associés seront
au cœur du propos. Ce chapitre introduit également certaines extensions des
automates temporisés qui offrent plus d’expressivité dans la phase de spécification.
Inversement, il sera aussi question de restrictions sous lesquelles il est possible de
vérifier des propriétés hors d’atteinte dans le cadre général des automates
temporisés, et d’utiliser des algorithmes plus efficaces en termes de complexité.
Enfin, une présentation est faite de l’environnement de modélisation et de
vérification UPPAAL.
Au travers de l’exemple d’un système industriel de perçage de pièces métalliques
développé tout au long du chapitre 5, Radu Mateescu présente les possibilités de
modélisation et de vérification offertes par la boite à outils CADP, conçue pour
fournir une aide au développement dans le cadre général des systèmes asynchrones Préface 23


qui évoluent en parallèle et communiquent par l’échange de messages. Comme
données en entrée, CADP accepte des modèles dans plusieurs formalismes dont les
réseaux d’automates communicants ou des spécifications de plus haut niveau en
langage Lotos. CADP implémente un ensemble de techniques de transformation de
modèles, comme des réductions, des techniques de vérification, allant de la
simulation à la vérification de formules de logique temporelle, et fournit la
possibilité de générer des tests de conformité de l’implantation.
Le chapitre 6, rédigé par Pascal Raymond, est consacré à la vérification de
programmes écrits dans le langage synchrone Lustre à l’aide du model-checker
Lesar qui a été spécifiquement développé à cet effet. Les langages synchrones
connaissent un succès grandissant pour le développement des systèmes réactifs,
c’est à dire des systèmes en interaction continue avec leur environnement, qui
englobent en particulier les systèmes ayant des contraintes temps réel strictes.
Fondés sur des modèles mathématiques de la concurrence et du temps, les langages
synchrones se prêtent bien aux vérifications formelles et ce chapitre en est la
meilleure illustration. Le chapitre 7, rédigé par Paul Caspi, Grégoire Hamon et Marc
Pouzet, traite du langage Lucid Synchrone qui étend Lustre avec des constructions
de haut niveau issues des langages fonctionnels, et permet ainsi de gagner en
expressivité. Les auteurs expliquent en premier lieu pourquoi les approches
synchrones offrent des éléments de solutions pertinents pour la conception de
systèmes critiques. Ils dressent ensuite un historique des développements du langage
puis, présentent de façon détaillée ses primitives et les concepts théoriques
sousjacents, en les illustrant sur plusieurs exemples.
On assiste progressivement depuis une quinzaine d’années à l’émergence de
techniques de vérification probabiliste, en lien étroit avec les travaux sur les
processus stochastiques réalisés dans la communauté de l’évaluation de
performances. Ces approches sont motivées par l’intérêt pratique qu’il y a d’obtenir,
pendant la phase de conception d’un système, une évaluation probabiliste de la
satisfaction d’une propriété, par exemple pour dimensionner au plus juste en
fonction des objectifs de sûreté de fonctionnement ou pour évaluer les performances
relatives de différentes solutions en concurrence. D’autre part, une modélisation
probabiliste permet généralement de mieux capturer la réalité de systèmes non
déterministes, par exemple, ceux soumis à des aléas de fonctionnement. Serge
Haddad et Patrice Moreaux, dans le chapitre 8, dressent un panorama des techniques
de vérification probabiliste : chaînes de Markov en temps discret et continu, réseaux
de Petri à loi exponentielle et à loi générale, logiques temporelles sur les chaînes de
Markov et les processus de décision markoviens, etc. Enfin, sont présentés les
principaux outils du domaine que sont GreatSPN, ETMCC et PRISM.
Le chapitre 9, rédigé par Marius Bozga, Susanne Graf, Laurent Mounier et Iulian
Ober, présente la boîte à outils IF qui est un environnement de modélisation et de 24 Systèmes temps réel – Volume 1

vérification dédié aux systèmes temps réel. Au cœur de l’outil se trouve un langage
de description interne, basé sur un formalisme d’automates temporisés
communicants, dans lequel sont traduites des spécifications d’entrée en UML ou
SDL fournies par l’utilisateur. Une fois cette traduction effectuée, peuvent être
appliquées les techniques implantées dans IF, comme la réduction de modèles par
analyse statique, la simulation ou la vérification par model-checking. L’utilisation
de IF est illustrée sur une étude de cas du domaine de l’aérospatiale issue d’une
collaboration avec EADS.
Pendant la phase de conception, la description architecturale du système peut
servir de référentiel à tous les acteurs impliqués et fournir les informations
nécessaires pour simuler, voire vérifier formellement certaines propriétés ou générer
tests de conformité et code source. Le dixième et dernier chapitre de ce premier
tome, rédigé par Anne-Marie Déplanche et Sébastien Faucou, traite des langages de
description d’architectures (Architecture Description Language - ADL ) en illustrant
avec le langage AADL conçu et standardisé pour une utilisation dans l’avionique et
l’aérospatiale, mais qui, à la date d’impression de cet ouvrage, se présente comme
un bon candidat pour les systèmes temps réel en général. Après avoir examiné les
besoins spécifiques rencontrés dans le contexte du temps réel, le langage AADL et
les outils logiciels associés sont présentés puis appliqués sur l’exemple d’un système
de contrôle échantillonné en boucle fermée.
Pour conclure, je voudrais exprimer ma gratitude à M. Jean-Charles Pomerol,
directeur éditorial, pour la confiance qu’il a accepté de me témoigner et remercier
chaleureusement les auteurs et les relecteurs des chapitres qui ont offert de leur
temps et partagé leur expertise dans la rédaction de ce livre. Je remercie également
Françoise Simonot-Lion et Stephan Merz pour leurs remarques et suggestions sur ce
chapitre introductif.
Enfin, j’espère que cet ouvrage sera, pour vous, chers lecteurs, une source
d’information complète, fiable et bien documentée sur les systèmes temps réel. Je
vous en souhaite une excellente lecture.


Nicolas NAVET
Chapitre 1
Réseaux de Petri temporels : méthodes
d’analyse et vérification avec TINA
1.1. Introduction
Parmi les techniques proposées pour spécifier et vérifier des systèmes dans lesquels
le temps apparaît comme paramètre, deux sont largement utilisées : Les Automates
Temporisés (voir le chapitre 4 de ce volume, consacré à ce modèle) et les Réseaux de
Petri Temporels (ou Time Petri Nets), introduits dans [MER 74].
Les réseaux temporels sont obtenus depuis les réseaux de Petri en associant deux
dates min et max à chaque transition. Supposons que t soit devenue sensibilisée pour
la dernière fois à la date θ, alors t ne peut être tirée avant la date θ +min et doit l’être
au plus tard à la date θ+max, sauf si le tir d’une autre transition a désensibilisé t avant
que celle-ci ne soit tirée. Le tir des transitions est de durée nulle. Les réseaux
temporels expriment nativement des spécifications «en délais». En explicitant débuts et fins
d’actions, ils peuvent aussi exprimer des spécifications «en durées». Leur domaine
d’application est donc large.
Nous proposons dans ce chapitre un panorama des méthodes d’analyse disponibles
pour les réseaux temporels et discutons de leur mise en œuvre. Ces méthodes, basées
sur la technique des classes d’états, ont été initiées par [BER 83 ; 91]. Ces graphes
constituent des abstractions finies du comportement des réseaux temporels bornés.
Différentes ont été définies dans [BER 83 ; 01 ; 03b], préservant diverses
Chapitre rédigé par Bernard BERTHOMIEU et François VERNADAT.



26 Systèmes temps réel – Volume 1
classes de propriétés. Dans ce chapitre, nous discuterons de plus du problème
pratique de la vérification de propriétés (model-checking) de certaines logiques sur les
graphes de classes construits. La mise en œuvre de ces techniques nécessite des outils
logiciels, tant pour la construction des abstractions requises que pour leur vérification
elle-même. Les exemples discutés dans cet article ont été traités avec les outils de
l’environnement [BER 04].
Les concepts de base des réseaux temporels sont rappelés section 1.2. Les
sections 1.3 à 1.5 introduisent les constructions de graphes de classes, fournissant des
abstractions finies de l’espace infini des états des réseaux temporels. Les sections 1.3
et 1.4 présentent les constructions préservant les propriétés des logiques temporelles
basées sur une sémantique linéaire telles que LTL ; la construction de la section 1.3
assure la préservation des seules propriétés de LTL (traces maximales et marquages),
tandis que celle exposée en section 1.4 assure de plus la préservation des états du
réseau (marquage et information temporelle). La section 1.5 discute de la préservation
des propriétés des logiques à temps arborescent. La section 1.6 discute de l’analyse
d’échéanciers et présente une méthode permettant de caractériser exactement les dates
de tir possibles des transitions le long d’une séquence finie.
La boîte à outils , permettant la mise en œuvre de ces techniques, ainsi que des
techniques de vérification discutées ensuite, est présentée en section 1.7. Les sections
suivantes sont consacrées à la vérification (model-checking) de formules de logique
temporelle linéaire sur les graphes de classes. La section 1.8 présente la logique
retenue, SE−LTL, une extension de la logique LTL, ainsi que sa mise en œuvre par le
module de . La section 1.9 présente deux exemples d’applications et leur
vérification.
1.2. Les réseaux de Petri temporels
1.2.1. Réseaux temporels
+Soit I l’ensemble des intervalles réels non vides à bornes rationnelles non
né+gatives. Pour i ∈ I ,↓ i désigne sa borne inférieure et↑ i sa borne supérieure (si i
.+est borné) ou∞ (sinon). Pour tout θ ∈ R , i− θ désignera l’intervalle{x− θ|x ∈
i∧ x≥ θ}.
Définition 1. Un réseau temporel (ou Time Petri net, TPN en abrégé) est un tuple
P,T,Pre,Post,m ,I , dans lequelP,T,Pre,Post,m est un réseau de Petri0 s 0
+et I : T →I est une fonction appelée Intervalle Statique.s
L’application I associe une intervalle temporel I (t) à chaque transition du ré-s s
seau. Les rationnels Eft (t)=↓I (t) et Lft (t)=↑I (t) sont appelés date statiques s s s
de tir au plus tôt de t et date statique de tir au plus tard de t, respectivement. Un réseau
temporel est représenté figure 1.1.

Réseaux de Petri temporels 27
p1 p2
2
2
[0,3] [4,9] [0,2] [1,3]t5 t1 t2 t3
p3
p4 p5
t4
[0,2]
Figure 1.1. Un réseau temporel.
1.2.2. États et relation d’accessibilité
Définition 2. Un état d’un réseau temporel est un couple e =(m, I) dans lequel m
+est un marquage et I : T → I une fonction qui associe un intervalle temporel à
chaque transition sensibilisée par m.
L’état initial est e =(m ,I ),où I est la restriction de I aux transitions sen-0 0 0 0 s
sibilisées par le marquage initial m . Toute transition sensibilisée doit être tirée dans0
l’intervalle de temps qui lui est associé. Cet intervalle est relatif à la date de
sensibilisation de la transition.
Franchir t, à la date θ, depuis e=(m, I), est donc permis si et seulement si :
m≥Pre(t)∧ θ∈ I(t)∧ (∀k = t)(m≥Pre(k)⇒ θ≤↑(I(k))).
L’état e =(m ,I ) atteint depuis e par le tir de t à θ est alors déterminé par :
1) m = m−Pre(t)+Post(t) (comme dans les réseaux de Petri)
2) Pour chaque transition k sensibilisée par m :
.
I’(k) = si k = t et m−Pre(t)≥Pre(k) alors I(k)− θ sinon I (k).s
t@θ
−→ la relation d’accessibilité temporisée définie ci-dessus et définissonsNotons
t t@θ e→ e par (∃θ)(e −→ e ). Un échéancier de tir est une séquence de transitions
temporisées t @θ ...t @θ ; il est réalisable depuis l’état e si les transitions de la séquence1 1 n n28 Systèmes temps réel – Volume 1
σ = t ...t sont successivement tirables depuis l’état e, aux dates relatives qui leurs1 n
sont associées. La séquence σ est appelée support de l’échéancier. Une séquence de
transitions est tirable si et seulemet si elle est le support d’un échéancier réalisable.
Notons que, dans les réseaux temporels (contrairement aux automates temporisés)
l’écoulement du temps ne peut qu’augmenter l’ensemble des transitions tirables, mais
en aucun cas le réduire. Si une transition est tirable à la date relative θ (ou, de
façon équivalente, immédiatement après une attente de θ unités de temps), alors elle le
restera tant que le temps peut s’écouler. Nous ne démontrerons pas ici cette propriété,
t
mais il en résulte que la relation→ définie ci-dessus caractérise exactement le
comportement «discret» d’un TPN (préservant la bissimilarité après abstraction du temps). Si
l’on s’intéresse au comportement temporel (capturé par la bissimulation temporisée),
t@θ
on doit ajouter aux transitions de la relation −→ celles traduisant le seul écoulement
δ(r) .
du temps, c’est-à-dire celles de la forme (m, I) −→ (m, I−r) (le délai r n’étant pas
plus grand que↑(I(k)), pour toute composante I(k) de I).
Enfin, notons que le concept d’état présenté associe exactement un intervalle
temporel à chaque transition sensibilisée, que celle-ci soit ou non multi-sensibilisée (t est
multi-sensibilisée par m s’il existe un entierk> 1 tel que m≥ k.Pre(t)). Une
interprétation alternative est discutée dans [BER 01], dans laquelle un intervalle temporel
est associé à chaque instance de sensibilisation des transitions. Cette interprétation
sera brièvement discutée en section 1.3.4.1.
1.2.3. Illustration
Les états peuvent être représentés par des paires (m,D), dans lesquelles m est un
marquage et D un ensemble de vecteurs de dates appelé domaine de tir. La i-ième
projection de l’espace D est l’intervalle de tir I(t ) associé à la i-ième transition sen-i
sibilisée. Les domaines de tir seront décrits par des systèmes d’inéquations linéaires
avec une variable par transition sensibilisée (notées comme les transitions).
L’état initial e =(m ,D ) du réseau figure 1.1 est ainsi représenté par :0 0 0
m : p ,p ∗ 20 1 2
D : 4≤ t ≤ 90 1
Le tir de t depuis e , à une date relative θ ∈ [4,9], mène en e =(m ,D ) :1 0 1 1 1 1
m : p ,p ,p1 3 4 5
D : 0≤ t ≤ 21 2
1≤ t ≤ 33
0≤ t ≤ 24
0≤ t ≤ 35Réseaux de Petri temporels 29
Le tir de t depuis e , à une date relative θ ∈ [0,2], mène en e =(m ,D ) :2 1 2 2 2 2
m : p ,p ,p2 2 3 5
D : max(0, 1− θ )≤ t ≤ 3− θ2 2 3 2
0≤ t ≤ 2− θ4 2
0≤ t ≤ 3− θ5 2
Comme θ peut prendre toute valeur réelle dans [0,2], l’état e admet une infinité2 1
de successeurs par t .2
1.2.4. Quelques théorèmes généraux
Rappelons tout d’abord un résultat d’indécidabilité :
Théorème 1. Les problèmes de l’accessibilité d’un marquage, d’un état, du caractère
borné et du caractère vivant, sont indécidables pour les TPN s.
Démonstration : Il est démontré dans [JON 77] que le problème de l’accessibilité d’un
marquage dans les TPN s peut être réduit à celui, indécidable, de l’arrêt d’une
machine à deux compteurs. Il en résulte l’indécidabilité des autres problèmes.
Représenter le fonctionnement d’un réseau temporel par le graphe d’accessibilité
de ses états (comme le d’un réseau de Petri est représenté par le graphe
d’accessibilité de ses marquages) est en général impossible : les transitions pouvant
être tirées à tout instant dans leur intervalle de tir, les états admettent en général une
infinité de successeurs par la règle de tir. Les classes d’états définies par la suite ont
pour but de fournir une représentation finie de cet ensemble infini d’états, lorsque
le réseau est borné, par regroupements de certains ensembles d’états. Toutefois, il
existe deux sous-classes remarquables de réseaux temporels pour lesquels chaque état
n’admet qu’un nombre fini de successeurs et donc admettant un graphe d’états fini
lorsqu’ils sont bornés.
Théorème 2. Soit un réseau temporel N = P ,T ,Pre,Post,M ,I . Si, pour ∫
toute transition t∈ T , I (t) est non borné supérieurement, alors son graphe des étatss
est isomorphe au graphe des marquages du réseau de Petri sous-jacent.
Démonstration : Par induction. Si chaque transition porte un intervalle statique non
borné, alors la condition de franchissement des transitions se réduit à celle des réseaux
de Petri (sans contrainte temporelle). De plus, la règle de tir préserve le caractère non
borné des intervalles.30 Systèmes temps réel – Volume 1
Théorème 3. Soit un réseau temporelN = P ,T ,Pre,Post,M ,I .Si I associe ∫ s
à chaque transition un intervalle réduit à un seul point, alors :
(i) le graphe des états du réseau est fini si et seulement si le réseau est borné ;
(ii) si, de plus, les intervalles statiques sont tous identiques, alors son graphe des états
est isomorphe au graphe des marquages du réseau de Petri sous-jacent.
Démonstration : Par induction. (i) Par la règle de tir, si tous les intervalles sont
ponctuels, alors un état a, au plus, autant d’états suivants que de transitions qu’il sensibilise.
De plus, la règle de tir préserve le caractère ponctuel des intervalles. Pour (ii), noter
que la condition de franchissement se réduit alors à celle des réseaux de Petri.
Les théorèmes 2 et 3 permettent d’interpréter de diverses façons les réseaux de
Petri comme des réseaux temporels. L’interprétation la plus fréquente est les considérer
comme des réseaux temporels dont chaque transition porte l’intervalle [0,∞[.
1.3. Graphes de classes préservant marquages et propriétés LTL
1.3.1. Classes d’états
L’ensemble des états d’un réseau temporel peut être infini pour deux raisons :
d’une part parce qu’un état peut admettre une infinité de successeurs, d’autre part,
parce qu’un réseau peut admettre des échéanciers de longueur infinie passant par des
états dont les marquages sont tous différents. Le deuxième cas sera discuté section
1.3.3. Pour gérer le premier cas, on regroupera certains ensembles d’états en classes
d’états. Plusieurs regroupements sont possibles ; le regroupement discuté dans cette
section est celui introduit dans [BER 83 ; 91].
Pour chaque séquence de tir tirable σ, notons C l’ensemble des états atteintsσ
depuis l’état initial en tirant des échéanciers de support σ. Pour tout ensemble C , dé-σ
finissons son marquage comme celui des états qu’il contient (tous ces états ont
nécessairement le même marquage) et son domaine de tir comme la réunion des domaines
∼de tirs des états qu’il contient. Enfin, notons = la relation satisfaite par deux ensembles
C et C si ceux-ci ont même marquage et même domaine de tir. Si deuxσ σ
∼d’états sont liés par =, alors tout échéancier réalisable depuis un état de l’un de ces
ensembles est réalisable depuis un état se trouvant dans l’autre ensemble.
Le graphe des classes d’états de [BER 83], ou SCG, est l’ensemble des ensembles
∼d’états C , pour toute séquence σ tirable, considérés modulo la relation =, muni de laσ
t ∼relation de transition : C → X si et seulement si C = X . La classe initiale est laσ σ.t
classe d’équivalence de l’ensemble d’états constitué du seul état initial.
Le SCG est obtenu comme suit. Les classes d’états sont représentées par des
paires (m, D),où m est un marquage et D un domaine de tir décrit par un système

Réseaux de Petri temporels 31
d’inéquations linéaires Wφ ≤ w. Les variables φ sont bijectivement associées aux
∼transitions sensibilisées par m.Ona (m, D) (m ,D ) si et seulement si m = m et=
les domaines D et D ont même ensemble de solutions.
Algorithme 1 (Calcul du SCG).
Pour toute séquence σ tirable, L peut être calculée comme suit. Calculer le plus petitσ
ensemble de classes contenant L et tel que, lorsque L ∈ C et σ.t est tirable, alors σ
∼(∃X ∈ C)(X = L ).σ.t
– La classe initiale est L =(m ,{Eft (t)≤ φ ≤ Lft (t)| m ≥Pre(t)}) 0 s s 0t
–Si σ est tirable et L =(m, D), alors σ.t est tirable si et seulement si :σ
(i) m≥Pre(t) (t est sensibilisée par m)et;
(ii) le système D∧{φ ≤ φ | i = t∧ m≥Pre(i)} est consistant.
t i
–Si σ.t est tirable, alors L =(m ,D ) est obtenue depuis L =(m, D) par :σ.t σ
m = m−Pre(t)+Post(t),
D obtenu comme suit :
(a) Les contraintes (ii) ci-dessus de tirabilité de t depuis L sont ajoutées à D ;σ
(b) Pour chaque k sensibilisée par m , une variable φ est introduite, par :
k
φ = φ − φ ,si k = t et m−Pre(t)≥Pre(k),
k k t
Eft (k)≤ φ ≤ Lft (k), sinon ;s sk
(c) les variables φ sont éliminées.
∼L est la classe d’équivalence pour la relation de l’ensemble C des états at-=σ σ
∼teints en tirant depuis s des échéanciers de support σ. L’équivalence est vérifiée=0
en mettant les systèmes représentant les domaines de tir sous forme canonique. Ces
systèmes sont des systèmes de différences, calculer leur forme canonique se ramène
à un problème de plus court chemin entre toutes paires de sommets, résolu en temps
polynômial en utilisant, par exemple, l’algorithme de Floyd/Warshall.
∼Remarque : deux ensembles C et C peuvent être équivalents par = bien que deσ σ
contenus différents. La notation des classes par une paire (m, D), identifie de façon
∼canonique une classe d’équivalence d’ensembles d’états pour la relation =, mais pas
un ensemble d’états.
1.3.2. Illustration
A titre d’illustration, construisons quelques classes du réseau temporel représenté
figure 1.1. La classe initiale c est décrite comme l’état initial e (voir section 1.2.3).0 0
Le tir de t depuis c conduit à une classe c décrite comme l’état e . Le tir de t1 0 1 1 2