Mémoire Online: Spécification et vérification des systèmes critiques (Extension de l’environnement VALID pour la prise en charge du temps réel)

Sommaire: Spécification et vérification des systèmes critiques

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

Extrait du mémoire spécification et vérification des systèmes critiques

CHAPITRE 1: Introduction et Motivation 
1.1 Problématique
La technologie des systèmes mixtes matériels et logiciels en anglais hardware-software (H/S) connaît de nos jours une révolution sans pareille dans tous les domaines technologiques. Le fait de mélanger matériel et logiciel, a donné naissance à des systèmes très complexes (plusieurs millions de composants électroniques et des centaines de milliers de lignes de code et même plus). La conception de tels systèmes, nécessite l’intervention de ressource humaine, financière et technologique très importante.

Aussi important soit-elle, leur modélisation, avant d’être fabriquée permet aux ingénieurs concepteurs de réduire le nombre d’erreurs de conception, connue sous l’appellation de bugs.
Pour veiller au bon fonctionnement de leurs conceptions, ces systèmes doivent être soumis à des processus de validation très rigoureux. Une telle tâche n’est point évidente vue l’accroissement rapide de la complexité et de l’hétérogénéité des nouvelles architectures H/S [Bal97]. Aussi correcte que possible, la conception doit tenir compte de certaines propriétés dites critiques, qui sans leur présence risque d’engendrer une situation de catastrophe sur le plan financier, humain et même de ternir l’image de la compagnie. En général, ces propriétés se répartissent en deux classes : propriétés de performance (durée du cycle de conception par exemple) et propriétés fonctionnelles (problèmes d’interblocage par exemple.)
La conception de composantes H/S d’un système intégré s’effectuait traditionnellement de manière séparée, c’est-à-dire que la partie logicielle obtenue, était exécutée sur le prototype de la partie matérielle. Si les contraintes de la spécification requises pour le système ne sont pas satisfaites par le design, le processus subit des modifications puis il est réitéré dans l’espoir d’obtenir le bon prototype.

Cette technique de validation s’avère être très coûteuse en temps et en coût de réalisation.
Pour parer à de telles inconvenances, plusieurs idées ont émané de la communauté scientifique pour l’élaboration de nouvelles techniques de vérification et d’environnements de co-design groupés sous l’appellation d’outils et techniques CAD (System-level Computer Aid Design) qui, en réalité, sont des plate-formes de modélisation, de validation et de synthèse, surtout de circuits VLSI (Very Large Scale Integration Circuits) [Bry91]. Comme la majeure partie des VLSI sont essentiellement des processeurs, la conception de la partie matérielle et de la partie logicielle est un problème très critique et complexe.
Aussi, compte tenu d’une compétitivité très prononcée dans un marché très ouvert tout produit conçu dans des délais moindres devient la clé du succès de tout projet.

Il est bien connu que les architectures H/S s’apparentent en général avec les systèmes enfouis (embedded), critiques et temps-réel, nécessitant qu’au moment de la phase de validation, une attention très particulière mettant en place des mécanismes de vérification tendant à éviter toute situation malencontreuse.
Au cours des dernières années, la complexité de ces systèmes (Embedded H/S Systems)[Ern98] n’a cessé de se développer. Les progrès technologiques favorables, notamment en terme de finesse de gravure, ont permis de diminuer considérablement leur taille. Cette miniaturisation entraînait incontestablement d’énormes avantages, tant au niveau de leur consommation (électronique grand public : téléphones cellulaires, distributeurs ATM…), de leur puissance et de leur rapidité.
Lors de la conception des systèmes enfouis, la phase de vérification est l’étape la plus longue.
Elle consomme jusqu’à 70 % du temps de conception. La notion de vérification elle-même, date des années soixante avec les travaux de Dijkstra et Floyd. Celle-ci, s’est étalée sur plus de trois décennies de découvertes théoriques extraordinaires qui a vu naître carrément une nouvelle science dite « vérification formelle », qui a vite déclassé certaines techniques traditionnelles telles que la simulation, le testing et les anciennes méthodes de validation. Une prise de conscience de l’importance de la vérification en tant que telle a émergée lors de la médiatisation de l’erreur de conception du Pentium d’Intel en 1994 [Pra95]. La perte a été estimée à plus de 400 millions de dollars. Ce cas n’est pas isolé, puisque de nombreux exemples d’erreurs de conception ont été médiatisées notamment le cas de l’accident lors du premier vol du lanceur européen ARIANE-5[Ari96, RSS96] en 1996 (Figure 1.1) qui a été suivi de la vérification du système complet par des techniques d’interprétation abstraite, ce qui a permis la suppression de certaines erreurs parmi elles, celles ayant entraîné la destruction de la fusée.
………..

Si le lien ne fonctionne pas correctement, veuillez nous contacter (mentionner le lien dans votre message)
Spécification et vérification des systèmes critiques (Extension de l’environnement VALID pour la prise en charge du temps réel) (1,25 Mo) (Rapport PDF)
Vérification des systèmes critiques

Télécharger aussi :

Laisser un commentaire

Votre adresse de messagerie ne sera pas publiée. Les champs obligatoires sont indiqués avec *