Unfolding based verification of concurrent infinite-state systems

The Quang Tran

Description

Sous la direction de Igor Walukiewicz
Thèse soutenue le 19 juin 2009: Bordeaux 1
Nous proposons une technique de dépliage pour vérifier les systèmes concurrents infinis bien structurés. Certaines propriétés d'intérêt comme la bornitude, la couverture et la terminaison sont décidables grâce à la bonne structure de ces systèmes. D'autre part, le dépliage réduit efficacement l'explosion combinatoire en exploitant l'ordre partiel entre les événements des systèmes concurrents. Nous proposons une modélisation par structure d'événements pour des systèmes bien structurés élémentaires, tels les compteurs et les files de communication. Le dépliage d'un réseau de structures d'événements étant une structure d'événements, nous proposons ensuite une approche hiérarchique à la modélisation et à la vérification des systèmes, qui préserve la bonne structure. Enfin, nous proposons une technique d'élimination des événements redondants. La mise en œuvre de notre approche dans l'outil ESU nous permet de conclure à son efficacité.
-Algorithme de dépliage
-Ordre partiel
-Préordre
-Produit synchronisé
-Structure d'événements
-Préfixe fini
-Système infini
-Bornitude
-Terminaison
-Quasi-vivacité
We propose an unfolding technique for verifying concurrent infinite-state systems that are well-structured. Some properties of interest such as boundedness, coverability and termination are decidable thanks to the well-structure of these systems. Moreover, the unfolding effectively reduces the combinatorial explosion by exploiting the partial order between events of concurrent systems. We propose a modelization using event structures for basic well-structured systems, such as counters and communication channels. As the unfolding of a synchronized product of event structures is an event structure, we obtain a hierarchical approach to modeling as well as to verifying systems, which preserves the well-structure. Finally, we propose a technique for eliminating redundant events. The implementation of our approach in the ESU tool allows us to conclude on its efficiency.
-Unfolding algorithm
-Partial order
-Preordre
-Infinite-state system
-Synchronized product
-Event structure
-Finite prefix
-Boundedness
-Termination
-Quasi-liveness
Source: http://www.theses.fr/2009BOR13832/document

Sujets

• Relation d'ordre
• Pré-ordre
• Borne (mathématiques)
• Désinence

Informations

• Publié par: Thesee
• Nombre de lectures: 236
• Langue: Français
• Poids de l'ouvrage: 1 Mo

Extrait

ENSEIRB
MM.
Claude
N
PR.
d'ordre
CNRS/LaBRI
:
an
3808

THÈSE
de
présen
Grégoire
tée

à
ants
L'UNIVERSITÉ

BORDEA
CR.
UX
1
1
Hadd
ÉCOLE

DOCTORALE
ENS
DE
Igor
MA
de
THÉMA

TIQUES
PR.
ET
han/Bretagne
INF
le
ORMA
de
TIQUE
Ber
par
Bruno
e
Univ.
atoir
hel
or
d'Orléans
ab
PR.
L
han
Sutre
u
Grégoire
Jard
et

u
CR.
Herbretea


e
F
Igor
p
adr
our
han
obtenir
Jard
LE
ENS
GRADE

DE
Dev
DOCTEUR
t
Sp
jury
écialité:
osé
INF
:
ORMA
Bernard
TIQUE
thomieu
Unfolding
CNRS/LAAS
Based
Cour
V
PR.

Bordeaux
of
Jean-Mic
Concurren
Couvreur
t
Univ.
Innite-State
Serge
Systems
ad
Souten
ENS
ue

le
F
19
Herbretea
juin,
MC.
2009
Claude
Après
PR.
a
de
vis
han/Bretagne
des
Sutre
rapp
CNRS/LaBRI
orteurs
W
:
DR.
MM.
Dir
Serge

Hadd
thèse
ad
W
PR.
Co-enc
ENS
LaBRI
de
de
◦
Thế QuangTrầnénemen

prop
des

systèmes
et

÷uvre
ts

innis
d'év
par


préserv
hnique
énemen
de
ESU
dépliages
préordre,
Résumé:
terminaison,
Nous
d'un
prop
t
osons
osons
une
à


hnique
onne
de
hnique
dépliage
ts.
p

our
de
v
de
érier
duit
les
prexe
systèmes
les

Le

de
ts
ts,
innis

bien
nous

une
Certaines

propriétés
mo
d'in
la
térêt
systèmes,

la
la
Enn,
b
une
ornitude,
des
la
re-

mise
erture
notre
et
dans
la
p
terminaison
à
son

t
ordre

inni,
grâce

à
énemen
la
b
b
acité.
onne
de

unication.
de
dépliage

réseau
sys-

tèmes.
énemen
D'autre
étan
part,
une
le
d'év
dépliage
ts,
réduit
prop

ensuite
t
appro
l'explosion
he

hique
binatoire
la
en
délisation
ex-
à
ploitan
v
t
des
l'ordre
qui
partiel
e
en
b
tre

les
nous
év
osons
énemen

ts
d'élimination
des
év
systèmes
ts

dondan
ts.
La
Nous
en
prop
de
osons
appro
une
he
mo
l'outil
délisation
nous
par
ermet


