Définition d’un système temps réel

Table des matières

INTRODUCTION
CHAPITRE 1 : INTRODUCTION ET MOTIVATION
1.1 Problème étudié dans la thèse
1.2 Contexte de Nos Travaux
1.3 Plan de la Thèse
CHAPITRE 2 : ETAT DE L’ART
2,1 Introduction
2.2 Méthodes Formelles
2.3 Processus de conception
2.4 Spécification Formelle
2.5 Vérification Formelle
2.6 Vérification du Matériel (Hardware)
2.7 Techniques de Vérification du matériel
2.8 Les spécifications comportementales
2.8.1 Les spécifications Axiomatiques
2.8.2 Les spécifications Logiques
2.8.3 Les spécifications Algébriques
2.9 Explosion des états et Génération de Modèles
2.10 Quelques Exemples Notables de cas vérifiés
2.11 Conclusion
CHAPITRE 3 : DEFINITIONS DE BASE
3.1 Introduction
3.2 Concepts fondamentaux
3.3 Systèmes temps réel
3.3.1 Définition d’un système temps réel
3.3.2 Temps et contraintes temporelles
3.4 Les classes de systèmes temps réel
3.5 L’Approche Synchrone
3.6 L’Approche Flot de Données
3.7 L’Approche Asynchrone
3.7.1 Synchrone / Asynchrone
3.8 Langages et automates
3.9 Les multi-ensembles
3.10 Équivalences de Bisimulation
3.11 Conclusion
CHAPITRE 4 : LES DIAGRAMMES BINAIRES DE DECISION
4.1 Introduction
4.2 Diagrammes De Décision Binaire
4.2.1 Diagrammes De Décision Binaires Ordonnés (OBDD)
4.2.3 Comment Construire les BDDs
4.3 Implantation Informatique Des BDDs
4.3.1 Algorithme De Réduction Des BDDs
4.4 Manipulation Des ROBDDs
4.4.1 L’ approche Depth-First search (profondeur d’abord)
4.4.2 L’approche Breadth-First Search
4.5 Algorithme ITE
4.6 Ordre Des Variables
4.7 Implantation des techniques de représentation et de minimisation des systèmes concurrents
4.8 Conclusion
CHAPITRE 5 : THEORIE DU MODEL-CHECKING
5.1 Introduction
5.2 Modèles Linéaires
5.2.1 La Logique Temporelle Linéaire (LTL)
5.3 Model-checking à la Volée
5.3.1 Les Automates de Büchi.
5.3.2 Quelques définitions de Base
5.4 L’Algorithme du Model-checking d’une Formule de LTL
5.4.1 Transformation d’un graphe de Kripke en un graphe de Buchi
5.4.2 Implémentation de la Procédure du Model-checking
5.4.3 Transformation d’une formule LTL en Automate de Büchi
5.5 Modèles Arborescents
5.5.1 La Logique arborescente CTL
5.5.2 Opérateurs Temporels Auxiliaires
5.5.3 Axiomatisation de la logique CTL
5.6 Model-checking de CTL
5.6.1 Calcul des points fixes de fonctions monotones : une approche pour CTL
5.6.2 Caractérisation des points fixe pour CTL
5.6.3 La génération de Contre-exemples.
5.7 Vérification des Systèmes Temps-réel
5.7.1 Modélisation des systèmes temps-réel
5.7.2 Systèmes de Transitions Temporisées
5.7.3 Composition d’Automates Temporisés
5.7.4 La Logique Temporelle Temporisée (TCTL)
5.7.5 Conclusion
CHAPITRE 6 : LA LOGIQUE DE REECRITURE, MAUDE ET FULL-MAUDE
6.1 Introduction
6.2 La réécriture
6.2.1 Quelques concepts fondamentaux
6.3 Notions de base des systèmes de réécriture
6.3.1 Syntaxe des systèmes de réécriture
6.4 Spécification équationnelle (syntaxe-sémantique)
6.4.1 Notions Générale
6.4.2 La déduction dans les Systèmes de réécriture
6.5 La logique de réécriture
6.5.1 Introduction
6.5.2 Expression de la Logique de Réécriture dans La Théorie des Catégories
6.6 Différents Type d’Algèbres Engendrées par la Réécriture 87
6.6.1 Many Sorted Algebra
6.6.2 Order-Sorted Algebra
6.7 Le Langage Maude
6.7.1 Généralités
6.7.2 Expression des Communications Synchrones et Asynchrones
6.7.3 Caractéristique du Module META-LEVEL et de la Réflexions
6.7.4 Full-Maude
6.8 Conclusion
CHAPITRE 7 : SPECIFICATION DES SYSTEMES TEMPS REEL DANS LE CADRE DE LA LOGIQUE DE REECRITURE
7.1 Introduction
7.1.1 Spécification des systèmes temps réels
7.2 Modèle temporisé
7.3 Expression du temps comme une action
7.4 Logique de réécriture en tant que sémantique pour les systèmes temps réel
7.4.1 Application aux automates temporisés
7.4.2 Systèmes temps-réel orienté-objets
7.4.3 Exemple d’application
7.5 Conclusion
CHAPITRE 8 : PROPOSITION D’UN ENVIRONNEMENT POUR LA MODELISATION DES SYSTEMES REACTIFS
8.1 Introduction.
8.2 Choix d’une méthodologie de modélisation
8.2.1 Choix d’un langage pour la méthodologie
8.3 La notation UML (Unified Modelling Language)
8.3.1 Les bénéfices d’UML
8.3.2 Les Classes
8.3.3 Diagramme de Classes
8.3.4 Diagramme de Séquences
8.3.5 Diagrammes de Collaboration
8.3.6 Diagramme de Statecharts (Diagramme de transitions)
8.3.7 Diagramme d’Activité
8.4 Vue Générale Sur le Langage OCL
8.4.1 POURQUOI OCL?
8.4.2 DANS QUEL CAS UTILISER OCL
8.4.3 Invariants
8.4.4 Expressions Générales
8.4.5 Caractéristiques Prédéfinies sur Tous les Objets
8.4.6 Collection
8.4.7 Valeurs Précédentes dans Les Post-conditions
8.5 Modélisation du système Train-Gate-Controller en UML/OCL
8.5.1 L’approche de modélisation par le langage UML
8.5.2 Spécification de Contraintes en OCL
8.6 L’abstraction des contraintes temporelles en UML/OCL
8.7 Traduction du langage UML vers Maude.
8.7.1 Contraintes: passage de l’OCL vers Maude
8.8 UML et le temps réel
8.8.1 Une représentation limitée du temps
8.8.2 Illustration d’UML pour la Modélisation des Systèmes Temps réel
8.8.3 Une approche pour la Spécification des Systèmes temps-réel en UML
8.8.4 Spécification des Systèmes Temps-réel
8.8.5 Spécification de l’Extension du Langage UML
8.8.6 Exemple de Spécification-Stéréotypes
8.9 Conclusion
CHAPITRE 9 : IMPLANTATION
9.1 Introduction
9.2 Module de Spécification et de Simulation des Systèmes Réactifs
9.2.1 Le Système VALID
9.2.2 Processus de Modélisation dans VALID
9.3 Simulation et Animation dans VALID 2
9.4 Transformation de Spécifications VALID en MAUDE
9.4.1 Vérification de la terminaison et de la confluence de la spécification.
9.4.2 Génération de Code MAUDE à Partir de Spécifications VALID
9.5 Proposition d’un Model Checker basé sur la Logique Temporelle PTL
9.6 Expérimentation
9.6.1 Exemple de Spécification d’un Système Hardware
9.6.2 Exemple de Spécification d’un Software
9.7 Conclusion
Conclusion et Perspectives
Bibliographie
Annexe A
Annexe B