Modélisation des systèmes

MODÉLISATION.
EXEMPLES DE MODÈLES.
CONCEPTS GÉNÉRAUX.
AUTOMATES AVEC VARIABLES.
AUTOMATES COMMUNICANTS.
AUTOMATES TEMPORISÉES
ABSTRACTION

2024-2025 ©Myiam Fourati Cherif

 MODÉLISATION

2 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Modéliser des
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

systèmes
Abstraction

❑Un modèle d’un système doit décrire

fidèlement son comportement sans
ambigüité.

❑Généralement, les systèmes sont décrits

par des automates.

3 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Modéliser des
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

systèmes
Abstraction

❑Ces machines peuvent être :

❑simples comme les machines à états finis
(automates) ou
❑plus complexes (pour les vrais programmes)
comme les machines de Turing.
❑Plus le formalisme utilisé est puissant,
moins il peut être traité automatiquement.
❑Le formalisme doit aussi être décidable.

4 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Automates
Automates communicants
Automates temporisés
Abstraction

❑Les système qui s’apprêtent mieux au model-

checking sont modélisables par des structures
de kripke.
❑Il est possible aussi de considérer des systèmes
à états infinis, mais ceci sort du cadre du cours.
❑Un automate est un modèle de machine évaluant
d’état en état sous l’effet de transitons :
❑Les états sont représentés par des : ,
❑Les transitions par des flèches : ,
❑L’état initial est marqué :
5 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Automates
Automates communicants
Automates temporisés
Abstraction

❑Un automate est un terme générique utilisé pour

désigner plusieurs concepts : système de
transition étiqueté ou pas, structure de Kripke,
etc..
❑Un automate est en général un quadruplet
M=(S,s0,E,R,F) :
❑S est un ensemble d’états,
❑s0S est l’état initial.
❑E est un ensemble d’étiquettes de transitions,
❑RSES est un ensemble de transitions.
❑F est un ensemble d’états finaux. ©Myriam Fourati Cherif
6
 EXEMPLES DE MODÈLES

7 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Exemple 1 :
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

montre digitale
Abstraction

❑Une montre digitale (qui indique seulement

l’heure et la minute) peut être représentée
par un automate :
❑Chaque état donne l’heure et les minutes
courantes  2460 états possibles.
❑Une transition relie toute paire d’états distants
d’une minute.
00:00 00:01 00:02 23:58 23:59

8 ©Myriam Fourati Cherif

 Modélisation

Exemple 2 :
Exemples de modèles
Concepts généraux
Automates avec variables

compteur modulo
Automates communicants
Automates temporisés
Abstraction

3 (M3)
❑Les états correspondent aux valeurs du
compteur.
❑Les transitions traduisent les actions
possibles sur le compteur : incrémentation
ou décrémentation.
M3=(S, s0,E,R) inc
0 1
S={0,1,2}, s0=0,E={inc,dec} dec
dec
R={(0,inc,1),(1,inc,2),…(2,dec,1),…} inc
dec
inc
2

9 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Exercice
Automates communicants
Automates temporisés
Abstraction

❑Représentez une machine de distribution

de boissons (jus et soda) par un automate.

payer

Prendre-jus Prendre-soda
Insérer-
pièce

jus choisir soda

 

10 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Exemple 3 :
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

Digicode
Abstraction

❑Pour ouvrir la porte d’un immeuble par

exemple.
❑La porte s’ouvre dès qu’on a tapé la bonne
combinaison (suite de caractères).
❑Pour le but de l’exemple, on suppose que
même si on commence par une mauvaise
combinaison, il suffit de finir avec la bonne.
❑3 touches sont possibles : A, B, C.
❑Le code est ABA. ©Myriam Fourati Cherif
11
 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Modélisation
Automates communicants
Automates temporisés
Abstraction

❑Automate à 4 états et 9 transitions :

B A
C
A B A
1 2 3 4
C

B
C

12 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Exécution
Automates communicants
Automates temporisés
Abstraction

❑ Pour spécifier des propriétés, on s’intéresse moins aux

transitions (mais possible) et on focalise sur l’exécution.
❑ Une exécution est une suite d’états décrivant une
évolution du système : 11,112, 1121, 12234, 112312234,
….
❑ Pour considérer toutes les exécutions possibles du
système, on peut par exemple les ranger par ordre de
longueur :
❑ 11,12
❑ 111, 112,121,122,123
❑…

13 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Arbre
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

d’exécution
Abstraction

❑Toutes les exécutions du système peuvent être

représentées par un arbre d’exécution (arbre
infini en largeur et en profondeur).
1

1 2

1 2 1 2 3

1 2 1 2 3 1 2 1 2 3 1 4

…………………………………….
14 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Propriétés
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

élémentaires
Abstraction

❑Pour vérifier des propriétés du système

(modèle), on associe à chaque état de
l’automate des propriétés élémentaires
(satisfaites à cet état) modélisées par des
propositions atomiques.
❑Exemples :
❑« la porte est ouverte » est vraie dans l’état 4
et fausse dans les autres états (1,2,3).

15 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Propriétés
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

vérifiables
Abstraction

❑On peut ainsi vérifier des propriétés

intéressantes telles que :
❑« Si la porte s’ouvre (une exécution arrive
dans l’état 4) alors les trois dernières lettres
tapées sont dans l’ordre A,B,A ».
❑« Toute suite de lettres tapées finissant par
ABA ouvre la porte (définit une exécution
menant à l’état 4) ».

16 ©Myriam Fourati Cherif

 Modélisation

Propositions
Exemples de modèles
Concepts généraux
Automates avec variables

atomiques pour le
Automates communicants
Automates temporisés
Abstraction

digicode
❑PA : on vient nécessairement de taper un A
(vraie dans les états 2 et 4).
❑PB : on vient nécessairement de taper un B
(vraie dans l’état 3 uniquement).
❑PC : on vient nécessairement de taper un C
(n’est vraie dans aucun état).
❑pred2 : l‘état précédent dans une exécution est
nécessairement un 2 (vraie dans l’état 3).
❑pred3 : l‘état précédent dans une exécution est
nécessairement un 3 (vraie dans l’état 4)
17 ©Myriam Fourati Cherif
 Modélisation

