Une approche complémentaire de test de robustesse basée sur l'injection de fautes et le test passif, A complementary approach for testing system robustness based on passive testing and fault injection techniques

Fayçal Bessayah

Description

Sous la direction de Ana Cavalli
Thèse soutenue le 03 décembre 2010: Institut national des télécommunications d'Evry
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.
-Test de robustesse
-Injection de fautes
Robustness is a specialized dependability attribute, characterizing a system reaction with respect to external faults. Accordingly, robustness testing involves testing a system in the presence of faults or stressful environmental conditions to study its behavior when facing abnormal conditions. Testing system robustness can be done either empirically or formally. Fault injection techniques are very suitable for assessing the robustness degree of the tested system. They do not rely however, on formal test oracles for validating their test. On the other hand, existing formal approaches for robustness testing formalize both the fault generation and the result analysis process. They have however some limitations regarding the type of the handled faults as well as the kind of systems on which they can be applied. The work presented in this thesis manuscript aims at addressing some of the issues of the existing robustness testing methods. First, we propose a formal approach for the specification and the verification of the fault injection process. This approach consists in formalizing the injected faults as a set of Hoare triples and then, verifying the good execution of the injection campaigns, based on a passive testing algorithm that checks the fault specification against a collected injection trace. Our second contribution focuses on providing a test oracle for verifying real time constraints. We propose a passive testing algorithm to check real time requirements, specified as a set of XCTL (eXplicit Clock Temporal Logic) formulas, on collected execution traces. Then, we propose a new robustness testing approach. It is a complementary approach that combines fault injection and passive testing for testing system robustness. The injected faults are specified as a set of Hoare triples and verified against the injection trace to validate the injection process. The robustness requirements are formalized as a set of XCTL formulas and are verified on collected execution traces. This approach allows one to inject a wide range of faults and can be used to test both simple and distributed systems. Finally, we propose an instantiation of our robustness testing approach for Web services. We chose Web services technology because it supports widely distributed and heterogeneous systems. It is therefore, a very good application example to show the efficiency of our approach.
Source: http://www.theses.fr/2010TELE0030/document

Informations

• Publié par: Thesee
• Nombre de lectures: 45
• Langue: English
• Poids de l'ouvrage: 2 Mo

Extrait

Ecole Doctorale EDITE



Thèse présentée pour l’obtention du diplôme de
Docteur de Télécom & Management SudParis


Doctorat conjoint Télécom & Management SudParis et Université Pierre et Marie Curie


Spécialité :

Informatique


Par

Fayçal Bessayah

Titre

Une Approche Complémentaire de Test de Robustesse
Basée sur l’Injection de Fautes et le Test Passif

Soutenue le 3 décembre 2010 devant le jury composé de :


Nina Yevtushenko Université d’Etat de Tomsk Rapporteur
Ismael Rodríguez Laguna Université Complutense de Madrid Rapporteur
Fatiha Zaidi Université Paris-Sud XI Examinateur
Sébastien Tixeuil Université Pierre et Marie Curie Examinateur
Eliane Martins Université d’Etat de Campinas Co-Encadrant
Ana Cavalli IT/Telecom SudParis Directrice de thèse



Thèse n° 2010TELE0030


tel-00585689, version 1 - 13 Apr 2011



Doctoral School EDITE

Thesis submitted for obtaining the

PHD DEGREE IN COMPUTER SCIENCE
Doctorate jointly delivered by
Telecom & Management SudParis and Pierre et Marie Curie
University- Paris 6

Speciality:

COMPUTER SCIENCE

Presented by
Fayçal Bessayah

Title
A Complementary Approach for Testing System
Robustness Based on Passive Testing and Fault Injection
Techniques


Committee in charge :
Nina Yevtushenko Reviewer Tomsk State University
Ismael Rodríguez Laguna Reviewer Complutense University of Madrid
Fatiha Zaidi Examiner Universisty of Paris-Sud XI
Sébastien Tixeuil Examiner Pierre et Marie Curie University
Eliane Martins Co-advisor State University of Campinas
Ana Cavalli Co-advisor IT/Telecom SudParis
tel-00585689, version 1 - 13 Apr 2011also
A
man

and
kno
of
wledgmen
arouk
ts
all
I
of
w
tor
ould
Willy
lik
Thanks
e
not
to
ort.
thank
made
Professor
to
Ana
Ro
Ca
Professor
v
in
alli
Mazen
for
Mohamed
her
Mme.

part
t
thank
supp
and
ort
ving
and
all
dedi-
e

t.
during
ev
all
evtushenk
the
S?bastien
time
Professor
I
alli.
sp
y
en
Bakr
t
F
w
laouiti,
orking
ablo
on
har
this
Brigitte
PhD
allet
thesis.
the
I
w
am
ould
v
m
ery
and
grateful

for
lot.
the
m
time
and
she
suggestions
sp
impro
en
qualit
t
do
helping
thanks
me
y
and