d'év
son
énemen
Mots
ts
algorithme
p
dépliage,
our
partiel,
des
système
systèmes
pro
bien
syn-

hronizé,
élémen-
d'év
taires,
ts,
tels
ni,
les
ornitude,

quasi-viv
et
Vérication
leservisor
friends.
and

thesis.
kno
of
wledgmen
his
ts
ha
My
m
foremost
for
gratitude
has
go
toine
es
tongue
to
hel
m
b
y
a

for
Igor

W
e

of
for
Mouyssinat.
his
I

that
Despite
e
his
m

Berthomieu,
wded
and
sc
to
hedule,
jury
he
t
alw
and
a
particularly
ys
een
found
ths.
some
Griaut,
time
also
to
the
help
Metho
me
A
to
addressed
o
ok
v
b

wish
problems.
h
His
ery
help
I
w
to
as
wing
really
m

to
t

to
Serge
write
Jard
this
kindly
thesis.
e
I
of
wish
review
to
imp
also
is
thank
time
m
e
y
gratitude.
t
Bruno
w
ving
o
y
rst
six

to
André
,
Arnold
Olivier
and
friendship.
Jean-Mic
ould
hel
thank
Couvreur
b
although
F
w
gr
e
aBRI
had
ecial
not
b
m

uc
has
h
after
time
a
to
there
w
help.
ork
thank
together.
another
I
of
am
appreciate
v
uc
ery
Finally
grateful
ould
to

m
y
y
the

to
F
family

vietnamese
Herbreteau
thanks
and
Bernard
Grégoire
Bruno
Sutre
Jean-Mic
who
Couvreur,
initiated
Haddad,
me
Claude
to
for
the
ving


h,
b
and
mem
then
ers
ha
the
v
and
e
the

This
me
ortan
throughout
task
this
alw
thesis.
ys
As

their
deserv
rst
all
PhD
y
studen
I
t,
thank
w

e
ha
ha
b
v
m
e
sup
shared
for
an
mon

Thanks
t
Anne
exp
ky
erience.
Alain
They
and
taugh
Ly
t
their
me
I
a
w
lot
lik
ab
to
out
all
not
mem
only
ers
ho
the
w
ormal

ds
aid
oup
v
L

.
but
sp
also
thanks
ho
to
w
e

to
eten
hel
t
He
and
lo

ed
heerful
me
sup
alw
ervisors
ys
aid
een
a
when
studen
needed
t
I
lik
to
e
An
me.

It

is
friend
not
mine
an
I
o
v
v
m
erstatemen
h
t
friendship.
to
,
sa
w
y
lik
that
to
without
h
their
m

mother
and
in

follo
this
page
thesis
thank
w
y
ould
and
not
y
exist.
y
Man
A
iiii
Biết ơn
Tôi muốn dành đôi dòng ngắn ngủi viết bằng tiếng mẹ đẻ cho những người mà chính họ
đã tạo nên tôi với những kết quả đạt được trong nghiên cứu này.
Trước hết là với bố mẹ, những người đến giờ mới yên lòng vì đã lo xong cho con ăn
học tới nơi tới chốn. Con trai của bố mẹ chỉ biết làm nhẹ bớt lo toan đó bằng những
kết quả đẹp - cái mà bố mẹ luôn tự hào suốt quá trình học dài đằng đẵng của con. Cái
đạt được ngày hôm nay, một lần nữa, chính là quả chín đền đáp công ơn nuôi nấng con
ăn học.
Tiếp đến là với những người thân trong gia đình: anh Kỳ, chị Lê, anh Hà, chị Thảo,
Quân, Minh, và cả Thỏ con nữa. Mọi người đã gánh giúp em, giúp cậu, những việc mà
một người con trai lớn khi xa nhà không thể làm được. Hơn nữa, niềm tin của anh chị
và các cháu với em đã không cho phép em buông xuôi, và luôn là động lực để em có đi
có đến.
Mảnh đất Bordeaux cho rượu và con người làng Nho cho tình. Đếm năm tháng cứ
ngỡ là dài nhưng nhắm mắt nhớ lại thì thấy quá ngắn. Từ anh Khuê già cho nhà đón
ngày đầu, đến Đai fou cho nhà tù ngày cuối, biết bao người ở làng này, nếu không muốn
nói là tất cả, đã giúp tôi ăn-ở-vui-chơi, nói chung là sống, để mà học tốt. Nợ chẳng trả
đủ đành cười xoà nói lời cám ơn. Tôi cũng xin phép không kể hết tên chủ nợ vì quá dài.
Nếu coi bạn bè như chân tay thì mấy năm xa nhà cũng đủ làm tôi khác người (hy
vọng không giống ngợm). Hơn nữa, tính rẻ hai năm có thêm một đầu đã là quá hời: anh
Hoàng cong, Đức chích, Đại fou. Những cái đầu sẵn sàng chung vai mà không bao giờ
làm đau đầu tôi, quả là đáng quý. Đáng quý hơn nữa khi biết rằng làm nghiên cứu là
đã phải đau đầu.
Có những người đã gửi trái tim cho tôi lúc