Synthèse pour une logique temps-réel faible, Synthesis for a weak real-time logic
157 pages
English

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Synthèse pour une logique temps-réel faible, Synthesis for a weak real-time logic

-

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
157 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Sous la direction de Igor Walukiewicz
Thèse soutenue le 07 décembre 2009: Bordeaux 1
Dans cette thèse, nous nous intéressons à la spécification et à la synthèse de contrôleurs des systèmes temps-réels. Les modèles pour ces systèmes sont des Event-recording Automata. Nous supposons que les contrôleurs observent tous les évènements se produisant dans le système et qu'ils peuvent interdirent uniquement des évènements contrôlables. Tous les évènements ne sont pas nécessairement contrôlables. Une première étude est faite sur la logique Event-recording Logic (ERL). Nous proposons des nouveaux algorithmes pour les problèmes de vérification et de satisfaisabilité. Ces algorithmes présentent les similitudes entre les problèmes de décision cité ci-dessus et les problèmes de décision similaires étudiés dans le cadre du $\mu$-calcul. Nos algorithmes corrigent aussi des algorithmes présents dans la littérature. Les similitudes relevées nous permettent de prouver l'équivalence entre les formules de ERL et les formules de ERL en forme normale disjonctive. La logique ERL n'étant pas suffisamment expressive pour décrire certaines propriétés des systèmes, en particulier des propriétés des contrôleurs, nous introduisons une nouvelle logique WT$_\mu$. La logique WT$_\mu$ est une extension temps-réel faible du $\mu$-calcul. Nous proposons des algorithmes pour la vérification des systèmes lorsque les propriétés sont écrites en WT$_\mu$. Nous identifions deux fragments de WT$_\mu$ appelés WT$_\mu$ bien guardé ($WG$-WT$_\mu$) et WT$_\mu$ pour le contrôle ($C$-WT$_\mu$). La logique $WG$-WT$_\mu$ est plus expressif que $C$-WT$_\mu$. Nous proposons un algorithme qui permet de vérifier si une formule de $WG$-WT$_\mu$ possède un modèle (éventuellement déterministe). Cet algorithme nécessite de connaître les ressources (horloges et constante maximale comparée avec les horloges) des modèles. Dans le cadre de $C$-WT$_\mu$ l'algorithme que nous proposons et qui permet de décider si une formule possède un modèle n'a pas besoin de connaître les ressources des modèles. En utilisant $C$-WT$_\mu$ comme langage de spécification des systèmes, nous proposons des algorithmes de décision pour le contrôle centralisé et le $\Delta$-contrôle centralisé. Ces algorithmes permettent aussi de construire des modèles de contr\^oleurs. Lorsque les objectifs de contrôle sont décrits à l'aide des formules de $WG$-WT$_\mu$, nous montrons également comment synthétiser des contrôleurs décentralisés avec des ressources fixées à l'avance et ceci, lorsqu'au plus un contrôleur est non déterministe.
-Systèmes temps-réel
-Event-Recording automata
-Logique temps-réel
-Satisfaisabilité
-Event-Recording Logic
-Méthodes formelles
-Vérification
-Synthèse de contrôleurs
In this dissertation, we consider the specification and the controller synthesis problem for real-time systems. Our models for systems are kinds of Event-recording automata. We assume that controllers observe all the events occurring in the system and can prevent occurrences of controllable events. We study Event-recording Logic (ERL). We propose new algorithms for the model-checking and the satisfiability problems of that logic. Our algorithms are similar to some algorithms proposed for the same problems in the setting of the standard $\mu$-calculus. They also correct earlier proposed algorithms. We define disjunctive normal form formulas and we show that every formula is equivalent to a formula in disjunctive normal form. Unfortunately, ERL is rather weak and can not describe some interesting real-time properties, in particular some important properties for controllers. We define a new logic that we call WT$_\mu$. The logic WT$_\mu$ is a weak real-time extension of the standard $\mu$-calculus. We present an algorithm for the model-checking problem of WT$_\mu$. We consider two fragments of WT$_\mu$ called well guarded WT$_\mu$ ($WG$-WT$_\mu$) and WT$_\mu$ for control ($C$-WT$_\mu$). We show that the satisfiability of $WG$-WT$_\mu$ is decidable if the maximal constants appearing in models are known a priori. Our algorithm allows to check whether a formula of $WG$-WT$_\mu$ has a deterministic model. The algorithm we propose to decide whether a formula of $C$-WT$_\mu$ has a model does not need to know the maximal constant used in models. All the algorithms for the satisfiability checking construct witness models. Using $C$-WT$_\mu$, we present algorithms for a centralised controller synthesis problem and a centralised $\Delta$-controller synthesis problems. The construction of witness controllers is effective. We also consider the decentralised controller synthesis problem with limited resources (the maximal constants used in controllers is known a priory) when the properties are described with $WG$-WT$_\mu$. We show that this problem is decidable and the computation of witness controllers is effective.
-Real-time systems
-Event-recording automata
-Formal methods
-Real-time logic
-µ-calculus
-Event-recording logic
-Satisfiability
-Model-checking
-Controller synthesis
Source: http://www.theses.fr/2010BOR13931/document

