Soutenance mémoire
1 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ériï¬cation des systèmes embarqués
4.1 Introduction
4.2 Vériï¬cation 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ériï¬cation formelle
4.3.1 Approches de vériï¬cation formelle
4.3.2 Apport des méthodes formelles à la conception conjointe
4.4 Vériï¬cation 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éciï¬cations formelles
5.1 Introduction
5.2 Les trois familles des langages de spéciï¬cations formelles
5.2.1 Langages de spéciï¬cations exécutables mais pas prouvables
5.2.2 Langages de spéciï¬cations prouvables mais pas exécutables
5.2.3 Langages de spéciï¬cations exécutables et prouvables
5.3 Outils pour la vériï¬cation 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
Rapport PFE, mémoire et thèse avec la catégorie modèles formels
|
|
Étudiant en université, dans une école supérieur ou d’ingénieur, et que vous cherchez des ressources pédagogiques entièrement gratuites, il est jamais trop tard pour commencer à apprendre vous trouverez ici des centaines de rapports pfe spécialement conçu pour vous aider à rédiger votre rapport de stage, vous prouvez les télécharger librement en divers formats (DOC, RAR, PDF).. Tout ce que vous devez faire est de télécharger le pfe de Bestpfe.com et ouvrir le fichier pfe PDF ou pfe DOC. Ce programme spécifique est classé dans la catégorie méthodologie de conception automatique où vous pouvez trouver quelques autres mémoires informatique similaires.
Actuellement, de plus en plus de gens sont prêts à partager leurs travaux pfe, mémoire, thèse.. avec les autres et ils ne veulent pas de compensation pour cela. Le rapport une méthodologie de conception automatique de modèles formels pour des déscriptions SystemC est un rapport complet pour aider les autres étudiants dans leurs propres travaux. |
Outils pour la vérification formelle
Nous présentons dans cette sections les deux outils de vérification formelle qui peuvent être utilisés pour la vérification formelle des spécifications SYSTEMC traduites en SIGNAL.
Coq
Coq est un outil de preuve développé par le Projet LogiCal à l’INRIA. La spécification dans le langage Coq est basée sur une logique d’ordre supérieur appelé Calcul des Constructions et les principales fonctionnalités de Coq sont au niveau du formalisme :
• Une structure primitive de définitions mutuellement inductives permettant des spécifications de haut niveau, fonctionnelle et relationnelle.
• Une structure primitive de définitions co-inductives permettant de représenter directement des structures infinies.
• Une interprétation des preuves comme des programmes certifiés mise en oeuvre dans une compilation des preuves sous forme de programmes ML.
Spécification syntaxique dans Coq
Le langage de spécification de l’assistant Coq permet de définir des types de données structurés en utilisant les définitions inductives. Les arbres de syntaxe abstraite se codent naturellement dans Coq comme des types de données structurés et les concepts importants de la définition d’une syntaxe abstraite sont les opérateurs et les types.
Spécification sémantique dans Coq
La spécification de la sémantique opérationnelle d’un langage de programmation en Coq, peut se faire de deux manières différentes, soit en utilisant l’approche fonctionnelle, soit en utilisant l’approche relationnelle. Dans les deux cas, on peut développer des preuves sur ces spécifications (nécessite une très bonne connaissances de Coq) en utilisant par exemple l’environnement Pcoq.
Approche relationnelle Dans cette approche, la spécification de la sémantique opérationnelle est donnée par des relations (ou des prédicats) inductives de type Prop (type des propositions en Coq).
Approche fonctionnelle Dans cette approche, la spécification de la sémantique opérationnelle est donnée par des fonctions récursives et non récursives.
Présentation de l’environnement Pcoq
Pcoq [?] fournit un environnement de travail pour le système de preuve Coq, il est construit et maintenu par l’équipe Lemme à l’INRIA. Il réunit les caractéristiques suivantes :
• Interface graphique.
• Séparation entre l’interface et le système de preuves : l’interface graphique et Coq sont deux processus indépendants.
• Des mécanismes d’édition et de présentation structurées.
• Proof by pointing : L’environnement utilise la structure des formules logiques pour aider l’utilisateur à effectuer les étapes du raisonnement en les désignant à la souris.
• écrit en Java et en Ocaml, Pcoq bénéficie de leurs portabilités combinées.
• Langue naturelle : les preuves en cours de développement peuvent être visualisées sous forme d’un texte en français ou en anglais, sur lequel les mécanismes de proof-by-pointing fonctionnent.
Télécharger le rapport complet
