OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Développement prouvé de composants formels pour un générateur de code embarqué critique pré-qualifié

Izerrouken, Nassima. Développement prouvé de composants formels pour un générateur de code embarqué critique pré-qualifié. PhD, Institut National Polytechnique de Toulouse, 2011

[img]
Preview
(Document in French)

PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
2MB

Official URL: http://ethesis.inp-toulouse.fr/archive/00001777/

Abstract

Nous nous intéressons au développement prouvé de composants formels pour un générateur de code pré-qualifié. Ce dernier produit un code séquentiel (C et Ada) pour des modèles d'entrée qui combinent les flots de données et de contrôle et qui présentent des possibilités d'exécution concurrente (Simulink/Stateflow et Scicos). Le développement prouvé permet de réduire le coût des tests et d'augmenter l'assurance des outils développés avec cette approche vis-à-vis de la qualification. Les phases de spécification, de développement et de vérification des outils développés sont effectuées avec l'assistant de preuve Coq. Ce dernier permet d'extraire le contenu calculatoire des composants en préservant les propriétés prouvées en Coq. Ce code extrait est ensuite intégré dans une chaîne complète de développement (chaîne de GeneAuto). Nous présentons un cadre formel, inspiré de l'analyse statique, qui s'appuie sur la sémantique abstraite et qui est instanciable sur plusieurs composants du générateur de code. Nous nous basons sur les ensembles partiellement ordonnés et sur le calcul de point fixe pour définir le cadre et effectuer les différentes analyses des composants du générateur de code. Ce cadre formel comporte toutes les preuves communes aux composants et indépendantes des analyses effectuées. Deux composants sont étudiés : l'ordonnanceur et le typeur des modèles d'entrée.

Item Type:PhD Thesis
Uncontrolled Keywords:
Institution: Université de Toulouse > Institut National Polytechnique de Toulouse - INPT
Laboratory name:
Research Director:
Sallé, Patrick
Statistics:download
Deposited By: admin admin
Deposited On:21 Nov 2012 12:37

Repository Staff Only: item control page