Propositions
Exemples de modèles
Concepts généraux
Automates avec variables

atomiques pour le
Automates communicants
Automates temporisés
Abstraction

digicode

B A
C

1 A 2 B 3 A 4
PA PB PA
C pred2 pred3

B
C

18 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Exercice
Automates communicants
Automates temporisés
Abstraction

❑Vérifier la propriété :
« Si la porte s’ouvre (une exécution arrive dans
l’état 4) alors les trois dernières lettres tapées
sont dans l’ordre A,B,A ».

❑C’est une propriété qui peut bien être

vérifiée automatiquement par un model
checker.

19 ©Myriam Fourati Cherif

 CONCEPTS GÉNÉRAUX

Myriam Fourati Cherif 2014-2015 20

20 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux

Système de
Automates avec variables
Automates communicants
Automates temporisés

transition étiqueté
Abstraction

❑ A=(Q,q0,E,T) :
❑ Q est un ensemble fini d’états.
❑ E est un ensemble fini d’étiquettes de transition.
❑ T Q  {E{}}  Q est l’ensemble de transitions, avec  est une
action interne non observable. Sachez que (q,e,q’) est souvent
𝑒 a
notée 𝑞 ՜ 𝑞′.
q0 q1
❑ q0 est l’état initial. c

❑Exemple. q3
b

❑Mais comment spécifier une propriété dans un

état : dans l’état initial d’un robot aspirateur, le
bac est vide.
21 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Système de
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

Kripke
Abstraction

❑A=(Q,q0,E,T,Prop,l) :
❑Q est un ensemble fini d’états.
❑E est un ensemble fini d’étiquettes de transition.
❑T Q  E  Q est l’ensemble de transitions.
❑ q0 est l’état initial.
❑Prop est un ensemble de propositions atomiques
{P1,P2,…,Pn}.
❑ l : Q →2Prop application d’étiquetage des états par des
propositions.(associe à tout état l’ensemble fini des
propriétés élémentaires vérifiées dans l’état).

22 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Chemin
Automates communicants
Automates temporisés
Abstraction

❑ Un chemin  de l’automate A est une suite , finie ou

infinie, de transitions (qi,ei,qi’) de A qui s’enchainent
(q’i=qi+1), et on note

❑ Exemple : .
❑ La longueur d’un chemin  (notée | |) est le nombre de
transitions qu’il contient ( s’il est infini).
❑ Le ième état de  ((i)) est l’état qi atteint après i transitons
(défini si i <| |).

23 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Exécution
Automates communicants
Automates temporisés
Abstraction

❑Une exécution est une suite d’états

décrivant une évolution du système.
❑Une exécution partielle de A est un chemin
partant de l’état initial q0 :
❑Une exécution complète est une exécution
qu’on ne peut pas prolonger (infinie ou se
termine dans un état sans successeur).

24 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Atteingabilité
Automates communicants
Automates temporisés
Abstraction

❑Un état est dit atteignable (accessible)

s’il apparaît au moins une fois dans
l’arbre d’exécution de l’automate.
❑Le passage par un état peut être utilisé
pour démonter des propriétés du système :
❑Dans un système de commande d’une porte
la vérification de l’atteingabilité de l’état
porte_fermée dans l’automate correspondant
à démonter la propriété « la porte peut être
fermée ».
25 ©Myriam Fourati Cherif
 AUTOMATES AVEC
VARIABLES
26

26 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux

Automates avec
Automates avec variables
Automates communicants
Automates temporisés

variables d’états
Abstraction

❑Introduire des données (variables) de contrôle.

❑Souvent nécessaire pour modéliser des
systèmes réels.
❑Exemple : dans les protocoles de
communication, il serait intéressant de compter
le nombre de paquets reçus, émis, nombre
d’erreurs, etc.
❑Permettent aussi de réduire le nombre d’états de
l’automate.

27 ©Myriam Fourati Cherif

 Modélisation

Définition :
Exemples de modèles
Concepts généraux
Automates avec variables

Automate avec
Automates communicants
Automates temporisés
Abstraction

variables
❑A=(Q,q0,E,T,Prop,Var,l) :
❑Q est un ensemble fini d’états.
❑E est un ensemble fini d’étiquettes de transition.
❑T Q  E  Q est l’ensemble de transitions.
❑ q0 est l’état initial.
❑Prop est un ensemble de propositions atomiques
{P1,P2,…,Pn}.
❑Var est un ensemble de variables {v1, ..., vn}, chaque
vi peut prendre des valeurs un domaine Dvi,
❑ l : Q →2Prop application d’étiquetage des états.

28 ©Myriam Fourati Cherif

 Modélisation

Manipulation des
Exemples de modèles
Concepts généraux
Automates avec variables

variables par
Automates communicants
Automates temporisés
Abstraction

l’automate
❑Le lien entre l’automate et les variable peut
être :
❑D’affectation : une transition peut modifier la
valeur d’une ou plusieurs variables.
❑De garde : une transition peut être gardée par
une condition sur les variables. Ainsi, pour
franchir la transition il faut que la condition sur
les variables soit vérifiée.

29 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Exemple :
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

Digicode
Abstraction

B A
C
A B A
1 2 3 4
C

B
C
❑Cette modélisation du digicode n’est pas réaliste,
c’est ainsi que nous l’améliorons en ajoutant un
compteur de nombre d’erreurs commises par
l’utilisateur et n’autoriser que 3 erreurs.
❑Nous ajoutons donc une variable entière cpt,
initialisée à 0.
30 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles
Concepts généraux

Lien entre
Automates avec variables
Automates communicants
Automates temporisés

l’automate et cpt
Abstraction

❑Affectation : les transitions correspondantes à

une erreur incrémentent le compteur.
❑Qu’elles sont ces transitions ?
B A
C
A B A
1 2 3 4
C

B
C

31 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux

Lien entre
Automates avec variables
Automates communicants
Automates temporisés