Sujets

Informations

Publié par
Nombre de lectures 20
Langue English

Extrait

.
Lime
.
vité
.
d'ordre
.
:
Professeur,
3931
Nan
THÈSE
.
PRÉSENTÉE
.
À
Rec
L'UNIVERSITÉ
.
DE
aris
BORDEA
.
UX
.
ÉCOLE
.
DOCTORALE
.
DE
.
MA
.
THÉMA
.
TIQUES
HDR
ET
.
D'INF
orteur
ORMA
aris
TIQUE
.
P
.
ar
École
Omer
W
Landry
herc
Nguena
.
Timo
.
POUR
André
OBTENIR
Professeur
LE
.
GRADE
.
DE
.
DOCTEUR
In
SPÉCIALITÉ
.
:
Chargé
INF
he
ORMA
.
TIQUE
.
SYNTHESE
.
POUR
.
UNE
rançois
LOGIQUE
ersité
TEMPS-REEL

F
.
AIBLE
orteur
(SYNTHESIS
.
F
.
OR
de
A
trale
WEAK
Examinateur
REAL-TIME
.
LOGIC)
de
Souten
CNRS
ue
.
le
.
:
.
07
.
Décem
de
bre
.
2009
.
Après
la
a
.
vis
.
des
.
rapp
.
orteurs
.
:
.
F
2009
ranc
Cassez
k
.
Cassez
.
.
.
.
de
.
herc
.
CNRS,
.
.
.
.
Chargé
.
de
.
Rec
.
herc
.
he
.
CNRS,
Rapp
HDR
F
F
Laroussinie
rançois
Univ
Laroussinie
P
Professeur,
Diderot
Univ
P
ersité
7
P
.
aris
Rapp
Diderot
Didier

