OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Test de modèles formels en B : cadre théorique et critères de couverture

Behnia, Salimeh. Test de modèles formels en B : cadre théorique et critères de couverture. PhD, Institut National Polytechnique de Toulouse, 2000

[img]
Preview
(Document in French)

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

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

Abstract

Les travaux présentés dans ce mémoire définissent un cadre théorique pour le test de logiciels développés selon la méthode formelle B. Les tests visent à révéler les fautes dues à une mauvaise compréhension ou à une mauvaise modélisation d’un besoin fonctionnel, et complètent ainsi les preuves effectuées pendant le développement formel. Un développement B peut être vu comme une série d’étapes durant lesquelles des modèles de plus en plus concrets de l’application sont construits, le code final pouvant être considéré comme une version compilée du modèle le plus concret. Le cadre théorique de test que nous avons défini est un cadre unifié, indépendant du fait que les résultats de test soient obtenus de l’animation des modèles ou de l’exécution du code. Ce cadre est explicitement lié à la notion du raffinement des modèles B : pour une entrée de test, l’acceptation des résultats fournis par un modèle implique l’acceptation des résultats fournis par les raffinements corrects de celui-ci. Nous définissons ensuite une approche d’analyse structurelle des modèles B. En poursuivant le cadre unifié, notre objectif est de définir des stratégies de couverture qui soient applicables à la fois à un modèle abstrait et à un modèle concret. Ceci a nécessité d’unifier pour les modèles B deux catégories de critères : • critères de couverture des spécifications orientées modèle basés sur la couverture des prédicats avant/après ; • critères classiques de couverture structurelle des programmes basés sur la couverture du graphe de contrôle. A partir de cette unification, nous avons défini un ensemble de critères, ordonnés selon la relation d’inclusion, qui complètent les critères existants.

Item Type:PhD Thesis
Uncontrolled Keywords:
Institution: Université de Toulouse > Institut National Polytechnique de Toulouse - INPT
Laboratory name:
Research Director:
Thévenod-Fosse, Pascale
Statistics:download
Deposited By: admin admin

Repository Staff Only: item control page