Le système Z/EVES

Table des matières

Remerciements
Résumé
Listes diverses
Introduction
1 Aperçu sur les applications des méthodes formelles
1.1 Approches générales
1.2 Historique 
1.3 Référentiel normatif 
1.3.1 Domaine aéronautique
1.3.2 Domaine spatial
1.3.3 Domaine ferroviaire
1.3.4 Domaine automobile
1.3.5 Domaine nucléaire
1.4 Utilisation actuelle et tendance
1.4.1 Analyse des données
1.4.2 Résultats
2 Notions de base du langage Z
2.1 Logique propositionnelle et logique des prédicats
2.1.1 Logique propositionnelle
2.1.2 Logique des prédicats
2.2 Théorie des ensembles 
2.2.1 Rappel
2.2.2 Extension Z de la théorie des ensembles
2.3 Relations
2.3.1 Notions générales
2.3.2 Fonctions
2.4 Schémas 
2.4.1 Taxonomie et morphologie des schémas
2.4.2 Notation des schémas
2.4.3 Interaction des schémas
2.4.4 Aide à la présentation
2.4.5 Schémas génériques
2.5 Object-Z 
3 Modélisation formelle du noyau
3.1 Introduction 
3.2 Types primaires 
3.2.1 Processus
3.2.2 Registres
3.2.3 Interruption
3.3 Abstractions nécessaires
3.4 Gestion des priorités
3.5 Processus courant et processus prêts 
3.6 Messages et sémaphores 
4 Preuves automatiques du modèle en utilisant Z/EVES
4.1 Introduction 
4.2 Expansion d’un schéma 
4.3 Vérification de la syntaxe et de la cohérence des types
4.4 Analyse de l’application des fonctions dans leur domaine 
4.5 Vérification des conditions initiales 
4.6 Théorème des préconditions 
Conclusion
Annexes
Annexe 1
Annexe 2