guiding
Nina
m
Professor
y
Laguna,

Do
hes.
atiha
I
Martins
w
Ca
ould
y
lik
all
e
and
also
particular
to
Wissam
thank
Mounir
her
e
for
Maarabani,
gran
Morais,
ting
Jose
me
Mohamed
the
and
freedom
eh
of
to
dev
t
eloping

m
their
y
ort
ideas

and
m
for
Last
her
I
suggestions
e
and
y

grandmother
throughout
y
this
Nassim,
w
for
ork.
and
A
a
sp
ha
ecial
read
thanks
y
also

to
for
m
the
y
she

to
Professor
v
Eliane
the
Martins
y
from
this
the

State
More
Univ
go
ersit
m
y
thesis
of
aluation
Campinas,

for
Professor
her
Y

o,
and
Ismael

dr?guez
in
Professor
preparing
Tixeuil,
this

thesis.
F
I
Zaidi,
really
Eliane
learned
and
a
Ana
lot
v
of
Man
things
thanks
b
to
y
m
w
friends
orking

with
no
her
order,
and
Sarakbi,
b
Mallouli,
eneted
Jimenez,
from
Lallali,
her
elip
exp
lalanne,
erience
Al
as
Anis
w
Anderson
ell
F
as
Aissanou,
her
P


t
Ahmed

Sidi
h

and
W

bi.
hnical
also
skills.
Mme.
I
Lauren
w
and
ould
Jo
lik
V
e
for
also
help
to
supp
thank

Do
non

hnical
Amel
of
Mammar
y
a
ork.

and
at
least,
T
w
elecom
lik
SudP
to
aris
m
who
mother,
help
y
ed
and
me
m
and
brothers

sisters
me
Souad
a
Radia
lot.
their
A
t
particular
supp
thanks
Thanks
to
her
for
tel-00585689, version 1 - 13 Apr 2011syst?me
R?sum?
le
Que
he

test.
soit
don
dans

le
la
domaine
requ?rir
des

transp
si
orts,
t,
des
actif
?nergies
breuses
ou
t
des
de
banques,
?cier
les

syst?mes
elopp
informatiques
test
son
la
t
v
immanquablemen
de
t
les
pr?sen
un
ts.
ec
Nous
de

syst?mes

in
que
t
nous
able.
a
formelles
v
or-
ons
p
de
tation
plus
p

du
her,
est
?
ermet
sa
ni
v
r?f?rence.
oir
de
nos
test
vies

et
aux
nos
de
biens,
test
?
au
des
tests
programmes
observ
informatiques.
de
P
g?n?ration
arall?lemen
?t?
t,
t

applicatifs
v
de
a
ec
sans
un
dire
rigoureux
que
fait,

p
syst?mes
m?tho
son
our
t
propri?t?s
de
tes
plus
mais
en
v
plus
sur

L'utilisation
Une
des

de
due
une
essen
de
tiellemen
l'ob
t
r?aliser
?
qui
une
v
expansion
pro
sans
ond
pr?c?den

t

de
a
syst?mes
breux
largemen
sur
t

distribu?s
p
et
l'ensem
h?t?rog?nes.
tra
Sans
deux
parler
m?tho
de
actif
l'utilisation
des
d'In
Le
ternet
?

sous

ble
r?seau
?
de
ortemen
transp
a
ort
sp
de
De
donn?es,
des
partag?
de
par
on
un
os?es
nom
Elles
bre
t


de
en
services
yp
et
ouv
d'applications
a
W
tation
eb.
er
F
raisonnemen
ace
plus
?
et



plus

On
te,
eut
tout
aux

des
t,
p
m?me
sp
temp
les
oraire,
imp
de
tan

du
syst?mes
test?,
p
aussi
eut
our
a
?rier
v
propri?t?s
oir
l'implan
de
nale.
lourdes
de

m?tho
?conomiques,
a
v
ermis
oire
d?v
dans
er

th?orie

test
h

umaines.
t
An

de
de
s'assurer
un
de
fonctionnel
la
p
abilit?
de
de
?rier
tels
le
syst?mes,
duit
il

imp
?
orte
sp
donc
de
de
La
v
herc
?rier
acad?mique
leurs
publi?

nom
ortemen
tra
ts
aux
de
le
la
de
mani?re
Globalemen
la
on
plus
eut
rigoureuse
er
p
ble
ossible.

L'utilisation
v
des
en
m?tho
grandes
des
les
formelles
des
p
test
our
et
le
m?tho
test
de
de
passif.

test
est

probablemen
appliquer
t
syst?me

test
qu'il
ensem
y
de
a
et
de

plus

s?r
t
en
?
mati?re
v
de
la


hniques
r?f?rence.
de
nom
v
m?tho

de

automatique
s'explique
tests
sans

doute
t
par
prop
les
dans
fondemen
litt?rature.
ts
traiten
math?matiques
g?n?ralemen
sur
des
lesquels
proto
se
et
basen
r?actifs
t
fa