Plan du cours

1 Problématique

Modélisation des Systèmes Répartis 2 Systèmes de transitions

Une modélisation par automates
3 Systèmes de transitions étiquetés
Propriétés
Emmanuelle Encrenaz-Tiphène Exemples

Master d’Informatique de l’Université Paris VI 4 Composition de systèmes

Spécialité SAR
Composition synchrone
Composition asynchrone
Exemples

5 Exercices

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 1 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 2 / 33

Problématique Problématique

Les composants à modéliser Les propriétés à vérifier

Propriété de sûreté
Processus ou threads Le système ne peut pas produire de comportement “défaillant”.
Deux processus en exclusion mutuelle n’accéderont jamais simultanément à la
algorithme séquentiel : automates (systèmes de transitions) ressource critique.
Le système ne peut pas se bloquer totalement.
Medium de communication
Décidable en examinant tous les états du système (nombre fini d’états).
variables globales
files de messages Propriété de vivacité
Le système évolue inévitablement vers “un progrès”.
Mode de synchronisation Tout message émis finira par être acquitté.
synchrone L’émetteur pourra toujours émettre de nouveaux messages.
asynchrone Le système repasse inévitablement par l’état initial.
Décidable en examinant les connexions entre les états du système
(automates finis).

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 3 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 4 / 33
 Systèmes de transitions Systèmes de transitions

Système de transitions (ou automate) Exemples de systèmes de transitions

Un compteur sur N
Définition
Q = N, T = {hx, x + 1i | x ∈ N}, q0 = 0
Un système de transitions est un triplet S = hQ, T , q0 i où :
Q est un ensemble d’états,
T ⊆ Q × Q est un ensemble de transitions reliant les états deux à deux,
q0 ∈ Q est l’état initial. 0 1 2 i

Un compteur modulo n
Q = {0, · · · , n − 1}, T = {hx, (x + 1) mod ni | x ∈ Q}, q0 = 0
Q = {v , w, x, y , z}
T = {hv , wi, hw, wi, hw, xi, hx, wi,
v w x
hw, y i, hy , zi, hz, xi}
0 1 2 i n−1
q0 = v
y z

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 5 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 6 / 33

Systèmes de transitions étiquetés Systèmes de transitions étiquetés

Système de transitions étiqueté Séquences de transitions

Définition
Un système de transitions étiqueté sur transition est un quadruplet
S = hQ, λ, T , q0 i où : Soit S = hQ, λ, T , q0 i un système de transitions étiqueté.
Q est un ensemble d’états, Le franchissement d’une transition hq, a, q 0 i ∈ T est noté
λ est un alphabet fini d’actions étiquetant les transitions, a
q −→ q0
T ⊆ Q × λ × Q est un ensemble de transitions reliant les états deux à
deux, Le franchissement d’une séquence de transitions hqi , ai , qi+1 i ∈ T (avec
q0 ∈ Q est l’état initial. 1 ≤ i < n) est noté
a1 a2 n−2 a n−1 a
q1 −→ q2 −→ . . . −→ qn−1 −→ qn
b Q = {v , w, x, y , z}
a λ = {a, b, c} a1 a2 n−1 a
a Soit σ = q1 −→ q2 −→ . . . −→ qn une séquence de transitions. La séquence
v w x T = {hv , a, wi, hw, b, wi, hw, a, xi, σ est dite être le support du mot a1 .a2 . . . an−1 .
b hx, b, wi, hw, c, y i, hy , a, zi, hz, b, xi}
c b q0 = v
y z
a
Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 7 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 8 / 33
 Systèmes de transitions étiquetés Systèmes de transitions étiquetés

Langage d’un système de transitions Exemple

Soient un système de transitions étiqueté S = hQ, λ, T , q0 i et un mot ω ∈ λ∗ .
Soit S le système de transitions étiqueté suivant :
Définition
b
Le mot ω est reconnu par S si et seulement s’il existe σ une séquence de
transitions telle que a
q1 q2
σ débute en q0 ,
σ est le support de ω. a c a

