Contribution à la modélisation et à la vérification de processus workflow
160 pages
Français
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Contribution à la modélisation et à la vérification de processus workflow

-

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
160 pages
Français

Description

Sous la direction de Kamel Barkaoui
Thèse soutenue le 13 novembre 2010: Université de Tunis et Ecole nationale d'Ingénieur de Tunis, CNAM
La technologie de workflow, tendant à automatiser les processus d'entreprise et à fournir un support pour leur gestion, est aujourd'hui un secteur actif de recherche. C'est dans ce contexte que se situent ces travaux de thèse qui portent aussi bien sur la modélisation des processus workflow que sur leur vérification. Ces processus, pouvant être contraints par des ressources partagées ou encore par des durées de traitement, doivent être vérifiés avant d'être confiés aux systèmes de gestion de workflow qui vont les exécuter. Nous nous sommes intéressés par la vérification de la propriété de cohérence (soundness) des réseaux de workflow (WF-net) : sous-classes des réseaux de Petri (RdPs) modélisant les processus workflow.Dans ce cadre, en explorant la théorie structurelle des RdPs, nous avons identifié des sous-classes de WF-nets pour lesquelles la cohérence peut être vérifiée et caractérisée efficacement. Nous nous sommes focalisés en outre sur l'extension de ces sous-classes en tenant compte de la présence de ressources partagées et sur la propriété de cohérence en présence d'un nombre arbitraire d'instances prêtes à s'exécuter. Dans cette partie, nous avons dû automatiser le calcul des siphons minimaux dans un RdP. Pour ce faire, nous avons choisi un algorithme de la littérature et l'amélioré par la recherche et la contraction de circuits alternés.Ensuite, nous avons abordé la modélisation et la vérification de processus workflow tenant compte des contraintes temporelles. Nous avons en premier lieu proposé un modèle de TWF-net (WF-net Temporisé). Pour ce modèle, nous avons défini la propriété de cohérence temporelle et proposé une condition nécessaire et suffisante pour la vérifier. En deuxième lieu, nous avons relaxé les contraintes temporelles adoptées par la proposition d'un modèle temporel visant des processus à contraintes temporelles variant dans des intervalles de temps. Nous avons défini formellement le modèle de ITWF-net (Interval Timed WF-net) et donné sa sémantique. Par ailleurs, nous avons développé et testé un prototype de modélisation et de simulation des ITWF-nets.La dernière partie de cette thèse a concerné la vérification formelle des processus workflow par SPIN model checker. Nous avons dû en premier lieu traduire la spécification des workflows adoptée vers Promela : le langage de description des modèles à vérifier par SPIN. En second lieu, nous avons exprimé les propriétés de cohérence en Logique Linéaire Temporelle (LTL) et utilisé SPIN pour tester si chaque propriété est satisfaite par le modèle Promela du WF-net en question. Enfin, nous avons exprimé les propriétés de k-cohérence pour les WF-nets modélisant plusieurs instances et de (k,R)-cohérence pour les processus workflow concurrents et qui possèdent des ressources partagées.
-Processus workflow
-Modélisation
-Vérification
-Réseaux de Petri
-Model Checking
Workflow technology, whose role is to automate business processes and to provide a support for their management, is today an active sector of research. This thesis deals with the modelling of the workflow processes and their analysis. These processes, probably constrained by shared resources or by durations of treatment, must be checked before being executed by their workflow management systems. In this direction, we were interested by the checking of the soundness property of workflow nets (WF-nets): subclasses of Petri nets modelling the workflow processes.To begin with, by exploring the structure theory of Petri nets, we have identified subclasses of WF-nets for which soundness can be checked and characterized effectively. We also extended these subclasses by taking account of the presence of shared resources and we focused on the soundness property in the presence of an arbitrary number of instances ready to be carried out. In this part, we had to automate the computation of minimal siphons in a Petri net. For that, we chose an algorithm of the literature and improved it by the research and the contraction of alternate circuits.Then, we were concerned by the modelling and the analysis of workflow processes holding temporal constraints. We initially proposed the model of TWF-net (Timed WF-net). For this model, we defined its soundness and proposed a method to check it. Then, we released the adopted temporal constraints by the proposal of a model covering workflow processes for witch temporal constraints vary in time intervals. We formally defined the model of ITWF-net (Interval Timed WF-net) and gave its semantics. In addition, we developed and tested a prototype of modelling and simulation of ITWF-nets.The last part of this thesis concerns the formal analysis of workflow processes with SPIN model checker. We initially translated the workflow specification into Promela: the model description language used by SPIN. Then, we expressed the soundness properties in Linear Temporal Logic (LTL) and used SPIN to test if each property is satisfied by the Promela model of a given WF-net. Moreover, we expressed the properties of k-soundness for WF-nets modelling several instances and (k,R)-soundness for competitive workflow processes which share resources.
-Workflow process
-Modelling
-Analysis
-Petri nets
-Model Checking
Source: http://www.theses.fr/2010CNAM0731/document