l’automate et cpt
Abstraction

❑Affectation : les transitions correspondantes à

une erreur incrémentent le compteur.
❑Qu’elles sont ces transitions ?
B A cpt := cpt+1
cpt := cpt+1
C
A B A
1 2 3 4
C
cpt := cpt+1

B cpt := cpt+1
C
❑Au fait toutes les transitions sauf (1,A,2),(2,B,3)
et (3,A,4) menant à l’ouverture de la porte.
32 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles
Concepts généraux

Lien entre
Automates avec variables
Automates communicants
Automates temporisés

l’automate et cpt
Abstraction

❑Garde : pour tolérer au maximum 3

erreurs, il faut marquer les transitions
correspondant à une erreur par une
condition de garde : cpt<3.
B cpt <3
cpt := cpt+1 A cpt := cpt+1
cpt <3 C
A B A
1 2 3 4
C
cpt := cpt+1
cpt <3
B cpt := cpt+1
C cpt <3

33 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Conventions
Automates communicants
Automates temporisés
Abstraction

❑Les gardes sont les premières à spécifier et sont

précédées par le mot clé si.
❑Ils sont suivis des étiquettes des actions.
❑Suivis des affectations.
Si cpt <3 Si cpt <3
B,C A
cpt := cpt+1 cpt := cpt+1
A A
1 2 3 4
B
Si cpt <3
C
cpt := cpt+1
Si cpt <3
B,C
cpt := cpt+1
34 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Amélioration du
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

Digicode
Abstraction

❑Déclencher une alarme si 4 erreurs sont

commises.

❑Ajouter un état err et 3 transitions

entrantes issues des trois états : 1,2,3 et
gardées par si cpt=3.

35 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Digicode
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

amélioré (A)
Abstraction

Si cpt :<3 Si cpt :<3

B,C A
cpt := cpt+1 cpt := cpt+1
A A
1 2 3 4
B

Si cpt <3
C
cpt := cpt+1
Si cpt =3
Si cpt <3 B,C
Si cpt =3 B,C
B,C cpt := cpt+1 cpt := cpt+1
cpt := cpt+1
err
Si cpt =3
A,C
cpt := cpt+1
36 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Dépliage de
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

l’automate
Abstraction

❑Pour appliquer des méthodes de

vérification telles que le model checking, il
est nécessaire de travailler sur des
modèles dépliés.
❑Uniquement les transitions possibles sont
présentes.
❑L’automate déplié est un graphe d’états
appelé souvent système de transitions.

37 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux

Construction de
Automates avec variables
Automates communicants
Automates temporisés

l’automate déplié
Abstraction

❑Construction des états : pour chaque état de A,

créer autant d’états (appelés globaux) qu’il y a
de valeurs des variables utilisées.
❑Construction des transitions :
❑déplier les transitions entre les occurrences d’état si la
garde est vraie,
❑les transitions ne sont plus gardées car on connaît les
valeurs des variables des états globaux,
❑supprimer les affectations des variables, car les états
contiennent directement les valeurs de variables.
❑Supprimer les états non atteignables.
38 ©Myriam Fourati Cherif
 Modélisation

Digicode avec
Exemples de modèles
Concepts généraux
Automates avec variables

comptage des
Automates communicants
Automates temporisés
Abstraction

erreurs

39 ©Myriam Fourati Cherif

 AUTOMATES
COMMUNICANTS
40

40 ©Myriam Fourati Cherif

 Modélisation

Compositions de
Exemples de modèles
Concepts généraux
Automates avec variables

structures de
Automates communicants
Automates temporisés
Abstraction

Kripke
❑Les modèles de Kripke complexes sont
obtenus généralement par composition
d’autres modèles : produits de systèmes.
❑On parle de produit cartésien pour les
systèmes indépendants.
❑On parle de produit synchronisé pour les
systèmes dépendants.

41 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Modèles
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

Composés
Abstraction

❑Permettent de modéliser des systèmes

découpés en modules ou sous-systèmes.
❑Ils sont adéquats pour abstraire les
systèmes parallèles et/ou distribués.
❑Consiste à modéliser chaque composante
du système, ensuite de les faire coopérer.

42 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Composants
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

sans interaction
Abstraction

❑Il suffit de représenter chaque composant

par une structure de Kripke.
❑Construire la structure qui soit le produit
cartésien des structures modélisant les
composants.
❑Un état global n’est autre qu’un vecteur
composé des différents états (locaux) des
composants.

43 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Exemple :
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

compteur
Abstraction

❑Un système composé de 3 compteurs :

modulo 2, modulo3 et modulo 4.
Compteur modulo 2 M2
Inc Compteur modulo 3 M3
dec inc
0 1 0 1
dec dec
dec
inc inc
Compteur modulo 4 M4 inc dec
inc 2
0 1
dec
inc dec inc dec
dec
3 2
inc
44 ©Myriam Fourati Cherif
 Modélisation

Les états de
Exemples de modèles
Concepts généraux
Automates avec variables

l’automate
Automates communicants
Automates temporisés
Abstraction

composé
❑L’automate M234 (produit cartésien des
automates M2, M3 et M4) contient
234=24 états.
❑Chaque état est étiqueté par un vecteur de
trois éléments chacune pouvant être : 0,1,
2 ou 3.

45 ©Myriam Fourati Cherif

 Modélisation

Etats du produit
Exemples de modèles
Concepts généraux
Automates avec variables

des 3 compteurs
Automates communicants
Automates temporisés
Abstraction

46 ©Myriam Fourati Cherif

 Modélisation

Transitions de
Exemples de modèles
Concepts généraux
Automates avec variables

l’automate
Automates communicants
Automates temporisés
Abstraction

composé
❑Il n’y a pas de synchronisation, chaque transition
permet l’incrémentation ou la décrémentation de
un ou plusieurs compteurs individuels :
333=27 choix.
❑Il est possible qu’un compteur reste stable, ceci
sera modélisé par le symbole « _ ».
❑Notez que ce symbole n’existait pas dans les
compteurs individuels. Pourquoi ?
❑Il y a 27-1=26 (on élimine celle où aucun
compteur n’évolue) transitions possibles dans
chaque état  24 26 = 624 transitions.
47 ©Myriam Fourati Cherif
 Modélisation