Soit un ensemble d’états terminaux F ⊆ Q. c q5 q4 q3

b c
Définition
Le mot ω est accepté par hS, F i si et seulement s’il existe σ une séquence de Soit F = {q3 , q5 } l’ensemble des états terminaux (représentés par un
transitions telle que double trait dans la figure ci-dessus).
σ débute en q0 et termine dans un état appartenant à F , Le langage de hS, F i correspond à l’expression régulière :
σ est le support de ω,
L’ensemble des mots acceptés est appelé le langage du système. (a.b∗ .(c.a + a.c.a))∗ .a.b∗ .(a + (c + a.c).b.c ∗ )

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 9 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 10 / 33

Systèmes de transitions étiquetés Propriétés Systèmes de transitions étiquetés Exemples

Propriétés des systèmes de transitions étiquetés Modélisation - exemples

Un système de transitions étiqueté est fini si et seulement si Un programme séquentiel

Q et T sont des ensembles finis.
début L’état du programme est défini par
Un système de transitions étiqueté est déterministe si et seulement si x ← 1; toutes les variables qui le
i ← 1; constituent et son état
∀hq, a, q 0 i, hq, b, q 00 i ∈ T , a = b ⇒ q 0 = q 00 . tant que (i < 3) faire d’avancement. Ici, un triplet
x ← 2 ∗ x; h compteur ordinal, x, i i.
Un système de transitions étiqueté est complet si et seulement si i ← i + 1;
fin Une transition représente
∀q ∈ Q, ∀a ∈ λ, ∃q 0 tel que hq, a, q 0 i ∈ T . fin l’exécution d’une instruction.

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 11 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 12 / 33
 Systèmes de transitions étiquetés Exemples Systèmes de transitions étiquetés Exemples

Système de transitions correspondant Une représentation correspondante par un automate

interprété
co = begin, x = ?, i = ?
co = begin

x←1 x
co = while, x = 1, i = 1
i←1
[i < 3]
x←2∗x co = while
co = while, x = 2, i = 2 i←i+1
[i ≥ 3] i

co = while, x = 4, i = 3 co = end

automate espace de données

co = end, x = 4, i = 3
Cet automate interprété produit les mêmes séquences de transition que le
système de transitions étiqueté précédent.
Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 13 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 14 / 33

Systèmes de transitions étiquetés Exemples Systèmes de transitions étiquetés Exemples

Modélisation - exemples L’automate interprété correspondant

Un programme séquentiel avec entrées indéfinies co = begin

x←1
début
x ← 1; i ←?
lire(i);
co = if
si (i < 3) alors
tant que (i < 3) faire
x ← 2 ∗ x; [i < 3] x
i ← i + 1; [i < 3]
fin [i ≥ 3]
x←2∗x co = while
sinon x←3∗x
i←i+1
x ← 3 ∗ x;
fin [i ≥ 3] i
fin
co = end

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 15 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 16 / 33
 Systèmes de transitions étiquetés Exemples Systèmes de transitions étiquetés Exemples

Abstraction de données Modélisation - exemples

Le digicode

co = begin
Les abstractions de données
peuvent être nécessaires mais Soit un digicode déclenchant l’ouverture d’une porte lorsque le code saisi est
elles doivent être faites sur les correct.
données n’ayant pas La saisie du code n’a lieu que lorsque la porte est fermée.
co = if d’influence sur le contrôle.
Le code est composé de trois digits.

La saisie d’un code correct provoque un bip sonore.

co = while Cet automate produit plus de Une touche spéciale (clear) permet la réinitialisation de la saisie.
séquences que les précédents
(notamment une divergence Un capteur détecte la fermeture de la porte.
dans la boucle).

co = end

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 17 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 18 / 33

Systèmes de transitions étiquetés Exemples Systèmes de transitions étiquetés Exemples

Modélisation - exemples Le système de transitions étiqueté correspondant

La modélisation du digicode