Sujets

Informations

Publié par
Nombre de lectures 97
Langue Français
Poids de l'ouvrage 2 Mo

Exrait

Titre,
ENIT
P
V
ENIT
A
Présiden
TOIRE
aris
NA
CNAM
TIONAL
Samir
DES
JUR
AR
de
TS
T
ET
BEN
MÉTIERS
BARKA
Ecole
Rahma
Do
T
ctorale
aris
Informatique,
hnique
Télécomm
ANE
u
GUEMARA
nications
OBBANA
et
de
Electronique
Samir
de
Professeur,
P
Maître
aris
ar
[Cen
Kamel
tre
A
d'Etudes
de
et
TEURS
De
T
Rec
TELECOM
herc
OBBANA
he
P
en
T
Informatique
:
du
Professeur,
CNAM]
du
THÈSE
Professeur,
présen
unis
tée
Professeur,
par
c
:
uni
[Zohra
T
SBAÏ]
TELECOM
souten
OUI
ue
P
le
YED
:
conférences,
13
p
no
:
v
OUI
em
Professeur,
bre
BEN
2010
YED
p
Maître
our
Conférences,
obtenir
RAPPOR
le
:
grade
A
de
A
:
Professeur,
Do
SudP
cteur
R
du
Riadh
Conserv
Ecole
atoire
olytec
National
de
des
unis
Arts
Y
et
JAÏD
Métiers
Mériem
Discipline/
ENIT,
Sp
t
éciali
jury

