Co-design et raffinement en B : BHDL Tool, plateforme pour la conception de composants numériques
- Systèmes, Conception de -- Fiabilité
- Génie logiciel
- Langages formels
- Logiciels -- Développement
- Circuits intégrés numériques -- Conception et construction -- Informatique -- Fiabilité
- VHDL (langage de description de matériel informatique)
- Systèmes enfouis (informatique)
- Méthode B (informatique)
- Méthodes formelles (informatique)
- Conception conjointe
- Langages d'entrée de conception
- Raffinement
- Système C (informatique)
- Langue : Français
- Discipline : Informatique
- Identifiant : Inconnu
- Type de thèse : Doctorat
- Date de soutenance : 01/01/2004
Résumé en langue originale
Dans le cadre de la modélisation de systèmes complexes, la conception d'entrée ou appelée système représente le plus haut niveau d'abstraction du système global, ceci avant tout choix en terme d'implantation et de technologies. A ce tout premier stade de la conception, l'utilisation d'un langage formel de spécification est de plus en plus considéré comme le fondement d'un réel processus de validation en particulier dans le cas d'exigences de sûreté. Cette thèse met en lumière la nécessité d'une modélisation par raffinement : de la spécification la plus abstraite vers un point de description proche de l'implémentation afin d'assurer (1) la traçabilité des besoins et des exigences, (2) une meilleure gestion du développement et (3) surtout une conception sûre des systèmes car générée par construction prouvée et ceci que ces sytèmes fassent appel à des technologies logicielles, numériques ou analogiques, voire autres. Le travail qui a été mené a consisté à mettre en perspective la taxinomie des langages ADL, le modèle de développement utilisé dans le cadre des composants électroniques et la méthode par raffinement, dite Méthode B. Ceci nous a permis de réaliser la plateforme BHDL Tool : plateforme de conception de circuits électroniques intégrant (1) une interface de description structurelle de composants électroniques, (2) un générateur de code VHDL et enfin (3) un traducteur en un langage formel pour les preuves de raffinement sous l'Atelier B.
- Directeur(s) de thèse : Devienne, Philippe - Tison, Sophie
AUTEUR
- Aljer, Ammar