Vérification du Matériel (Hardware)

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

Vérification du Matériel (Hardware)

L’importance de la vérification du matériel. La prévention du risque d’erreur dans la conception du hardware est vitale pour toute entreprise. Le hardware a toujours été sujet à un coût de fabrication très élevé. La découverte d’un défaut de fabrication après la distribution d’un produit risque de coûter très chère à l’entreprise en question. Le fait de rappeler le produit pour le corriger certes de nos jours une telle situation est acceptée par le client, mais entraîne en général la banqueroute de l’entreprise si ce n’est plus grave. Nous pouvons avoir une idée sur les conséquences d’une telle débâcle, justement sur le cas du rappel et la correction du processeur Pentium II, qui a causé une perte sèche de 475 Millions de Dollars à Intel.
L’un des indicateurs de l’évolution du nombre de portes logiques (logical gates) dans un circuit, la très célèbre loi de Moore, d’ailleurs de tout temps vérifiée en pratique vraie, atteste que ce nombre à tendance à doubler tous les 18 mois ce qui est par conséquent un obstacle de taille pour fabriquer des produits corrects. Certaines études empiriques ont indiqué que plus de 50% des ASICs (ApplicationSpecific Integrated Ciruit) au début de leur design et fabrication ne fonctionnent pas normalement.
Donc, il n’est pas surpris de voir des manufactures investir des sommes colossales pour que leurs produits soient dépourvus d’erreurs, ce qui constitue en soit l’importance qu’on donne aux méthodes de vérification qui sont d’ailleurs une partie très importante est bien-établie dans le processus de conception. Nous constatons aussi que 27% des efforts consentis au processus de conception sont en générale réservés au design lui-même, le reste soit à peu prêt 73% du temps est réservé à la phase de vérification, c’est-à-dire, la recherche et la prévention des bugs.

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

De nombreuses définitions ont été données pour les systèmes temps réel, nous nous consacrerons à celle qui sera fournit ci-après. De plus amples explications formelles seront étayées par la suite.
Définition 3.1 (Système temps réel) Un système temps réel est un système dont l’exactitude (correctness) dépend non seulement des résultats logiques, mais également des instants où ces  résultats sont fournis.
Cette définition permet de mettre de côté les définitions courantes qui s’attachent à le définir aussi comme un système constitué de processus dont l’exécution est très rapide. Un système ayant des délais à respecter exprimés en heures peut être considéré comme un STR (Chaudières à vapeur par exemple).
Ce n’est donc pas uniquement la « rapidité des temps de réponse » (au sens valeurs très faibles des durées) qui caractérise un STR. Néanmoins, la plupart des STR ont des temps de réponse exprimés en milli-secondes (ms). Le respect de telles contraintes de promptitude rend complexe le développement des systèmes et constitue une des caractéristiques importantes des STR.
Cette définition s’explique essentiellement par le fait que les STR sont des systèmes appartenant à la classe des systèmes dits réactifs. Par exemple, et de manière simplifiée, le rôle du système réactif de pilotage automatique d’un avion sera justement d’empêcher sa chute, c’est-à-dire de le maintenir à une altitude tolérable (ce que nous appelons le comportement maîtrisé).

Télécharger le rapport complet