d0
Entrées (symbolisées par “ ?” sur les transitions) : ?digit1_KO ou ?clear
?digit1_OK
Les touches (digit, clear) tapées, ?digit2_KO ou ?clear
d1
l’état de la porte. ?digit2_OK
?digit3_KO ou ?clear
d2
?digit3_OK

Sorties (symbolisées par “ !” sur les transitions) : d3

!bip
Ouvrir la porte,
d4
émettre un signal sonore. !ouvrir_porte
?porte_fermée
d5 ?porte_ouverte

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 19 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 20 / 33
 Systèmes de transitions étiquetés Exemples Systèmes de transitions étiquetés Exemples

Modélisation - exemples Le système de transitions étiqueté correspondant

La porte

La porte peut être ouverte grâce à la commande du digicode, ou alors avec

une clé.
De même, elle peut être fermée manuellement, ou bien être bloquée en
position ouverte.
?ouvrir_porte ou ?clé
!porte_fermée p0 p1 !porte_ouverte
Entrées : ?fermer_porte
Commandes d’ouverture et de fermeture, clé.

Sorties :
L’état de la porte.

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 21 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 22 / 33

Composition de systèmes Composition de systèmes Composition synchrone

Composition de systèmes de transitions étiqueté Composition synchrone

Les sous-systèmes franchissent simultanément une transition.

Définition
Soient S1 = hQ1 , λ1 , T1 , q01 i et S2 = hQ2 , λ2 , T2 , q02 i deux systèmes de hq1 , q2 iha−→
1 ,a2 i
hq10 , q20 i ⇔
a1 a2
transitions étiquetés. ∃a1 ∈ λ1 tel que q1 −→ q10 et ∃a2 ∈ λ2 tel que q2 −→ q20
Le comportement du système global peut être représenté par un système de
transitions étiqueté S = hQ, λ, T , q0 i tel que
Q ⊆ Q1 × Q2 ,
λ ⊆ λ1 × λ2 ou λ ⊆ λ1 ∪ λ2 ∪ (λ1 × λ2 ), Contrainte de synchronisation
T ⊆ T1 × T2 , Soit un ensemble Υ ⊆ λ1 × λ2 .
q0 = hq01 , q02 i.
Une transition étiquetée ha1 , a2 i n’est autorisée que si elle appartient à Υ.

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 23 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 24 / 33
 Composition de systèmes Composition asynchrone Composition de systèmes Composition asynchrone

Composition asynchrone Construction du produit de deux systèmes

début
New ← hq01 , q02 i;
Les sous-systèmes fonctionnent indépendamment les uns des autres. S ← hNew, ∅, ∅, hq01 , q02 ii;
tant que (New 6= ∅) faire
hq1 , q2 i ← un état issu de New;
hq1 , q2 iha−→
1 ,a2 i
hq10 , q20 i ⇔
a1 a2 New ← New \ {hq1 , q2 i};
∃a1 ∈ λ1 tel que q1 −→ q10 et ∃a2 ∈ λ2 tel que q2 −→ q20 pour tous les hhq1 , a1 , q10 i, hq2 , a2 , q20 ii ∈ T1 × T2 faire
a1 a1
hq1 , q2 i−→ hq10 , q2 i ⇔ ∃a1 ∈ λ1 tel que q1 −→ q10 si (ha1 , a2 i ∈ Υ) alors
a2
hq1 , q2 i−→ a2
hq1 , q20 i ⇔ ∃a2 ∈ λ2 tel que q2 −→ q20 si (hq10 , q20 i est un nouvel état) alors
Ajoutez hq10 , q20 i à l’ensemble des états de S;
New ← New ∪ {hq10 , q20 i};
fin
Ajoutez hhq1 , q2 i, ha1 , a2 i, hq10 , q20 i, i aux transitions de S;
Ce mode de composition correspond à une composition synchrone pour
Ajoutez ha1 , a2 i à l’ensemble des étiquettes de S;
laquelle une action nulle a été ajoutée dans les alphabets λ1 et λ2 .
fin
fin
fin
fin
Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 25 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 26 / 33

Composition de systèmes Composition asynchrone Composition de systèmes Exemples

Exercice Composition - exemples

