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

Nicolas Navet

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

• Sciences & Techniques
• Informatique
• Electronique & télécommunications
• Technique
• Ordinateur
• Engineering
• Electronics
• Technology
• Sciences et techniques
• Techniques

Informations

• Publié par: Hermès - Editions Lavoisier
• Date de parution: 16 juin 2006
• Nombre de lectures: 172
• EAN13: 9782746237445
• Licence : Tous droits réservés
• Langue: Français
• Poids de l'ouvrage: 6 Mo

Extrait

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. Introductio