Upload
diane-garcia
View
112
Download
5
Embed Size (px)
Citation preview
J-M Ilié, IRISA - Mai 2002 1
Aide à la conception de systèmes distribués
Cadre théorique réduction de modèle réduction d'espace d'états
Outils de vérification LTL et Automates de Büchi
Outils d'évaluation de performance évaluation probabiliste et chaîne de Markov
Perspectives
J-M. IliéLip6 SRC
J-M Ilié, IRISA - Mai 2002 2
Modèles-cadres pour la vérification
Système concurrent fini RDP
• Sémantique concurrente asynchrone• Générateur d'espace d'états• Aspects structurels (invariants, dépendances)• Aspect symbolique (gestion des couleurs)
Propriété de logique temporelle Linéaire : LTL, automates de Büchi
• Logique intuitive• Aspects applicatifs (propositions d'états,
propositions événementielles)• Même complexité en temps que CTL*• Traitement possible de l'équité des systèmes• Vérification à la volée
J-M Ilié, IRISA - Mai 2002 3
Automatisation de la vérification
Produit Synchronisé avec l'automate de la propriété
Interpréteur d'automate de Büchi
Produit
synchronisé
Interpréteur
dumodèle
Automate BüchiSpécification RDP
LTL
• Propriété vraie: ou• Séquence d'exécution invalidante
//f= G (w1 X F e1)
PROPw1 = ph1.Waitinge1 = ph1.Eating
true
!e1
f
A f
A f
CLASSPhilo = ph{1-3}
Thinking
Waiting
Eating
Forks
e1w1
true
J-M Ilié, IRISA - Mai 2002 4
Optimisations heuristiques
Interpréteur d'automate de Büchi
Noyau de
vérification
Interpréteur
dumodèle
Optimisation fonction d'une propriété
Réduction de modèle [thèse de Klai] sous-réseau suffisant pour la vérification
Réduction d'espace d'états [thèse de Ajami] exploitation des symétries partielles
Optimisations du noyau [DEA de Roux] Algorithme magique [évitement des redondances de recherche, cache d'états] Satisfaction semi-décidable [cache d'états réduits aux bits]
Produit Synchronisé avec l'automate de la propriété
Complexité : O(Af)*O(GRDP) !!! Bornes de complexité égales
J-M Ilié, IRISA - Mai 2002 5
Réduction des espaces d'états symétriques
Groupe de symétries globales sur les états
. s , .s . s1 s2 , .s1 .s2
. s. 0= 0
Classes d'équivalence d'états symétriques
Graphe d'états quotient (graphe de classes d'équivalence)
Automate de Büchi quotient (+ préserver les états d'acceptation)
f = ORiPhilo G (wi X F ei)
Différentes classes d'états symétriquespar permutations sur 1..3
1 3
true
w1
!e1
e1
true
w2
! e2
e2
w3
! e3
e3
1 2 2 3
Des symétries ressortent de l'analyse des permutations des propositions atomiques
J-M Ilié, IRISA - Mai 2002 6
Efficacité vue par GreatSPN
Réseau de Petri Bien Formé ---------> Système de transitions symétriques
Classe de couleurs Famille génératrice de symétries par
Action : permutations préservant les classes
Marquage symbolique Représentation d'une classe de marquages
Franchissement symbolique Préservation des symétries
Graphe de marquages symboliques Graphe quotientm11 = p1.Waiting + (p2+p3).Thinking
m12 = p2.Waiting + (p1+p3).Thinking
m13 = p3.Waiting + (p1+p2).Thinking
m1= Ph1.Waiting + (Ph2).Thinking
Avec Philo = Ph1 Ph2 (symboliquement)
tel que Ph1 = 1 Ph2 = 2
J-M Ilié, IRISA - Mai 2002 7
Efficacité vue par GreatSPN
0
20000
40000
60000
80000
100000
120000
140000
160000
180000
1 2 3 4 5 6 7
C
noeu
ds
evan(RG)
tang(RG)tang(SRG)&evan(SRG)
RG : graphe de marquagesSRG : graphe de marquages symboliquesevan : marquage évanescent (proba nulle)tang : marquage tangible
SRG RG|C|#tang(SRG) #evan(SRG) #tan(RG) #evan(RG)
4 30 30 312 3845 39 39 960 12006 48 48 2736 34567 57 57 7392 94088 66 66 19200 245769 75 75 48384 62208
10 84 84 119040 153600
MarquagesSymboliques
Marquagesstandards
J-M Ilié, IRISA - Mai 2002 8
Exploitation des symétries pour la vérification
Produit synchronisé quotient S : Groupe de symétrie Espace d'états symétrique sur S Propriété symétrique sur S Produit synchronisé quotient (symbolique)
état du produit synchronisé quotient : <m, b> contrainte : m m m b
f = GF (iPhilo phi.Thinking)
1,2 - 2,3 - 1,3
^
[ ^ ]
Sans précaution, seules des symétries propositionnelles sont exploitables !!
f = iPhilo G (phi.Thinking F phi.Eating)Les philosophes ne sont pas (suffisamment) symétriquespour la vérification
Le produit synchronisédoit être un système de transitions symétriques
J-M Ilié, IRISA - Mai 2002 9
Exploitation des symétries pour la vérification
Construction d'un produit synchronisé quotient Groupe de symétries S Espace d'états symétrique sur S Propriété symétrique sur S Produit synchronisé quotient (symbolique)
état du produit synchronisé quotient : <m, b> contrainte : m m m b
f = GF (iPhilo phi.Thinking)
1,2 - 2,3 - 1,3
^
[ ^ ]
Sans précaution, seules des symétries propositionnelles sont exploitables !!
f = iPhilo G (phi.Thinking F phi.Eating)Les philosophes ne sont pas (suffisamment) symétriquespour la vérification
Le produit synchronisédoit être un système de transitions symétriques
J-M Ilié, IRISA - Mai 2002 10
Lemme :
Si n1 -> n2 existe dans le produit synchronisé symbolique
alors
chaque marquage de n2 is accessible par un marquage de n1
Chaque séquence invalidante du produit synchronisé quotient
doit correspondre
à une séquence invalidante dans le produit synchronisé ordinaire
Validité de l'approche quotient
Assurer par construction la préservation des séquences invalidantes
J-M Ilié, IRISA - Mai 2002 11
Exploitation des symétries pour la vérification
Cas des RDP symétriques
définir le sous groupe de symétries valides définition statiques de sous classes de couleurs actions : permutations préservant les sous classes de couleurs
Vérifier f = G (ph1.Thinking F ph1.Eating)
Raffinement : Philo = {ph1} {ph2,ph3}
b1 b2 b3
a1 a2 a3
A
B
b3
a1
A
B
b1 b1
a2 a3
G (a1 FXb3)true
A
B
a1
b3
a1
b3intérêt modèle et propriété fortement symétrique
J-M Ilié, IRISA - Mai 2002 12
Plate-forme de vérification symbolique
Interpréteur d'automate de Büchi
GMCnoyau de vérification
Interpréteursymbolique
(noyau GreatSPN)
automateRéseau Bien Formé
Interface IHM (AMI-NET)
Raffinement
Cas des symétries globales CLASS Philo PH1 is {ph1}PH2 is ph{2-4}
PROPw1 = PH1.Waitingw2 = exist PH2.Waitingw3 = all PH2.Waitingw4 = # PH2.Waiting > 2
e1 = PH1.Eatinge2 = exist PH2.Eatinge3 = all PH2.Eating
w1 & !w2 ! e1true
J-M Ilié, IRISA - Mai 2002 13
Les comportements asymétriques sont reportés sur ceux de l'automate de Büchi
Model Checking : produit synchronisé des automates
calcul des symétries locales
calcul à la volée des symétries du produit synchronisé symbolique
Définition du système (1) système symétrique
(2) un automaton de contrôle des asymétries
Automaton Ac
for the controlof asymmetry
Büchi
Automaton A¬f
SymmetricWN* *
Asymmetric system
Automaton Ac
for the controlof asymmetry
Büchi
Automaton A¬f * *
Asymmetric automaton Symmetric system
SymmetricWN
La plupart des systèmes et algorithmes distribués sont partiellement symétriques
Vérifier les systèmes partiellement symétriques
J-M Ilié, IRISA - Mai 2002 14
Application : Algorithme de Bagrodia
Rendez-vous distribué fonctionnant par paire de sitepossibilité de retardement de sites
Eviter les blocages : retard possible de sj par si seulement si sj > si
Comportement partiellement symétrique
J-M Ilié, IRISA - Mai 2002 15
Application : Algorithme de Bagrodia
iAti j < iReti,j
iAti
cA
\{k}
A1 = A \ A(1)
avec
cA
\ A(2)… k\
A(k)
cA cA cA
k+1A(1)… n A(n-
k)
A= k et A= n-k
avec kAavec kA
{k}
1 k k+1 n
j
iAti j<iReti,j
iAti
iAti j < iReti,j
iAti
ik+1Ati j < iReti,j
ik+1Ati
inAti j < iReti,j
inAti
j
j
j
j
n
Choix de l'automate de contrôlele plus symétrique possible
Seuls les sites mutuellement en attente de réponse peuvent être retardés Les sites qui ne sont pas en attente sont laissés symétriques
A paraître chez Hermes en 2002
iAti j < iReti,j Condition de retardement
J-M Ilié, IRISA - Mai 2002 16
distinguer parties asymmetriques and symétriques
RDP et Graphe de marquages symboliques étendu
prise en compte dynamique du sous groupe de symétries
Définir un ensemble de relations d'équivalence
d'états en fonctions d'un famille de sous groupes
construire un produit synchronisé quotient adapté
Pb : petit facteur de réduction dues aux contraintes de bissimulation de la relation
Ajami & al, 98
Autoriser les comportements symétriques mais seulement sur les états totalement symétriques
Pb : applications aux propriété de sûreté
Pb : très peu d'applicationsEmerson and Trefler, 99
Thèse de Zouari, 95
Sur le modèle
Sur l'automate de la formule
Exploiter les symétries partiellesun historique
J-M Ilié, IRISA - Mai 2002 17
Intérêt principal : indépendance de la structure de l'automate
Gb0 = GPhilo Gb1
= {2 3,identity} Gb2 = {identity}
w1 & ! e1
& t2 & t3
w2 & ! e1
b0 b1b2
Calcul de symétries locales
Chaque état permet localement de calculer un sous groupe de symétries
H0= {1,2,...} H1= {1} {2,3} H2= {1} {2} {3}
Représentation sous forme de partitions des couleurs Restriction locale des permutations
analogie : sous-classes statiques des réseaux bien formés
true
[Haddad, Ilié - FORTE 2000]
J-M Ilié, IRISA - Mai 2002 18
Contraintes :
(c1) chaque état de m satisfait b m m m |=b
(c2) les symétries d'états déduites de H préservent la classe d'états GH . m = m
<H, m, b>
partition représentation (symbolique) état de l'automate
de couleurs d'un ensemble de marquages
Etat du produit synchronisé symbolique
^
^
^ ^
^
J-M Ilié, IRISA - Mai 2002 19
la classe de marquages est définie par des symétries communes à GH1 et Gb2
m2 (GH1 Gb2 ) . m2
on peut exploiter d'autres symétries sur m2 tant que GH2 Gm2.
calcul d'un successeur valide
Soit <H1, m1, b1>
tel que b1b2 m1m1 : m1m2 et m2|= b2
Alors construire <H1, m1, b1> <H2, m2, b2>
H2 est choisi pour représenter un sous groupe de symétries (maximal)
au minimum : GH2 (GH1 Gb2 ) au plus GH2 Gm2
b1
b2
GH1.m1= m1
=|
=|
m2
m1
m1
m2
Calcul du produit synchronisé symbolique
^
^
^
^
^
^
GH2.m2= m2 ?
^
^^^
^ ^
J-M Ilié, IRISA - Mai 2002 20
Condition de regroupement de sous classes de couleurs
m = (S1+ S2 + S3) . Repos + (S1) . EnCours
Avec H= {S1 S2, S3}et Sites = S1 S2 S3et S1 = S2 = S3 = 1
^ m = (S1+ S2 + S3) . Repos + (S1) . EnCours
Avec H= {S1 S23}et Sites = S1 S23et S1 = 1 S23 =2
^
Pour 2 sous classes de couleurs - uniformité de chaque sous classe- même distribution d'états pour les deux classes
J-M Ilié, IRISA - Mai 2002 21
Intégration des symétries partielles pour la vérification
Interpréteurétendu
d'automate de Büchi
automate
Interface IHM (AMI-NET)
Automatede contrôledes asymétries
GMCnoyau de vérification
Interpréteursymbolique
Etendu(noyau
GreatSPN)
Réseau Bien Formésymétrique
Produit
Symétries locales
Cache des partitions locales de couleurs
Calcul des états symboliques successeurs
Match symbolique
J-M Ilié, IRISA - Mai 2002 22
Modèle pour l'évaluation de performances
RDP
Réseau de Petri Bien Formé Système symétrique Taux de franchissement sur les transitions fonction des sous classes statiques Poids sur les transitions immédiates Nombre de serveurs par transition
Graphe de marquages symboliques étiqueté Taux de sortie des Marquages
Equiprobabilité au sein d'un marquage symbolique Equivalence à une chaîne de Markov agrégée Analyse globale du graphe
Vérifier la condition d'ergodicité (régime permanent) test de forte connexité du
GMS Abstraire les marquages evanescents (probabilité nulle) Vérifier la condition d'agrégation (homogénéité des taux de sortie)
m1m2m̂
m̂'
J-M Ilié, IRISA - Mai 2002 23
symétries partiellespour l'évaluation de performances
Calcul de la Chaîne de Markov agrégé
Interpréteursymbolique
étendu(noyau
GreatSPN)
Réseau Bien Formé
Interface IHM (AMI-NET)
"Prise en compte dynamique" des sous classes de couleurs
Re-calcul de marquages symboliques
Raffinements de graphe Ergodicité Chaîne de Markov agrégée
Graphe de MarquagesSymbolique étendu
graphe très compact accessibilité préservée
Test ergodicité
J-M Ilié, IRISA - Mai 2002 24
Perspectives
Recherche Affiner la notion de symétries partielles Rapprocher le graphes de performance et de vérification Traitement des logiques temporisées probabilistes Intégrer la réduction de modèles
Atelier
Automatiser la construction des automates de contrôle des asymétries Traitement des logiques événementielles Introduire l'équité pour la vérification