.
P
.
aris
.
7
.
Dev
Maître
an
Conférences,
t
Cen
la
de
commission
tes
d'examen
Igor
comp
alukiewicz
osée
.
de
Directeur
:
Rec
Marc
he
Zeitoun
.
.
.
.
.
.
.
.
.
.
.
.
.
Professeur,
.
Univ
.
ersité
Directeur
Bordeaux
Thèse
1
Arnold
.
.
.
.
.
.
.
à
.
retraite
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Présiden
.
t
.
du
.
jury
.
F
ranc
k
oNprésidé
ymeric
plus.
ts
p
Ce
promptemen
man
enric
uscrit
a
témoigne
et
du
fait
tra
séjour
v
de
ail
aux.
que
v
j'ai
de
réalisé
Je
duran
un
t
Cassez
ma
Didier
thèse,
c
non
t.
pas
Je
en
v
solitaire,
orté
mais
soutenance.
a
Rollet
v
sein
ec
V
le
de
concours
conn
d'une
remercie
m
et
ultitude
clin
de
thèse,
p
Laroussinie
ersonnes:
ortan
des
honoré
p
tra
ersonnes
k
qui
a
m'on
est
t
un
aidé,
bres
encour-
MVTSI
agé,
eu
écouté,
qui
inspiré,
à
encadré.
nom
Ces
particulier
p
uel
ersonnes
Castanet,
on
et
t
ANR
con
ma
tribué
ez
au
ers
ra
et
y
thèse.
onnemen
vide
t
de
de
administrativ
ce
l'Univ
tra
metten
v
tra
ail
Remerciemen
et
jury
je
ranc
tiens
F
à
m'on
les
en
remercier.
cette
Je
qui
ne
acceptan
p
d'examiner
ourrai
aux.
toutes
ami
les
Brlek,
citer;
LA
mais,
très
j'esp
qui
ère
l'est
qu'elles
te
se
grand
reconnaîtron
les
t.
group
André
v
Arnold,
LaBRI
tu
qui
as
éc
débuté
ts
l'encadremen
t
t
l'in
de
tra
cette
ous
thèse.
à
Je
remercie
regrette
G.,
que
et
nos
An
démarc
Ric
hes
ous
de
souten
rec
tégré
herc
pro
he
esTEC
de
an
nancemen
de
t
m'a
n'aien
p
t
diriger
pas
autre
ab
herc
outi.
des
Cep
nir
endan
n'ai
t,
le
je
l'après
garde
ous
de
cela.
b
équip
ons
tec
souv
tretien
enirs
Bordeaux
des
LaBRI
discussions
en
que
agréable
nous
ail.
a
à
v
t
ons
mon
eu
de
p
F
endan
k
t
et
et
rançois
après
qui
la
t
thèse.
honneur
Elles
rapp
étaien
t
t
thèse,
viv
Lime
an
m'a
tes,
en
en
t
thousiastes,
t
motiv
mes
an
v
tes
Mon
et
her
éclairan
Srec
tes.
o
T
mon
u
au
as
CIM
pris
été
de
marquan
ton
Ce
temps
en
de
ressorti
rep
encore
os
Je
p
dis
our
très
assister
merci.
à
remercie
ma
mem
soutenance
du
et
e
témoigner
tra
ainsi
ail
de
du
l'in
a
térêt
ec
p
j'ai
our
des
ce
hanges
tra
hissan
v
et
ail.
on
Je
p
te
de
remercie
térêt
p
mes
our
v
tout
V
cela.
étiez
Igor
breux
W
ma
alukiewicz,
Je
j'ai
en
probablemen
Alain
t
A
écrit
V.,
ou
Emman
dit
F.
b
toine
eaucoup
et
de
hard
c
v
hoses
m'a
erronées.
ez
Cep
u
endan
in
t,
au
tu
du
as
jet
guidé
T
mes
bien
tra
v
v
t
aux
soutenance
a
thèse.
v
ous
ec
v
b
ainsi
eaucoup
ermis
de
me
patience,
v
de
une
rigueur,
thématique
leur
rec
donnan
he
t
d'obtenir
une
ressources
qualité
our
meilleure.
ma
Les
Je
qualités
pas
scien
u
tiques
fameux
qu'on
de
p
thèse.
eut
v
m'attribuer
remercie
son
tout
t
Je
le
les
fruit
es
de
es,
ton
hniques
encadremen
d'en
t.
de
Je
ersité
te
1
remercie
du
p
qui
our
t
tout
place
cela.
cadre
Je
de
remercie
v
Marc
Un
Zeitoun
d'÷il
qui
Jean-louis
a
honorablemenk,
M.,
Saady
Lebna
l'ASECB
M.
mes
et
Larissa
Phillip
N.,
e
organisé
B..
en
Je
Á
remercie
ainsi
les
Jacqueline
équip
Jonathan
es
W.,
p
Camerounais
édagogiques
our
de
je
l'UFR
reconnaissan
Math-Info
t
de
quotidiennes
l'Univ
je
ersité
Sarah
Bordeaux
y
1
W.,
et
Picasso
du
Herv
départemen
I.,
t
des
d'informatique
Stagiaires
de
tous
l'IUT
de
Bordeaux
on
1
euvré
qui
mes
m'on
t'en
t
remercie
in
eurs
tégré
our
comme
L.,
A
cette
TER
E.
ou
profondémen
enseignan
Nathalie
t
Agnes
v
F
acataire.
Aude
En
V
particulier,
atric
je
k
remercie
Dominique
Marie-Christine
Benoît
C.,
N.,
Olivier
I.,
G.,
E.,
Pierre
N.,
C.
bres
Je
ciation
remercie
Étudian
les
Bordeaux)
collègues
on
et
p
amis
Merci
du
cela.
labri
Pierre
qui
as
on
ce
t
oursuiv
fa
sup
v
rance.
orisé
innimen
des
Enn
éc
paren
hanges
et
rendan
ne
t
eort
la
bien
vie
et
au
les
lab
de
oratoire
thèse?
plus
a
sympathique.
que
Si
remercie
je
t
ne
que,
p
R.,
eux
S.,
pas
I.,
tous
K.,
les
ann
citer,
B.,

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