Sihem
:
SUP'COM
Informatique
T
Con
R
tribu
Riadh
t
Ecole
i
olyte
on
hnique
à
T
la
s
Mo
A
délisation
A
et
Professeur,
à
SudP
la
BARKA
Vérication
Kamel
de
CNAM
Pro
aris
cessus
A
W
Rahma
orko
de
w
dirigée
THÈSE
CONSER
tel-00553383, version 1 - 7 Jan 2011tel-00553383, version 1 - 7 Jan 2011uni-
la
ces
ts
p
Les
re
tra
f
v
oratoire
aux
son
présen
d
tés
à
dans
au
cette
p
thèse
v
on
le
t
ce
été
GUEMARA,
eectués
oir
au
ici
Lab
BEN
oratoire
our
Systèmes
v
de
s'adresse
Comm
National
unication
t
de
qu'il
l'
mes
Ecole
u
Nationale
fourni.
d'Ingénieurs
qu'il
de
a
T
Je
unis,
Sup
et
unis
au
partie
Cen
Qu'ell
tre
profond
d
emen
'Etude
des
et
de
de
dirigé
Rec
et
herc
son
he
années.
en
BARKA
Informatique
au
du
Métiers
Conserv
oir
atoire
ces
N
conseil
a
endan
ti
v
o
mem
n
et
al
du
des
orable
Arts
e
et
l'analyse
Métiers
menée
d
et
e
tribué
P
hissemen
aris
Madame
.
à
Mes
des
remerciemen
de
ts
d'a
v
de
on
mem
t
jury
à
trouv
Madame
de
Mériem
ect.
JAID
très
AN
Madame
E,
YED,
Professeur
n
à
Nationale
l'Ecole
unis,
Nationale
v
d'Ingénieurs
endan
de
v
T
our
unis,
accordé
p
précieux
our
de
le
profonde
grand
Monsieur
honneur
P
qu'elle
s
m'a
v
fait
Arts
en
P
acceptan
m'a
t
to
de
long
présider
p
ce
et
jury
a
de
accordés
th
ce
è
Je
s
emen
e.
et
Qu'elle
du
trouv
de
e
bres
ici
oratoire
le
p
témoignage
fa
de
m'on
ma
3
resp
reconnaissance
e
our
ctu
rigoureuse
euse
a
gratitude
à
et
mémoire
mon
qui
profond
con
resp
à
ect.
enric
Je
t.
tiens
remercie
à
Sihem
exprimer
Professeur
ma
l'Ecole
gratitude
érieure
en
Comm
v
cations
ers
T
Monsieur
(SUP'COM),
Riadh
v
R
accepté
OBBANA
faire
,
des
Professeu
bres
r
u
à
.
l'Ecole
e
P
e
olytec
l'expression
hnique
mon
de
resp
T
Je
unis,
mercie
qui
viv
m'a
t
honoré
Rahma
en
A
acceptan
Maître
t
Co
de
férences
j
l'Ecole
uger
d'Ingénieurs
ce
T
tra
p
v
m'a
ail.
oir
Q
p
u
t
'il
tra
trouv
aux
e
p
ici
m'a
l'expression
oir
de
de
ma
temps
profonde
tout
gratitude
long
et
ces
mon
Ma
resp
gratitude
ect.
à
Je
Kamel
suis
OUI,
égalemen
ro
t
e
très
seur
reconnaissan
Conser-
te
atoire
en
des
v
et
ers
de
Monsieur
aris,
Samir
our
T
v
A
guidé
T
u
A,
au
Professeur
de
à
années,
TE-
our
LECOM
conance
S
les
udP
s
aris,
visés
qui
m'a
m'a
p
fait
t
un
tra
grand
ail.
honneu
remercie
r
iv
en
t
acce
amis
p
collègues
tan
bres
t
Lab
d
Sys'Com
e
l'ENIT
juger
mem
ce
d
tra
Lab
v
CEDRIC
ail.
CNAM
Je
our
tiens
climat
à
v
lui
qu'ils
exprimer
t
toute
viv
ma
Remerciemen
tel-00553383, version 1 - 7 Jan 2011MENTS
4
E
CI
REMER
tel-00553383, version 1 - 7 Jan 2011del
our
king.
La
mo
tec
satisfaite.
hnologie
(WF-net
de
visan
w
délisation
orko
nous
w,
ts
tend
temp
a
propriété
n
temp
t
in-
à
ailleurs,
autom
a
atis
lieu
e
TL)
r
délisan
les
Pro
pro
t
cessus
lieu
d'en
dèle,
treprise
osé
et
a
à
ro
fournir
tes
un
ons
supp
WF-net)
ort
et
p
dernière
our
o
leur
v
gestion,
ws
est
cohérence
aujourd'h
c
ui
propriétés
un
our
secteur
s
actif
Réseaux
d
w
e
des
rec
v
herc
mo
he.
P
C'est
on
dans
temp
ce
et
con
En
texte
les
que
adoptées
se
mo
situen
cessus
t
arian
ces
temps.
tra
leme
v
(In
aux
séman
de
ons
thèse
yp
qui
ulation
p
thèse
orten
des
t
par
aussi
er.
bien
p
sur
écication
la
Promela.
mo
exprimé
délisation
T
des
p
pro
propriété
cessus
v
w
our
orko
et
w
w
que
ossèden
sur
partagées.
leur
w,
v
etri,
éric
pro
ation
w
.
p
Ces
train
pro
Nous
cessus,
en
p
osé
ouv
de
an
emp
t
ce
être
a
con
déni
train
co-
ts
et
par
condition
des
te
ress
v
o
lieu,
u
ons
rce
train
s
l
partagées
la
ou
osition
encore
temp
par
des
d
con
es
orelles
durées
dans
d
alles
e
a
traitemen
forme
t,
t
doiv
de
en
al
t
donné
être
P
v
a
ériés
elopp
a
un
v
de
an
de
t
ITWF-nets.
d'être
de
conés
concerné
aux
érication
systèm
cessus
es
o
de
m
ge
hec
s
s
tion

de
i
w
la
orko
w
w.
v
Nous
second
nous
v
sommes
propriétés
in
Logique
téressés
orelle
par
utilisé
la
tester
v
a
érication
s
de
nous
la
exprimé
propriété
k-cohérence
d
WF-nets
e
plusieurs
cohéren
(k,R)-cohérence
c
pro
e
w
(sou
qui
ndness)
des
des
u
réseaux
clés
de
w
w
délisation,
orko
e
w
del
(WF-net)
5
:
cessus
sous-classes
orko
des
tenan
réseaux
com
de
te
P
con
etri
tes
(RdP
orelles.
s)
a
mo
ons
délisan
premier
t
prop
les
un
pro
dèle
cessus
TWF-net
w
T
orko
orisé).
w.
our
Dans
mo
ce
nous
cadre,
v
en
s
exploran
la
t
de
la
hérence
théorie
orelle
structurelle
prop
des
une
RdP
nécessaire
s,
susan
nous
p
a
la
v
érier.
ons
deuxième
iden
nous
tié
v
des
relaxé
sous-classes
con
de
tes
WF-n
ore
ets
les
p
par
our
p
lesquelles
p
la
d'un
cohérence
dèle
p
orel
eut
t
être
pro
v
à
ériée
train
et
temp
caractérisée
v
eca-
t
cemen
des
t.
terv
Nous
de
nous
Nous
som
v
mes
déni
fo
l
calisés
n
en
le
outre
dèle
sur
ITWF-net
l'extension
terv
de
Timed
ces
et
sous-classes
sa
en
tique.
ten
ar
a
nous
n
v
t
dév
compte
é
de
testé
la
protot
présence
e
de
mo
ressources
et
partagées
sim
et
des
sur
La
la
partie
propriété
cette
de
a
cohérence
l
en
v
présence
formelle
d'un
pro
nom
w
bre
rk-
arbitraire
w
d'instances
SPIN
à
o
e
c
xécuter.
k
Dans
Nou
cette
a
partie,
ons
nous
en
a
rem
v
er
ons
traduire