Quelques
Exemples de modèles
Concepts généraux
Automates avec variables

transitions de
Automates communicants
Automates temporisés
Abstraction

M234

48 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Produit
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

synchronisé
Abstraction

❑Effectué pour les systèmes dépendants.

❑Nous désirons obtenir le produit de n
automates : Ai =<Qi,Ei,Ti,q0,i,li>, i=1,…,n.
❑Nous avons besoin d’un symbole spécial
« - » pour exprimer la stabilité d’un
composant.
❑Le produit cartésien A1  A2 …  An est
l’automate A =<Q,E,T,q0,l> et est noté A1 ∥
A2 ∥ … ∥ An, calculons le.
49 ©Myriam Fourati Cherif
 Modélisation

Produit
Exemples de modèles
Concepts généraux
Automates avec variables
Automates communicants

synchronisé
Automates temporisés
Abstraction

❑Le produit cartésien A1  A2 …  An est

l’automate A =<Q,E,T,q0,l> avec :
❑Q=Q1 Q2  …  Qn(
❑E=1i n(Ei{-}),
❑T={((q1,q2,… ,qn), (e1,e2,… ,en), (q’1,q’2,… ,q’n))|i : ei=‘-’
et q’i=qi, ou ei ‘-’ et (qi,ei,q’i) Ti}
❑q0=(q01,q02,… ,q0n),
❑l((q1,q2,… ,qn))= 1i n li(qi).
❑Pour synchroniser les composants, nous
restreignons les transitions autorisées :
❑Sync 1i n(Ei{-}).
50 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Produit
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

synchronisé
Abstraction

❑Les composants évoluent selon une

fonction de synchronisation.
❑Exemples :
❑Exiger que les 3 compteurs évoluent en même
temps et au même rythme : étiquettes
possibles « inc,inc,inc » et « dec,dec,dec ».
❑Un seul compteur peut évoluer à la fois.
❑Les compteurs évoluent en couple

51 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Produit
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

synchronisé
Abstraction

❑Pour avoir un automate composé qui

couple fortement les 3 compteurs (M234c)
Sync sera définie par :
❑Sync ={(inc,inc,inc),(dec,dec,dec)}.
❑La fonction T doit donc être redéfinie :
❑T={((q1,q2,… ,qn), (e1,e2,… ,en), (q’1,q’2,…
,q’n))| (e1,e2,… ,en)  Sync et i : ei=‘-’ et
q’i=qi, ou ei ‘-’ et (qi,ei,q’i) Ti}

52 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux

M234c avec les

Automates avec variables
Automates communicants
Automates temporisés

états atteignables
Abstraction

53 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

M234c Nettoyé
Automates communicants
Automates temporisés
Abstraction

54 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Problème
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

d’explosion
Abstraction

❑Trouver l’ensemble des états atteignables dans un

produit synchronisé est un problème difficile.
❑Heureusement que cette procédure est
généralement automatisable.
❑Elle consiste à explorer tous les états du produit
synchronisé.
❑Le produit synchronisé des automates A1, A2, …,
Ap ayant respectivement les états n1, n2, …, np,
aura n1  n2 …np états  nombre exponentiel
en p : problème de l’explosion du nombre d’états.
55 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Problème
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

d’explosion
Abstraction

❑L’utilisation de variables peut aussi causer

un problème d’explosion d’états.
❑Lors du dépliage, les valeurs prises par
une variable peuvent être infinies.
❑Une solution serait l’utilisation des réseaux
de Petri (adaptés pour les systèmes
parallèles).

56 ©Myriam Fourati Cherif

 Modélisation

Variantes du
Exemples de modèles
Concepts généraux
Automates avec variables

produit
Automates communicants
Automates temporisés
Abstraction

synchronisé
❑Synchronisation par envoie de
message.

❑Synchronisation par variables

partagées.

57 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Synchronisation
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

par message
Abstraction

❑Il s’agit de la synchronisation par

envoie/réception de messages.
❑Il existe deux sortes d’étiquettes pour les
transitions :
❑Emission d’un message : !m.
❑Réception d’un message : ?m.
❑Dans le produit synchronisé par message,
seulement les transitions où l’émission est
accompagnée de la réception correspondantes
sont autorisées.
58 ©Myriam Fourati Cherif
 Modélisation

Exemple1 : envoie
Exemples de modèles
Concepts généraux
Automates avec variables

et réception de
Automates communicants
Automates temporisés
Abstraction

messages
❑Partage d’une donnée v entre deux
systèmes A1 et A2 : calcul et traitement.

59 ©Myriam Fourati Cherif

 Modélisation

Exemple1 : envoie
Exemples de modèles
Concepts généraux
Automates avec variables

et réception de
Automates communicants
Automates temporisés
Abstraction

messages
❑Partage d’une donnée v entre deux
systèmes A1 et A2 : calcul et traitement.
A1
Fin calcul Préparation !Msg(v) Attente
Calcul v
(C1) d’émission Ack
(C2) (C3)

?Ack

60 ©Myriam Fourati Cherif

 Modélisation

Exemple1 : envoie
Exemples de modèles
Concepts généraux
Automates avec variables

et réception de
Automates communicants
Automates temporisés
Abstraction

messages
❑Partage d’une donnée v entre deux
systèmes A1 et A2 : calcul et traitement.
A1
Fin calcul Préparation !Msg(v) Attente
Calcul v
(C1) d’émission Ack
(C2) (C3)

?Ack

A2
Attente ?Msg(v) Préparation !Ack
Traitement
message Ack (T3)
(T1) (T2)

Fin Traitement
61 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Synchronisation
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

de A1 et A2
Abstraction

❑A =A1  A2 <FC,FT>
<-,FT>
<?Ack,->
C1,T1 <-,?Msg> C1,T2 <-,!Ack> C1,T3

<FC,?Msg> <FC, !Ack>

<FC,-> <FC,-> <FC,->

C2,T1 <-,?Msg> C2,T2 <-,!Ack> C2,T3 <-,FT>

<!Msg,?Msg>
<?Ack,-> <!Msg,-> <!Msg,FT>
<!Msg,-> <!Msg,->
<?Ack,?Msg> <?Ack,!Ack>
C3,T1 <-,?Msg> C3,T2 <-,!Ack> C3,T3

<-,FT> <?Ack,FT>

62 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Contrainte de
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

synchronisation
Abstraction

❑La contrainte de synchronisation entre ces

deux automates se réduit à la simultanéité
des émissions/réceptions de messages :
❑Transitions de la forme (!t,?t) : !t A1,?t A2,
ou inversement.
❑Transitions ne contenant aucune émission
et/ou réception de messages.
❑Sync = {<!Msg,?Msg>, <!Ack,?Ack>,
<FC,FT>, <-,FT>, <FC,->}
63 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés
A1  A2
Synchronisé
Abstraction

❑A s =A1 || A2 <FC,FT>
<-,FT>

C1,T1 C1,T2 C1,T3

<FC,-> <FC,-> <FC,->

C2,T1 C2,T2 C2,T3 <-,FT>

<!Msg,?Msg>
<?Ack,!Ack>
C3,T1 C3,T2 C3,T3

<-,FT>

64 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Exemple 2 :
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

Ascenseur
Abstraction

❑Ascenseur à trois étages (rez-de-chaussée, 1er,

2ème)
❑Cinq composants :
❑Une Cabine : qui monte et descend,
❑Trois portes (une par étage) : qui s’ouvrent et se
ferment,
❑Un contrôleur : contrôle les 3 portes et la cabine par
émission d’ordre.
❑Nous négligeons le monde extérieur au système
(appels à l’ascenseur)
65 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Modélisation
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

des composants
Abstraction

❑Cabine

?descend ?monte

?monte ?monte
0 1 2

?descend ?descend

66 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Modélisation
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

des composants
Abstraction

❑Porte numéro i

?fermer_i ?ouvrir_i

?ouvrir_i
F O

?fermer_i

67 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Modélisation
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

des composants
Abstraction

❑Contrôleur
PO2 !fermer_2 PF2 !descend

2à0
!ouvrir_2

!descend
!monte
!descend

PO1 !fermer_1 PF1

!monte
!ouvrir_1

!descend
!monte
0à2

PO0 !fermer_0 PF0

!monte
!ouvrir_0
68 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Synchronisation
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

de l’ascenseur
Abstraction

❑Le produit des 5 composants contient :

❑Des états à 5 éléments <porte0,porte1,porte2,cabine,contrôleur>
❑Des transitions à 5 éléments, un pour chaque système
(porte0, porte1, porte2, cabine, contrôleur).
❑La contrainte de synchronisation Sync garantie
la simultanéité des émissions/réception de
messages :
❑ Sync={<?ouvrir_0,-,-,-,!ouvrir_0>, <?fermer_0,-,-,-,!fermer_0>,
<-,?ouvrir_1,-,-,!ouvrir_1>, <-,?fermer_1,-,-,!fermer_1>,
<-,-, ?ouvrir_2,-,!ouvrir_2>, <-,-, ?fermer_2,-,!fermer_2>,
<-,-,-,?descend,!descend>,<-,-,-,?monte,!monte>} .
69 ©Myriam Fourati Cherif
 Modélisation

Spécification de
Exemples de modèles
Concepts généraux
Automates avec variables

propriétés pour
Automates communicants
Automates temporisés
Abstraction

l’ascenseur
❑Avant de livrer ce produit, il est utile de
s’assurer qu’il ne cause pas d’ennuis à ses
utilisateurs.
❑Il est important de vérifier :
❑(P1) « la porte d’un étage ne peut s’ouvrir si la
cabine n’est pas à cet étage ».
❑(P2) « la cabine ne peut se déplacer si une
des portes est ouverte ».

70 ©Myriam Fourati Cherif

 Modélisation

Vérification de
Exemples de modèles
Concepts généraux
Automates avec variables

propriétés de
Automates communicants
Automates temporisés
Abstraction

l’ascenseur
❑(P1) signifie pour la porte 0 : tout état ayant « o »
comme premier composant (porte 0 ouverte), a
nécessairement « 0 » comme quatrième
composant (la cabine est dans l’étage 0).
❑Il suffit donc de vérifier qu’il n’existe pas d’états
atteignables ayant sous la forme :
❑(o,-,-,1,-) ou
❑(o,-,-,2,-)
❑Cette propriété peut être vérifiée aussi pour les
autres portes.
71 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Messages
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

asynchrones
Abstraction

❑Lorsque les messages ne sont pas reçus

instantanément : communication asynchrone.
❑Les messages émis et non encore reçus sont
stockés dans des canaux de communication
(buffers) et gérés en FIFO.
❑Le buffer est synchronisé avec l’émetteur et le
récepteur, mes ces derniers sont asynchrones.
❑Peut être représenté par un automates
synchrone nonPlein(F) nonVide(F)
?X X:=Tete(F)
enfile(F,X) !X
72 ©Myriam Fourati Cherif
 Modélisation

Conclusion sur la
Exemples de modèles
Concepts généraux
Automates avec variables

synchronisation
Automates communicants
Automates temporisés
Abstraction

par message
❑Communication synchrones est utilisée
pour modéliser les système de
contrôle/commande.

❑Communication asynchrones est souvent

utilisée pour modéliser des protocoles de
communication.

73 ©Myriam Fourati Cherif

 Modélisation

Synchronisation
Exemples de modèles
Concepts généraux
Automates avec variables

par variable
Automates communicants
Automates temporisés
Abstraction

partagée
❑Il s’agit de faire communiquer des automates en
les faisant partager des variables.
❑Utiliser les variables locales à chaque automate
comme des variables globales partagées par
l’automate synchrone.
❑Exemple : imprimante partagée par deux
personnes A et B on utilisera une variable
partagée tour indiquant lequel des deux a le droit
d’imprimer.

74 ©Myriam Fourati Cherif

 Modélisation

Exemple :
Exemples de modèles
Concepts généraux
Automates avec variables

imprimante
Automates communicants
Automates temporisés
Abstraction

partagée
❑ Utilisateur A
Si tour=A
Imprime A

X Y
Tour := B
tour est une variable partagée
❑ Utilisateur B par les deux automates

Si tour=B
Imprime B

Z W
Tour := A

75 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Imprimante
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

synchronisée
Abstraction

❑ L’état initial dépend de l’initialisation de tour (ici A).

x,z,A x,z,B
Tour :=A Tour :=B
Imprime B
Imprime A
x,w,A x,w,B

y,z,A y,z,B

y,w,A y,w,B

76 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Imprimante
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

synchronisée
Abstraction

❑ L’automate synchronisé avec états atteignables.

x,z,A Tour :=A Tour :=B x,z,B

Imprime A Imprime B

x,w,B
y,z,A

❑ Il est évident que ce protocole d’impression simpliste

fonctionne bien puisqu’aucun état de la forme (y,w,-)
n’est atteignable.
❑ Sauf qu’il ne permet pas des impressions simultanées
pour un seul utilisateur.
77 ©Myriam Fourati Cherif
 Modélisation

Imprimante
Exemples de modèles
Concepts généraux
Automates avec variables

partagée par
Automates communicants
Automates temporisés
Abstraction

Peterson
❑Deux processus PA et PB, trois variables
partagées :
❑dA : l’utilisateur A met à vrai s’il veut imprimer.
Initialement elle est fausse.
❑ dB : l’utilisateur B met à vrai s’il veut imprimer.
Initialement elle est fausse.
❑tour : départage le conflit.

78 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux

Code de Peterson
Automates avec variables
Automates communicants
Automates temporisés

pour PX
Abstraction

❑X = A si X=B et A sinon.
dx := vrai
tour := X
tant que (dx && tour = X)
//Attendre
section_critique()
dx := faux
❑Garantit plusieurs propriétés, entre autres
l’exclusion mutuelle.
79 ©Myriam Fourati Cherif
 Modélisation

Imprimante de
Exemples de modèles
Concepts généraux
Automates avec variables

Peterson
Automates communicants
Automates temporisés
Abstraction

synchronisée
❑ L’utilisateur A chez Peterson
dA:=vrai
1 2
dA :=faux

tour :=B
Si tour = A, Imprime A
4 3

Si dB = faux, Imprime A

❑ L’utilisateur B est construit de la même façon.

80 ©Myriam Fourati Cherif

 Modélisation

Propriétés de
Exemples de modèles
Concepts généraux
Automates avec variables

l’automate de
Automates communicants
Automates temporisés
Abstraction

Peterson
❑Un état de l’automate synchronisé est un
quintuplet (état de A, état de B, valeur dA, valeur
dB, valeur de tour). L’automate a donc 44  2  2
 2 = 128 états.
❑Le nombre d’états atteignables est 21.
❑Un model checker peut vérifier qu’aucun état de la
forme (4,4,-,-,-) n’est atteignable garantissant
l’impossibilité d’impression simultanée par A et B .
❑Il peut aussi vérifier que toute demande
d’impression finit par être satisfaite.
81 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Produit
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

synchrone
Abstraction

❑Cas particulier du produit synchronisé :

systèmes totalement dépendants.
❑Les composants doivent évoluer en même
temps.
❑A chaque instant tous les sous systèmes
doivent exécuter une action.
❑Exemple : feu de circulation.

82 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Produit
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

asynchrone
Abstraction

❑Cas particulier du produit synchronisé :

systèmes indépendants.
❑Exécution non simultanée des sous
systèmes (interleaving).
❑A chaque instant un seul composant est
autorisé à exécuter une transition.
❑Exemple : protocoles de communication.

83 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Automates
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

temporisés
Abstraction

❑Les automates classiques permettent de

modéliser des systèmes à événements discrets
sans considération du délais (temps) séparant 2
actions.
❑Une propriété non temporelle (ordonnancement) :
❑ si détection d’erreur alors déclenchement d’alarme.
❑Une propriété temporelle (délai) :
❑si détection d’erreur alors déclenchement d’alarme dans
moins de 5s.

84 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Pourquoi
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

temporiser ?
Abstraction

❑Cette notion temporelle est importantes

pour la modélisation des systèmes réactifs
(temps réel).

85 ©Myriam Fourati Cherif

 Modélisation

Modélisation des
Exemples de modèles
Concepts généraux
Automates avec variables

automates
Automates communicants
Automates temporisés
Abstraction

temporisés
❑Pour modéliser des automates temporisés,
il est possible d’ajouter des horloges
globales contrôlant les actions d’un réseau
d’automates.
❑Deux façons de représenter l’horloge :
❑Temps discret,
❑Temps continu.

86 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Temps discret
Automates communicants
Automates temporisés
Abstraction

❑Les valeurs du temps sont des entiers

positifs.
❑Une transition spéciale ajoutée à
l’automate classique : ticks d’horloge pour
marquer l’écoulement du temps (unité
choisie).
❑Le temps est discret car entre 2 ticks
successifs, le comportement du système
est non observable.
87 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Exemple d’un
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

Gradateur
Abstraction

❑ Interrupteur intelligent (gradateur) :

Appuyer Appuyer
éteint estompé allumé

Appuyer
Appuyer

❑ Appuyer 2 fois rapidement pour allumer.

❑ Appuyer 1 fois pour une lumière estompée.
❑ Appuyer une fois, quand la lumière est allumée
(estompée ou allumée), pour éteindre.

88 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Exemple d’un
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

Gradateur
Abstraction

❑ Interrupteur intelligent (gradateur) :

Appuyer Appuyer
éteint estompé allumé

Appuyer
Appuyer

❑ Appuyer 2 fois rapidement pour allumer.

❑ Appuyer 1 fois pour une lumière estompée.
❑ Appuyer une fois, quand la lumière est allumée
(estompée ou allumée), pour éteindre.
❑ Mais le temps n’a pas été spécifié !
89 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Gradateur avec
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

ticks
Abstraction

❑Un tick représente ½ seconde.

❑Un appui rapide représente 2 appuis en moins
d’une seconde.

allumé tick
Appuyer

Appuyer
Appuyer
Appuyer
éteint estompé1 estompé2 tick estompé2
tick

tick
Appuyer

90 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Temps discret
Automates communicants
Automates temporisés
Abstraction

❑La taille du modèle croît avec la finesse du

temps, ce qui entraine une perte de lisibilité du
modèle.
❑Mélange entre transitions temporelles et celles
qui modifient l’état de contrôle : modifier la
procédure du gradateur en remplaçant ½ s
séparant 2 appuis successifs par 10 s oblige le
changement de la structure de l’automate.
❑Manque de précision.

91 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Temps continu
Automates communicants
Automates temporisés
Abstraction

❑Le temps est précis puisqu’il est modélisé

par 0.
❑Des horloges mesurent le temps au sein
du système.
Appuyer x1
éteint x:=0 estompé Appuyer allumé

x>1
Appuyer Appuyer

92 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Automates
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

temporisés
Abstraction

❑Proposés par Alur et Dill en 1994.

❑Il se compose de deux éléments :
❑Un automate fini décrivant les états de
contrôle du système et les transitions,
supposément instantanées, entre les états.
❑Des horloges, associées aux transitions,
spécifient des contraintes quantitatives de
temps.

93 ©Myriam Fourati Cherif

 Modélisation

Description d’un
Exemples de modèles
Concepts généraux
Automates avec variables

automate
Automates communicants
Automates temporisés
Abstraction

temporisé
❑Un automate temporisé est composé de :
❑Un graphe d’états (structure de kripke)
décrivant les états du système avec transitions
instantanées entre les états.
❑Un ensemble fini d’horloges H={h1,h2,…, hn},
associées aux transitions, utilisées pour
spécifier des contraintes quantitatives de
temps. Elles sont des variables à valeurs
réelles positives et à l’état initial du système
elles ont toutes la valeur 0.
94 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Transitions d’un
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

AT
Abstraction

❑Une transition d’un automate temporisée

est un triplet d’actions :
❑Contrainte d’horloge (appelée aussi garde ou
condition de franchissement) : portée sur les
valeurs des horloges et spécifie une contrainte
pour le franchissement de la transition.
❑ Action : une action de l’automate fini.
❑Des actions de remise à zéros de certaines
horloges.

95 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Définition d’un
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

AT
Abstraction

❑ Un automate temporisé AT =<Q,E,q0,H,T> est défini par ;

❑ Q un ensemble fini d’états de contrôle,
❑ E ensemble d’étiquettes d’actions,
❑ q0 l’état initial de l’automate,
❑ H un ensemble d’horloges
❑ T Q  C(H)  E  2H  Q
❑ Avec C(H) est une contrainte d’horloge présentée sous
formule d’une formule  ;
❑  ::= c ≤ h | c<h | ch | c>h | 1 ∧ 2 : h ∈ H, c ∈ Q (nombres
rationnels).
❑ Et 2H est un ensemble d’horloges remises à zéro.

96 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Exemple d’un
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

AT
Abstraction

❑ système déclenchant une alarme lorsque le

délai séparant 2 réceptions de messages (?msg)
est inférieur à 5 secondes.

97 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Exemple d’un
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

AT
Abstraction

❑ système déclenchant une alarme lorsque le

délai séparant 2 réceptions de messages (?msg)
est inférieur à 5 secondes.
h5,?msg,h:=0

init -,?msg,h:=0 verif h<5,?msg,- alarme

98 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Exemple d’un
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

AT
Abstraction

❑ Une seule horloge h, elle est mise à zéro à l’état initial.

❑ La valeur de h augmente avec le temps.
❑ Dès qu’un message est reçu, on passe à l’état verif et h
est remise à zéro.
❑ A la prochaine réception de message :
❑ Si h <5, l’alarme est déclenchée (état alarme)
❑ Si h5, on peut recevoir un message et on doit initialiser h.
Remise à Contrainte action
h5,?msg,h:=0
zéro de h d’horloge

init -,?msg,h:=0 verif h<5,?msg,- alarme

99 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Remarque
Automates communicants
Automates temporisés
Abstraction

❑Il est possible d’utiliser plusieurs horloges,

notamment pour modéliser des systèmes
communicants.

❑Toutes les horloges doivent progresser à

la même vitesse de manière synchrone.

100 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Configuration
Automates communicants
Automates temporisés
Abstraction

❑La configuration d’un système définit son

état global, elle est donnée par :
❑L’état de contrôle courant, et
❑La valeur de chaque horloge.
❑Elle est notée (q,v) :
❑q : un état de contrôle,
❑v H→+ : une application de valuation
associant à chaque horloge sa valeur
courante.
101 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Configuration
Automates communicants
Automates temporisés
Abstraction

❑Le système change de configuration par :

❑Transition de délais : laisse s’écouler un
certain délais d (toutes les horloges
s’incrémentent de d : v+d). On passe donc de
la configuration (q,v) à (q,v+d).
❑Transition de d’action (discrète) : l’automate
s’active par une transition franchissable.
L’initialisation de l’un ou de plusieurs horloges
est possibles, les valeurs des autres horloges
restent alors inchangées.
102 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Exemple de
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

configurations
Abstraction

❑Evolution de l’automate de l’exemple précédent

en partant de la configuration (init,0) :
?msg ?msg
(init,0)→(init,10.2) → (verif,0) →(verif,5.8) → (verif,0)
→(verif,3.1)?msg
→ (alarme,3.1),…
h5,?msg,h:=0

init -,?msg,h:=0 verif H<5,?msg,- alarme

❑Cette séquence de configurations est appelée

exécution.
103 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Exécution
Automates communicants
Automates temporisés
Abstraction

❑Une exécution de l’AT est une séquence

(infinie) de configurations, chaque
configuration est soit :

❑Une action de l’automate, soit

❑L’écoulement d’un délai.

104 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Trajectoire
Automates communicants
Automates temporisés
Abstraction

❑Une trajectoire est une exécution vue

globalement.
❑C’est une application  de + vers
l’ensemble des configurations (q,v).
❑L’état initial est noté (0) et (t) est la
configuration à l’instant t le long de cette
configuration.
❑Exemple : (12.3)=(verif,2.1)
105 ©Myriam Fourati Cherif
 Trajectoire :
exemple
❑(12.3)=(verif,2.1)
+10,2 +2,1
H=0 H=10,2 H=12,3
?msg ?msg
(init,0)→(init,10.2) → (verif,0) →(verif,5.8) →
(verif,0) →(verif,3.1)?msg
→ (alarme,3.1),…

106 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Réseaux d’AT et
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

synchronisation
Abstraction

❑ Composer des automates temporisés et les synchroniser

: réseau temporisé.
❑ Une exécution du réseau est une séquence de
configurations.
❑ Une configuration comporte l’état de contrôle de chaque
automate du réseau et la valeur de chacune des
horloges.
❑ Un changement de configuration :
❑ Écoulement d’un délai d, toutes les horloges s’incrémentent de d.
❑ Exécution d’une action franchissable

107 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Synchronisation
Automates communicants
Automates temporisés
Abstraction

❑Si 3 automates communiquent, le réseau

passe de la configuration (q0, q1, q2 ,v) à
(q’0, q’1, q’2 ,v’) en exécutant les actions
synchronisées a0, a1, a2, alors v’ ne diffère
de v que par les horloges remise à zéro
par ces transitions.

108 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux

Exemple :
Automates avec variables
Automates communicants
Automates temporisés

passage à niveau
Abstraction

❑Un train

❑Une barrière

109 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Passage à
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

niveau
Abstraction

❑ Deux capteurs : Approche

loin avant sur loin
et Départ signalant à la
barrière l’approche du
train et son éloignement.
❑ Le train peut être :
❑ loin : hors de la
considération de la
barrière.
❑ avant : entre le capteur
d’approche et le début de
Approche Départ la zone protégée par la
barrière.
❑ sur : sur la zone protégée.
110 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Passage à
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

niveau
Abstraction

❑Système faisant coopérer 2

composants :
❑Le train
❑La barrière

❑Système = train || barrière

111 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Modèle du train
Automates communicants
Automates temporisés
Abstraction

❑ Le train passe de l’état

loin à l’état avant en
émettant un signal Approche
Approche. loin Ht:=0 avant
❑ Le train met entre 2 et
5 mn pour parcourir la
portion avant (arrive 2<Ht<5
1<Ht<2
Ht:=0
au passage à niveau). Départ
sur
❑ Le train met entre 1 à
2 mn pour parcourir la
portion sur (quitter la
zone protégée).
112 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles

Modèle de la
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

barrière
Abstraction

❑ Lorsque la barrière Départ Approche

reçoit le signal
Approche
Approche (le train Hb:=0
levée se_baisse
arrive), elle doit se
mettre à baisser. Approche
❑ Lorsqu’elle reçoit le 1<Hb<2
Hb:=0
1<Hb<2
signal Départ (train Départ
s’éloigne), elle doit se Hb:=0

mettre à se lever.
❑ Elle met entre 1 à 2 se_lève
Départ
baissé

mn pour se lever et se Hb:=0

baisser. Départ
Approche
113 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Synchronisation
Automates communicants
Automates temporisés
Abstraction

❑La synchronisation se fait sur les variables

partagées : Approche et Départ.
❑Par exemple, lorsque le train passe de
l’état loin à l’état avant par la transition
Approche, la barrière doit franchir une
transition étiquetée par Approche pour
assurer la synchronisation.

114 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Synthèse
Automates communicants
Automates temporisés
Abstraction

❑Cette modélisation peut aboutir à des

blocages sur les actions franchissables.
❑Exemple : si le train reste plus de 5 mn
dans l’état avant, il y reste indéfiniment car
l’action menant à l’état sur n’est plus
déclanchable (propriété de vivacité non
respectée).
❑Une solution serait l’introduction
d’invariants dans les états.
115 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles
Concepts généraux

Invariants pour le
Automates avec variables
Automates communicants
Automates temporisés

passage à niveau
Abstraction

Départ Approche
Approche
Approche se_baisse
Hb:=0
Ht:=0 levée Hb<2
loin avant
Ht<5 Approche
1<Hb<2 Hb:=0 1<Hb<2
2<Ht<5 Départ
1<Ht<2
Ht:=0 Hb:=0
Départ Sur
Ht<2 se_lève
Hb<2 baissé
Départ
Hb:=0
Départ Approche
116 ©Myriam Fourati Cherif
 Modélisation
Exemples de modèles
Concepts généraux
Automates avec variables

Invariants
Automates communicants
Automates temporisés
Abstraction

❑Les invariants ajoutés dans les états obligent les

transitions d’écoulement du temps de les
respecter.
❑A la fin du délai, le système doit obligatoirement
franchir une transition discrète.
❑Si aucune configuration autorisée n’est
atteignable, il y a blocage : divergence (livelock).

117 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Passage à
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

niveau amélioré
Abstraction

❑Système faisant coopérer 3

composants :
❑Le train
❑La barrière
❑Le contrôleur

❑Système = train || barrière || contrôleur

118 ©Myriam Fourati Cherif

 Modélisation
Exemples de modèles

Méthodes
Concepts généraux
Automates avec variables
Automates communicants
Automates temporisés

d’abstraction
Abstraction

❑ Techniques utilisées pour simplifier les automates.

❑ Basées sur le fait d’ignorer certains aspects de
l’automate.
❑ Un modèle pour un système à vérifier peut ne pas être
adéquat pour une technique automatique de model
checking (ex. taille de l’automate).
❑ Pour répondre à la question Q1 : A , il faudrait alors
abstraire A en A’ et répondre à la question Q2 : A’ .
❑ Il faut bien sûr s’assurer qu’une bonne réponse pour Q1
soit aussi bonne pour Q2.

119 ©Myriam Fourati Cherif