Spécification syntaxique dans Coq

Table des matières

Introduction
I Conception et vérification des systèmes embarqués
2 Flot de conception des systèmes embarqués
2.1 Introduction
2.2 Systèmes embarqués
2.2.1 Caractéristiques d’un système embarqué
2.2.2 Contraintes temps réel
2.2.3 Architecture des systèmes embarqués
2.3 Flot de conception d’un système embarqué
2.3.1 Flot de conception de base
2.3.2 Flot de conception modulaire
2.3.3 Flot de conception à base d’IPs
2.4 Flot de conception des systèmes sur puces
2.4.1 Flot de conception logiciel pour les systèmes sur puces
3 SYSTEMC, un langage de conception au niveau système
3.1 Introduction
3.2 Présentation du langage SYSTEMC
3.2.1 Historique
3.2.2 Objectifs
3.3 Architecture de SYSTEMC
3.4 Les particularités de SYSTEMC
3.5 Principaux composants SYSTEMC
3.5.1 Les modules
3.5.2 Les processus
3.5.3 Les Ports
3.5.4 Les Interfaces
3.5.5 Les Canaux
3.6 Simulation par SYSTEMC
3.6.1 Le modèle du temps
3.6.2 Le Noyau SYSTEMC
3.7 Exemple de description en SYSTEMC
3.8 conclusion
4 Vérification des systèmes embarqués
4.1 Introduction
4.2 Vérification par simulation
4.2.1 Étapes d’exécution d’un simulateur
4.2.2 Le compilateur
4.2.3 Génération du programme simulable
4.2.4 Exécution de la simulation
4.3 Vérification formelle
4.3.1 Approches de vérification formelle
4.3.2 Apport des méthodes formelles à la conception conjointe
4.4 Vérification des systèmes décrits en SYSTEMC
4.4.1 Techniques de validation de modèles SYSTEMC
4.4.2 Intégration des méthodes formelles dans les flots de conception
4.5 Conclusion
II Transformation de descriptions SYSTEMC en modèles formels
5 Etat de l’art sur les langages de spécifications formelles
5.1 Introduction
5.2 Les trois familles des langages de spécifications formelles
5.2.1 Langages de spécifications exécutables mais pas prouvables
5.2.2 Langages de spécifications prouvables mais pas exécutables
5.2.3 Langages de spécifications exécutables et prouvables
5.3 Outils pour la vérification formelle
5.3.1 Coq
5.3.2 SIGALI
5.4 Conclusion
6 SIGNAL, un langage formel synchrone
6.1 Introduction
6.2 Conception synchrone des systèmes réactifs
6.2.1 Les systèmes réactifs
6.2.2 Caractéristiques des systèmes réactifs
6.2.3 Modèles synchrones pour systèmes réactifs
6.3 Le formalisme synchrone
6.4 Hypothèse synchrone
6.4.1 Concepts de base
6.5 Polychrony, un environnement synchrone pour la conception des systèmes
6.6 Le paradigme synchrone
6.6.1 Le style impératif : ESTEREL et SYNCCHARTS
6.7 Langage SIGNAL
6.7.1 Exemple de modélisation en SIGNAL
6.7.2 Les éléments de base du langage SIGNAL : les signaux
6.7.3 Les opérateurs de signaux
6.7.4 Compilation de SIGNAL
6.8 Conclusion
7 Transformation de descriptions SYSTEMC en modèles formels de SIGNAL
7.1 Introduction
7.1.1 Présentation générale de l’approche proposée
7.1.2 Restriction syntaxique et hypothèses
7.2 Préliminaires
7.2.1 Graphe de flot de données
7.2.2 Graphe de flot de contrôle
7.2.3 Le formalisme Static Single Assignment
7.3 Phase d’extraction structurelle
7.4 Phase d’extraction comportementale
7.4.1 Transformation des types de données
7.4.2 Transformation des opérateurs et des fonctions standards
7.4.3 Transformation des blocs SSA
7.4.4 Transformation de la fonction PHI
7.4.5 Transformation des expressions conditionnelles
7.4.6 Transformation des expressions d’affectation
7.4.7 Transformation des boucles
7.4.8 Transformation des modules
7.5 Codage des pointeurs SYSTEMC en SIGNAL
7.5.1 Présentation du problème
7.5.2 Lecture des pointeurs (load)
7.5.3 Écriture des pointeurs (store)
7.6 Conclusion
8 Implémentation
8.1 introduction
8.2 Format intermédiaire SSA
8.3 Le compilateur GCC-4.1.0
8.4 Adaptation du Compilateur GCC-4.1.0
8.5 L’outil de transformation SC2SIG
8.6 Exemples de traduction
8.6.1 Exemple 1
8.6.2 Exemple 2 : Finite Impulse Response
8.7 Compilation des modèles SIGNAL
8.7.1 Compilation en code C exécutable
8.7.2 Compilation en format Z3Z
8.8 Conclusion
9 Conclusion et perspectives
Bibliographie