La robustesse est un attribut spécifique de la fiabilité qui caractérise la réaction d'un système aux fautes externes. Par conséquent, le test de robustesse consiste à tester un système en présence de fautes ou dans des conditions environnementales stressantes afin d'étudier son comportement lorsqu'il évolue dans un environnement hostile. Le test de robustesse peut être soit empirique ou formel. Les méthodes d'injection de fautes sont très communément utilisées pour évaluer le degré de robustesse d'un système. Cependant, elles ne se basent sur aucun oracle de test pour valider leurs résultats. D'autre part, les méthodes formelles de test de robustesse formalisent et la génération de fautes et le processus d'analyse. Elles présentent cependant quelques limitations par rapport aux types de fautes considérées qui dépendent fortement du modèle fonctionnel du système testé. Le travail que nous présentons dans cette thèse, consiste en un ensemble de propositions qui ont pour objectif de répondre aux défis auxquels font face les approches de test de robustesse existantes. D'abord, nous proposons une approche formelle pour la spécification et la vérification du processus d'injection de fautes. Cette approche consiste à formaliser les fautes injectées par un ensemble de triplet de Hoare et ensuite d'utiliser cette spécification pour vérifier la bonne exécution des campagnes d'injections. Notre seconde contribution concerne la spécification et la vérification des propriétés de robustesse. Nous proposons de formaliser les propriétés de robustesse en utilisant une extension de la logique temporelle linéaire qui permet la spécification de contraintes temps réel (XCTL) et nous proposons un algorithme de test passif qui permet de tester la satisfiabilité de ce type de contraintes sur des traces d'exécution finies. Nous contribuons aussi par une nouvelle approche de test de robustesse. Nous proposons une approche hybride basée sur l'injection de fautes et le test passif. L'injection de fautes est utilisée pour créer des conditions environnementales stressantes, et le test passif permet de vérifier la satisfiabilité des propriétés de robustesse sur les traces d'exécution collectées. Les fautes injectées ainsi que les propriétés de robustesse sont formellement spécifiées. Nous utilisons la logique de Hoare pour la spécification des fautes et la logique XCTL pour la formalisation des propriétés de robustesse. Ce qui nous permet de vérifier à la fois le processus d'injection et les exigences de robustesse en appliquant les approches de test passives proposées dans nos contributions précédentes. Finalement, nous proposons une plateforme de modélisation et de vérification de la robustesse des services Web. Cette plateforme est en réalité une instanciation de notre approche de test de robustesse, adaptée aux services Web. Le choix des services Web est motivé par l'émergence de cette technologie qui tend progressivement à s'imposer comme un standard du paradigme de communication programme-à-programme. Ils fournissent aussi un excellent exemple de systèmes hétérogènes fortement distribués.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00585689 |
| Date | 03 December 2010 |
| Creators | Bessayah, Fayçal |
| Publisher | Institut National des Télécommunications |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0021 seconds