Le digicode et la porte

Construire le produit synchronisé des deux systèmes suivants en considérant

la contrainte de synchonisation Υ = {ha, ai, hb, bi} Contraintes de synchronisation :
1 Digicode
h ?digitn_OK, - i, h ?digitn_KO, - i,
a
p1 h !bip, - i, h ?clear, - i
q1 q3 a
a
b b b
2 Porte
h -, ?clé i, h -, ?fermer_porte i
q2 q4 p2 p3
b a 3 Synchronisation effective
b b b h !ouvrir_porte, ?ouvrir_porte i,
h ?porte_ouverte, !porte_ouverte i,
Peut-on atteindre les états hq2 , p3 i, hq2 , p2 i et hq4 , p3 i ? h ?porte_fermée, !porte_fermée i
Y-a-t-il un état de blocage ?

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 27 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 28 / 33
 Composition de systèmes Exemples Composition de systèmes Exemples

Le système de transitions étiqueté résultant de la Automates synchronisés

composition
h-, ?cléi
d0 , p0 h-, ?fermer_portei d0 , p1
h ?digit1_KO, -i ou h ?digit1_KO, -i ou
Systèmes finis (généralement).
h ?clear, -i h ?digit1_OK, -i h ?digit1_OK, -i h ?clear, -i
h ?porte_fermée, !porte_ferméei

h-, ?cléi
h ?digit2_KO, -i ou
d1 , p0 h-, ?fermer_portei d1 , p1
h ?digit2_KO, -i ou Modélisation du contrôle essentiellement : manipulation des données à
h ?clear, -i h ?clear, -i
h ?digit2_OK, -i
h-, ?cléi
h ?digit2_OK, -i l’extérieur.
h ?digit3_KO, -i ou h ?digit3_KO, -i ou
h ?clear, -i
d2 , p0 h-, ?fermer_portei d2 , p1 h ?clear, -i
h ?digit3_OK, -i h ?digit3_OK, -i Synchronisation extérieure au modèle.
h-, ?cléi
d3 , p0 h-, ?fermer_portei d3 , p1
h !bip, -i h !bip, -i
Collection de processus avec mécanismes de synchronisation à définir
h-, ?cléi
d4 , p0 h-, ?fermer_portei d4 , p1 (synchrone / asynchrone / messages).
h !ouvrir_porte, ?ouvrir_portei

d5 , p0 d5 , p1 Analyse sur le graphe produit uniquement.

h-, ?fermer_portei

h ?porte_ouverte, !porte_ouvertei

Que se passe-t-il si un usager

(i) ouvre la porte avec sa clé, (ii) tape le bon code, (iii) puis ferme la porte ?
Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 29 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 30 / 33

Exercices Exercices

Exercice : les philosophes Modélisation d’un philosophe et d’une baguette

Soit une table circulaire qui comporte cinq assiettes et cinq baguettes
pense
entre les assiettes.
Cinq philosophes assis à cette table mangent et pensent alternativement.
Pour manger les philosophes doivent s’emparer des deux baguettes de attend
part et d’autre de leur assiette. !prend droite !prend gauche

Lorsqu’ils se remettent à penser ils reposent leurs deux baguettes. attend gauche attend droite disponible
Les philosophes prennent et reposent leurs baguettes l’une après l’autre, !prend gauche !prend droite
?prend ?rend
dans un ordre indifférent. mange
Initialement tous les philosophes pensent. occupée
repose
!rend droite !rend gauche
1 Modélisez chaque philosophe par un automate distinct.
repose gauche repose droite
2 Comment modéliser les baguettes ?
!rend gauche !rend droite
3 Montrez que le système comprend des blocages.

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 31 / 33 Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 32 / 33
 Exercices

Modélisation d’une file de messages

vide
ajoute retire

1 message
ajoute retire

ajoute 2 messages
retire
ajoute retire

3 messages
ajoute retire

4 messages
ajoute retire

Emmanuelle Encrenaz-Tiphène (LIP6) Modélisation par automates M2-SAR-MSR 33 / 33