sp
automati-
des
ser
orko
le
adoptée
calcul
ers
des
En
siphons
lieu,
minimaux
a
dans
ons
un
les
RdP
de
.
en
P
Linéaire
our
emp
cela,
(L
nous
et
a
SPIN
v
our
ons
si
c
h
hoisi
que
u
e
n
t
algorithme
Enn,
de
a
la
ons
littérature
les
et
de
l'amélioré
p
par
les
la
mo
rec
t
herc
instances
he
de
et
p
la
les
con
cessus
traction
orko
de
concurren
circuits
et
alternés.
p
Ensuite,
t
n
re
ous
so
a
rces
v
Mots
ons
:
ab
cessus
ordé
orko
l
Mo
a
Vérication,
mo
d
délisation
P
et
Mo
la
Chec
v
de
érication
Résumé
tel-00553383, version 1 - 7 Jan 20116
RÉSUMÉ
tel-00553383, version 1 - 7 Jan 2011tes
witc
constrain
W
concerns
orko
w
w
c
te
v
c
to
hnology
erties
,
y
whose
or
role
the
is
d
to
yp
automa
c
te
the
business
of
pro
e
cesses
Then,
a
w
n
mo
d
soundness
to
the
pro
v
vide
in
a
ITWF-net
supp
e
ort
of
for
orko
their
the
managemen
used
t,
oral
is
is
to
er,
da
sev
y
h
an
nets,
activ
w
e
and
sector
cesses
of
initially
researc
(Timed
h.
w
This
a
thesi
Then,
s
constrain
deals
a
with
w
the
constrain
mo
als.
delling
the
of
Timed
the
tics.
w
and
orko
delling
w
part
p
n
ro
with
cesses
W
and
sp
their
mo
analysis.
Then,
These
in
pro
and
cesses,
h
probably
the
constrained
WF-net.
b
p
y
WF-
shared
(k,R)-soundness
resources
w
or
ords
b
delling,
y
Chec
durations
w
o
concerned
f
mo
treatmen
analysis
t,
w
m
temp
ust
W
b
osed
e
of
c
net).
hec
mo
k
dened
ed
prop
b
d
efore
k
b
e
e
temp
i
b
ng
osal
executed
del
b
w
y
cesses
their
temp
w
v
orko
in
w
e
ma
n
n
del
ag
terv
emen
and
t
its
systems.
addition,
In
elop
this
a
d
of
irection,
sim
w
The
e
this
w
formal
ere
of
i
pro
n
mo
terested
k
b
initially
y
orko
the
ation
c
:
hec
description
king
y
of
e
the
prop
soundness
T
prop
(L
ert
SPIN
y
if
of
ert
w
b
orko
mo
w
giv
nets
reo
(WF-nets)
e
:
the
s
k-soundness
ub
mo
classes
instances
of
comp
P
o
etri
cesses
nets
resources.
mo
W
delling
cess,
the
P
w
d
orko
i
w
7
pro
e
cesses.
ere
T
b
o
the
b
delling
egin
the
with,
of
b
orko
y
pro
exploring
holding
the
oral
structure
ts.
theory
e
of
prop
P
the
etri
del
nets,
TWF-net
w
WF-
e
F
ha
this
v
del,
e
e
iden
its
tied
and
su
osed
b-
metho
classes
to
of
hec
WF-nets
it.
for
w
whic
released
h
adopted
soundness
oral
can
ts
b
y
e
prop
c
of
hec
mo
k
co
ed
ering
and
orko
c
pro
haracterized
for
eectiv
h
ely
oral
.
ts
W
ary
e
time
also
terv
extended
W
these
formally
sub
e
classes
ed
b
mo
y
of
taking
(In
accoun
al
t
WF-net)
of
ga
th
e
e
seman
p
In
resence
w
o
dev
f
ed
s
tested
hared
protot
resources
e
a
mo
n
and
d
ulation
w
ITWF-nets.
e
last
fo
of
cused
thesis
on
the
th
a
e
alysis
soundness
w
prop
w
ert
cesses
y
SPIN
in
del
the
hec
presence
er.
of
e
an
translated
arbitrary
w
n
w
um
ecic
b
in
er
Promela
of
the
instances
del
ready
language
to
b
b
SPIN.
e
w
carried
expressed
out.
soundness
In
erties
this
Linear
part,
emp
w
Logic
e
TL)
had
used
to
to
automate
t
the
eac
computation
prop
of
y
minimal
satised
siphons
y
in
Promela
a
del
P
a
etri
en
net.
Mo
F
v
or
w
that,
ex
w
ressed
e
prop
c
of
hose
for
an
nets
algorithm
delling
of
eral
the
and
literature
for
and
etitiv
impro
w
v
rko
ed
pro
it
whic
b
share
y
Keyw
the
:
researc
orko
h
pro
a
Mo
n
Analysis,
d
etri
the
Mo
con
el
traction
k
of
ng.
alternate
circuits.
Abstract
tel-00553383, version 1 - 7 Jan 20118
CT
ABSTRA
tel-00553383, version 1 - 7 Jan 201125
w
.
able
.
des
.
matières
.
In
.
tro
.
duction
.
15
.
1
.
Con
.
texte
w
.
.
.
.
.
.
.
.
.
.
.
.
.
eb
.
26
.
.
.
.
.
.
.
.
.
.
.
3
.
.
.
1.2.1
.
.
.
lémen
.
.
.
métier
.
.
.
ho
.
.
.
W
.
.
.
.
.
.
.
.
.
.
.
.
.
w
.
.
.
Le
.
.
.
.
.
.
.
29
.
.
16
orko
1.1
.
Emergence
.
des
.
w
.
orko
.
ws
pro
.
.
.
.
.
5
.
cessus
.
.
.
.
.
hnologies
.
.
.
.
.
.
.
ec
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
26
.
.
.
.
.
.
.
.
16
c
1.2
.
Motiv
.
ations
.
.
La
.
.
.
.
.
.
.
.
.
w
.
.
.
.
.
.
.
Dénitions
.
.
.
.
.
.
.
terminologie
.
.
.
.
.
Classication
.
.
.
.
.
.
.
9
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
délisation
.
métier
.
.
.
.
16
.
2
.
Problématique
.
.
Im
.
de
.
.
.
.
.
.
.
.
.
.
.
T
.
pro
.
.
.
.
.
.
.
.
.
.
.
.
.
1.3.1
.
A
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
26
.
ws
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
17
Services
3
.
Ob
.
jectifs
.
de
.
la
.
thèse
.
.
.
.
.
.
Autres
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
27
.
hnologie
.
w
.
.
.
.
.
.
.
.
.
.
.
.
.
28
.
hoix
.
w
.
.
.
.
.
.
.
.
.
.
.
.
.
28
.
base
.
w
17
.
3.1
.
Etude
.
des
.
lacunes
.
d'un
Concepts
certain
w
nom
.
bre
.
de
.
WfMSs
.
.
29
.
systèmes
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
18
.
3.2
.
Caractérisation
.
Structurelle
.
de
.
la
.
propriété
.
de
.
cohérence
.
.
.
.
.
.
.
.
.
.
23
.
Mo
.
de
18
cessus
3.3
.
Vérication
.
structurelle
.
de
.
la
.
propriété
.
de
.
cohérence
.
.
.
.
.
.
2
.
1.2.2
.
p
.
tation
.
pro
.
métier
.
.
19
.
3.4
.
Mo
.
délisation
.
et
.
analyse
.
des
.
pro
.
cessus
1.3
w
ec
orko
de
w
cessus
à
.
con
.
train
.
tes
.
temp
.
o-
.
relles
.
.
.
.
.
.
.
.
.
.
.
.
26
.
T
.
hniques
.
d
.
c
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
1.3.2
.
orko
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
19
.
3.5
.
Vérication
.
par
.
mo
.
del
.
c
.
hec
1.3.3
king
W
des
.
pro
.
cessus
.
w
.
orko
.
w
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
20
.
4
.
Plan
1.3.4
du
Appro
mémoire
hes
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
1.4
.
tec
.
de
.
orko
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
1.4.1
20
c
1
du
T
orko
ec
.
hnologie
.
du
.
w
.
orko
.
w
.
et
.
con
.
tribution
.
pratique
.
23
.
1.1
.
In
.
tro
.
duction
1.4.2
.
de
.
du
.
orko
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
1.4.3
.
et
.
de
.
orko
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
1.5
.
des
.
w
.
w
.
.
.
.
.
.
.
.
.
.
23
.
1.2
.
Pro
.
cessus
.
métier
.
.
.
.
1
.
.
T
tel-00553383, version 1 - 7 Jan 2011Vérication
.
(k,
ABLE
.
DES
.
MA
2.4.3
TIÈRES
.
1.6
.
Mo
.
dèle
.
de
R-cohérence
référence
w
des
.
systèmes
.
w
.
orko
.
w
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
v
.
.
.
W
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
La
32
.
1.7
K
Mo
de
délisation
.
d
.
es
.
pro
.
cessus
.
w
de
orko
érication
w
tous
.
.
.
.
.
tests
.
.
.
.
.
Conclusion
.
.
.
.
.
orelles
.
.
.
.
.
temps
.
.
.
tiques
.
.
.
a
.
.
.
cohérence
.
.
.
54
.
.
.
.
34
.
1.7.1
.
Asp
.
ects
.
à
.
mo
2.3.3
déliser
(KWF-nets)
.
sous
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
sous
.
.
.
Pro
.
cohérence
.
63
.
dans
.
.
.
du
.
.
.
.
.
67
.
timisé
.
.
.
2.5.4
.
CS
34
.
1.7.2
.
T
.
ec
.
hniques
.
et
.
outi
.
ls
con
de
tro
mo
.
délisation
.
de
.
w
.
orko
In
w
s
.
.
.
.
.
3.2.1
.
.
.
.
.
.
.
des
.
temps
.
.
.
10
.
de
35
WF-nets
1.7.3
.
Les
.
asp
.
ects
La
temp
.
orels
.
d
.
e
.
w
.
orko
.
w
.
.
55
.
généralisée
.
.
.
.
.
.
.
.
.
.
.
.
.
structurelle
.
orko
.
.
.
2.4
.
train
.
.
.
.
.
.
.
.
.
.
.
2.4.1
37
.
1.7.4
.
Structure
.
organisationnelle
.
.
.
.
.
.
.
.
2.4.2
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
cohérence
.
train
.
.
.
.
.
62
.
de
.
de
.
pro
.
o
.
Calcul
.
siphons
38
RdP
1.8
.
Outils
.
logiciels
2.5.2
p
el
our
.
décrire
.
et
.
gérer
.
un
.
w
Complexité
orko
l'algorithme
w
.
.
.
.
.
.
.
.
cédure
.
de
.
ert
.
.
.
.
.
.
.
80
.
.
.
.
.
.
.
.
.
.
38
.
1.9
.
Présen
.
tation
.
de
80
l'outil
ws
jPnet
tes
.
3.1
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
83
.
duction
.
les
.
.
.
.
.
.
.
.
.
.
.
.
.
rois
.
tes
.
.
.
.
.
.
.
.
.
.
.
3.2.2
40
augmen
1.9.1
ec
Mapping
.
en
.
tre
.
jPdl
4
et
2.3
RdP
paramétrée
.
la
.
des
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.3.1
.
k-cohérence
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
40
.
1.9.2
.
Mapping
.
en
2.3.2
tre
Cohérence
PNML
.
et
.
Rd
.
P
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
55
.
Caractérisation
.
des
.
-w
.
w-nets
.
.
.
.
.
55
.
Vérication
.
con
.
tes
.
ressources
.
.
.
.
44
.
1.10
.
Conclusion
.
.
.
.
.
.
.
.
.
.
60
.
La
.
R)-cohérence
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
60
.
La
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
47
62
2
La
Vérication
généralisée
des
con
pro
tes
cessus
ressources
w
.
orko
.
w
.
49
.
2.1
2.5
In
cédure
tro
v
duction
structurelle
.
la
.
des
.
cessus
.
ork
.
w
.
2.5.1
.
de
.
les
.
minimaux
.
un
.
.
.
.
.
.
.
.
.
.
.
63
.
Description
.
nouv
.
algorithme
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.5.3
.
et
.
de
.
op
.
.
.
.
.
.
49
.
2.2
.
Les
.
réseaux
.
w
77
orko
Pro
w
de
:
érication
mo
la
dèle
-prop
de
y
base
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.6
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
49
.
2.2.1
.
Choix
.
des
.
réseaux
.
de
3
P
orko
etri
à
comme
train
langage
temp
de
83
mo
In
délisation
duction
de
.
w
.
ork
.
o
.
w
.
50
.
2.2.2
.
Notions
.
de
.
base
.
d
.
e
.
s
.
réseaux
.
de
.
P
.
etri
.
.
.
.
3.2
.
tro
.
du
.
dans
.
RdP
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
84
51
T
2.2.3
séman
Les
Diéren
réseaux
.
w
.
orko
.
w
.
(WF-nets)
.
.
.
.
.
.
.
.
.
.
.
.
.
.
84
.
Sous-classes
.
RdPs
.
tés
.
v
.
le
.
.
.
.
.
.
.
.
.
.
.
.
.
86
.
5
T
tel-00553383, version 1 - 7 Jan 2011

  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents