LogoLogo

Nasr, Odile. Spécification et vérification des ordonnanceurs Temps Réel en B

Nasr, Odile (2007). Spécification et vérification des ordonnanceurs Temps Réel en B.

[img]PDF - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
3598Kb

Résumé en francais

L'objectif de cette thèse est de proposer une démarche de spécification et de validation des ordonnanceurs temps réel. Le modèle à analyser et les politiques d'ordonnancement sont exprimés à l'aide du langage Cotre. Ce dernier peut être considéré comme un langage de description d'architecture permettant la description formelle du comportement d'un système, ainsi que les contraintes à respecter. La vérification du système ordonnancé repose sur la traduction du modèle en automates temporisés. Notre modélisation des ordonnanceurs préemptifs devant être traduite en Uppaal, ne doit gérer le temps qu'à travers des horloges. Nous cherchons ensuite à valider notre modélisation en utilisant la méthode B. Pour cela, nous avons débuté par une spécification abstraite des ordonnanceurs, et nous l'avons raffiné par étapes successives afin de prendre en compte les caractéristiques des automates temporisés. Nous avons ensuite vérifié la hiérarchie des raffinements en prouvant les différentes obligations de preuve générées. Afin de traduire la modélisation B des ordonnanceurs en Uppaal, nous avons défini un langage B0_Uppaal et des règles à respecter lors de la transformation. Cette traduction est enfin vérifiée par des propriétés d'ordonnançabilité exprimées en logique CTL.

Sous la direction du :
Directeur de thèse
Bodeveix, Jean-Paul
Filali, Mamoun
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :Temps réel - Ordonnancement - Spécification - Vérification - Méthodes Formelles - Méthode B - Raffinement - Logiques Temporelles et Temporisées - Automates Temporisés - Uppaal
Sujets :Informatique
Déposé le :16 Jan 2008 15:28