close

Se connecter

Se connecter avec OpenID

Chapitre 2 - Site Web à vocation éducationnel de l`UQO

IntégréTéléchargement
Chapitre 2
Machines à états
w3.uqo.ca/luigi
Remerciements au prof. Hasan Ural
pour plusieurs exemples
1
Exemple:
un automate qui modèle le comportement d’un ordinateur
Au début il est en état éteint
L’événement allumer le met en état allumé
L’événement CtrAltDel le met en état login
L’événement login le fait passer à un des deux états:
 Login accepté
 Login refusé
 S’il accepte, l’événement clique sur icône Word le fait passer en état: prêt pour
WordProcessing
 Noter:
 Ce qui précède est une abstraction. Certaines choses ne sont pas dites: p.ex.
quel sera le résultat si








CtrAltDel ne sont pas frappés simultanément
On frappe CtrAltDel avant d’allumer
On fait des erreurs de frappe pendant le login
Etc.
INF6001 Chap 2
2
Concept d’état
 Le concept d’état du système est une abstraction utile


Dans la réalité il n’y a pas d’états …
Donc normalement, on peut choisir les états de manières différentes
 Représente une instantanée (snapshot) du contenu de la machine à
un moment donné


Déterminé par ce qui s’est produit dans la machine avant
Détermine ce qui peut se produire dans le futur
 État:
 local: état d’une entité dans le système
 global: état de tout le système dans son entièreté,
 incluant donc toutes les entités
 Transitions d’état: événements qui causent changements d’états
INF6001 Chap 2
3
Machines à états
 Comportements possibles de cette
machine:
?2
état 1

état 2
?5
!1
!4

état 3
état 4
?3
?2
état 5
INF6001 Chap 2
Elle peut:
 Envoyer un message 1,
 Puis recevoir un message 3
 Puis envoyer un 4
 Recevoir un 5, etc.
Ou
 Recevoir un message 2
 Puis recevoir un message 5
 Puis envoyer un message 4 et
retourner à pouvoir recevoir 5,
etc.
 L’état 1 est un état ‘initial’
 L’état 5 est un état ‘final’
4
Tableaux de transition d’états
?2
état 1
état 2
!4
?5
!1
1
2
3
4
état 3
!1
3
?2 ?3 !4
2
?5
4
4
5
2
état 4
?3
?2
état 5
INF6001 Chap 2
Machine partiellement spécifiée:
Les transitions impossibles ne sont pas
spécifiées.
Nous pouvons interpréter ces transitions
comme transitions à un état erreur
5
Différents modèles à états
 Les machines à états, aussi appelés automates, sont
un concept très utilisé en informatique
 Un bon nombre de défs différentes existe, chacun avec
sa propre théorie avec des différences
 Tous les modèles suivants sont utilisés dans la
conception des protocoles, ainsi que dans la
conception de circuits, de logiciels, etc.
INF6001 Chap 2
6
Systèmes de transition
 Le concept le plus général
 Nous avons un ensemble d’états (pas nécess. fini) et
une relation de successeur entre états
 Exemple de s.d.t.:
état 1
état 3
INF6001 Chap 2
état 2
état 4
7
Systèmes de transition étiquetés (LTS, labeled transition systems)
semblables aux Machines de Moore
 Les transitions sont nommées
a
état 1
état 2
c
b
état 3
d
état 4
e
INF6001 Chap 2
8
Machines de Moore
 Dans leur définition exacte, dans les machines de
Moore



les entrées sont représentées dans les transitions
et les sorties dans les états
peu de différence car dans les systèmes étiquetés, on peu
penser que chaque état donne son propre nom comme sortie
INF6001 Chap 2
9
Utilisation des étiquettes
 Nous pouvons donner une signification aux étiquettes, p.ex.


?x Veut dire une entrée (input) d’une valeur x
!y Veut dire une sortie (output) d’une valeur y
 x, y: variables ou constantes
?2
état 1
état 2
!4
?5
!1
état 3
INF6001 Chap 2
état 4
?3
10
Notation
 + et – sont aussi utilisés pour indiquer la réception ou
l’envoi d’un message, respectivement
 ? et ! sont plus utilisés récemment
INF6001 Chap 2
11
Machines de Mealy
 Chaque arête est étiquetée par une paire
Entrée/Sortie
Voulant dire que quand à l’état donné l’entrée donnée est reçue,
il y a la sortie donnée et la transition d’état a aussi lieu
2/a
état 1
état 2
4/b
5/c
1/b
état 3
Quand l’entité spécifiée reçoit
un 2 en état 1, elle fait sortir
un a et le système effectue
une transition à l’état 2
Si au lieu un 1 est reçu …
état 4
3/d
INF6001 Chap 2
12
Exemple déjà vu de système téléphonique
OffHook
DialTone
CallAlert
Ringtone
Idle
OnHookTime
Dialing
elapsed
Ringing
DialDIgits
Clicks
Ringback
OffHook
StopRing
Path
Active
INF6001 Chap 2
Notez la description partielle:
qu’arrive si le no n’est pas correct? Etc.
13
Le service TCP décrit comme machine de Mealy
http://www.ssfnet.org/Exchange/tcp/tcpTutorialNotes.html
Quelques
transmissions n’ont
pas de sortie
INF6001 Chap 2
14
Modèle architectural
SYN
Usager
client
SYN+ACK
ActiveOpen
Close
Client
ACK
Serveur
FIN
INF6001 Chap 2
15
Ceci est une application du concept de:
 Établissement en trois étapes: Three-way handshake




Client: Je suis prêt à envoyer (SYN)
Serveur: D’accord (SYN+ACK)
Client: Allons-y donc (ACK)
Le client et le serveur peuvent alors commencer à transférer des données
Client
Serveur
Invitation
Serveur
Client
Closed
SYN
SYN+ACK
Acceptation
Confirmation
INF6001 Chap 2
ACK
16
Le diagramme de transition TCP
Ex:
(CLOSED)ActiveOpen/SYN(SYN_SENT)SYN/SYN+ACK(SYN_RCVD)ACK(ESTABLISHED)







The ESTABLISHED state is where data transfer
can occur between the two ends in both
directions. Data transfer is not shown.
The two transitions leading to the
ESTABLISHED state correspond to the opening
of a connection, and the two transitions leading
from the ESTABLISHED state are for the
termination of a connection.
The client does an Active open which causes
its end of the connection to send a SYN
segment to the server and to move to the
SYN_SENT state.
If a connection is in the LISTEN state and a
SYN segment arrives, the connection makes a
transition to the SYN_RCVD state and the
server takes the action of replying with an
SYN+ACK segment.
The arrival of the SYN+ACK segment causes
the client to move to the ESTABLISHED state
and to send an ACK back to the server.
When this ACK arrives the server finally moves
to the ESTABLISHED state.
For more explanations:


SYN
http://www.ssfnet.org/Exchange/tcp/tcpTutorialNotes.html
Ce diagramme est une simplification


Il n’y a pas de diagramme de transition d’état vraiment
fidèle pour TCP
Notez qu’il n’est pas clair si ce diagramme représente
les états du client, du serveur, ou de la connexion
INF6001 Chap 2
Usager
client
SYN+ACK
ActiveOpen
Close
Client
ACK
Serveur
FIN
17
Voici un beau diagramme sur la connexion TCP
http://www.tcpipguide.com/free/t_TCPConnectionEstablishmentProcessTheThreeWayHandsh-3.htm
INF6001 Chap 2
18
Difficultés du modèle de transitions d’états
 Cet exemple montre que pour pouvoir exprimer
clairement des protocoles dans des modèles de
transitions d’états concis, on fait des simplifications

Dans ce diagramme, les états sont parfois états de la
connexion, parfois états d’une entité!
 Les modèles de transition résultants ne sont pas exacts
et ne sont donc pas appropriés pour l’analyse discutée
dans ce cours…
 Des modèles plus complexes, plus exacts, peuvent être
requis pour l’analyse formelle
INF6001 Chap 2
19
Une présentation différente (wikipédia)
INF6001 Chap 2
20
Revenons au Service de transport OSI
avec sa représentation comme système de transition étiqueté
INF6001 Chap 2
21
B
A
B
A
T-ConReq
T-ConReq
T-ConInd
T-ConResp
T-ConConf
T-DiscInd
Connexion avec Succès AB
T-ConReq
T-ConInd
T-DiscReq
A
Connexion refusée par B
B
A
B
T-DatReq
T-DatInd
T-DiscInd
Tentative de
connexion de A
refusée
par le fourniss. de service
A
A
B
T-DiscReq
T-DiscReq
T-DiscInd
T-DiscInd
INF6001 Chap 2
B
T-DiscReq
Les deux décident
de déconnecter
(collision)
A décide de
déconnecter
A
Transfert Données
AB
B
T-DiscInd
Service de la couche transport,
Cas d’usage
22
Le service de transport OSI décrit comme
système de transition étiquété (un seul T-SAP)
Simplifié!
T-DiscReq
T-DiscInd
T-ConReq
Outgoing
Connection
Pending
T-ConInd
T-DiscReq
T-DiscInd
T-ConConf
T-ConResp
Ce diagramme ne
décrit que des séquences
possibles d’événements
(n’incluant pas des E/S)
INF6001 Chap 2
T-DiscReq
T-DiscInd
Idle
Data
Transfer
Ready
Incoming
Connection
Pending
T-DatReq, T-DatInd
23
Scénarios possibles: deux T-SAP
A
B
(Notes de cours du Prof. Bochmann)
INF6001 Chap 2
24
Le protocole Transport OSI
décrit comme machine de Mealy
Très simplifié!
INF6001 Chap 2
(Notes de cours du Prof. Bochmann)
25
La place de chaque machines à état
 La machine à états pour le service décrit les séquences
qu’on voit au SAP
 La machine à état pour le protocole décrit ce qu’on voit
dans le protocole
SAP N
Protocole Couche N
Échange d’unités
protocole PDU
Couche N
décomposée
Interface
entre couche N et couche N-1
SAP N-1
INF6001 Chap 2
Échange d’unités
service SDU
26
Il y a les deux pour chaque côté
Dans chaque côté, les transitions des deux machines sont simultanées
SDUs
SDUs
Côté B
Service
Côté A
Service
T-DiscReq
T-DiscInd
T-DiscReq
T-DiscInd
T-DiscReq
T-DiscInd
Idle
T-ConReq
T-ConReq
Outgoing
Connection
Pending
T-ConInd
T-DiscReq
T-DiscInd
T-ConConf
T-ConResp
Data
Transfer
Ready
Outgoing
Connection
Pending
Incoming
Connection
Pending
T-DiscReq
T-DiscInd
Idle
T-ConInd
T-DiscReq
T-DiscInd
T-ConConf
T-ConResp
Data
Transfer
Ready
Incoming
Connection
Pending
T-DatReq, T-DatInd
T-DatReq, T-DatInd
Côté B
Protocole
Côté A
Protocole
PDUs
INF6001 Chap 2
27
États et transitions (H. Ben Yedder, 2010)
INF6001 Chap 2
Montre en même temps le fonctionnement
du service et du protocole
28
Comparaison avec le Service TCP (Machine Mealy)
INF6001 Chap 2
29
Comparaison OSI-TCP
 Il est intéressant de faire une comparaison de la description de service transport de OSI et
TCP

Laissée à vous comme exercice
 La description OSI-TS est abstraite, laisse le travail au protocole

Dans TCP, il n’y a pas de distinction entre PDUs et SDUs
 TCP décrit déjà le protocole quand il décrit le service



P.ex. notez comment la spec service TCP utilise les messages d’ACK.
Dans l’ OSI, l’acquittement est une fonction de protocole
Pour OSI, 2-way handshake est suffisant car il suppose que les couches sous-jacentes sont fiables,
TCP demande 3-way.
 OSI-TS décrit la communication entre deux pairs

Peuvent être clients-serveurs, n’importe
 Dans TCP les deux entités ne sont pas égales
 Mélange de la notion d’état de la connexion et d’état du client-serveur


P.ex. l’état ‘Established’ est un état global, des deux côtés qui savent que maintenant ils peuvent
recevoir/envoyer
Tandis que l’état ‘SYN_SENT’ est propre du client!
 Pour utiliser les notions discutées dans ce cours dans l’analyse de TCP il est
nécessaire de décomposer cette machine en :


Machine du client
Machine du serveur
INF6001 Chap 2
30
La différence ….
 Les différences de style entre les spécs de OSI et TCPIP sont probablement dues au fait que:


La description de l’OSI est plus précise, pour pouvoir être
implémentée de différentes manières, qui doivent être toutes
conformes avec la spéc abstraite
La description du TCP-IP est plus sommaire, étant la
description d’un programme qui existe déjà
INF6001 Chap 2
31
Le passage du temps dans les machines
 En principe, les transitions sont instantanées
 Le temps passe quand le système est dans un état
 Cependant il y a plusieurs variations à ce concept

Différents types de machines temporisées
INF6001 Chap 2
32
Machines communicantes
 Une machine à états peut définir un système entier ou
une partie de système
 Si elle définit une partie d’un système, elle sera
composée avec autres machines
 Plusieurs méthodes de communications ont été
utilisées
 Nous en discuterons ici deux:


Synchrones
Asynchrones
INF6001 Chap 2
33
A
B
Communication asynchrone
Service Provider
 Dans la communication asynchrone, les machines communiquent par un
‘milieu’ souvent représenté par des canaux pouvant contenir des
primitives de communication (PDUs ou SDUs)
 Normalement modélisés par des files FIFO infinies et sans pertes de
données
 Ces canaux sont une abstraction pour le fournisseur de service sousjacent
 Une machine peut donc mettre des données dans une file et continuer son
travail, peut être mettant d’autres données dans la même file plus tard
 L’autre machine prendra des données de la file quand elle le voudra.
C12
…
Machine B
Machine A
…
C21
INF6001 Chap 2
34
Modèles de machines à états finis
communicantes asynchrones
(appelés aussi CSM ou CFSM, Communicating Finite-state Machines)
 Machines communicantes à moyen de files d’attentes
Files FIFO et
sans pertes
10
?3
!4
!1
20
!3
C12
…
?4
11
21
…
?2
?1
!2
C21
22
12
P.Ex un client et serveur.
INF6001 Chap 2
1 requête d’accès
2 permission d’accès
3 refus d’accès
4 terminaison d’accès
35
Exécution du système
 L’état global initial est


l’ensemble de tous les états
initiaux des composants
et l’ensemble de tous les
contenus de files initiales

Dans ce cas <10,20>,<ε, ε>

INF6001 Chap 2
Files FIFO et
sans pertes
10
ε file vide…
 Dans cet état, le seul événement
qui peut se produire est l’envoi
d’un 1 par le client
 Il est mis dans la file, puis la seule
chose qui peut se produire est la
réception de 1 de la part du
serveur
serveur
client
?3
!4
!1
20
!3
C 12
…
?4
11
21
…
?2
12
?1
!2
C 21
22
36
Construction de la machine globale du système
 Chaque état global du système spécifie:


L’état de chacune des deux machines communicantes
Le contenu des deux files
 Par exemple, au début les deux machines sont dans leur état initial
 Le seul premier événement possible est que le client met 1 dans la file et passe à l’état
suivant, tandis que la deuxième machine reste sur son état
 Le serveur peut puis recevoir
 Après ça, le client peut envoyer


un 3, ce qui change l’état global à <11,20>, avec un 3 dans la file de sortie du client
ou un 2, ce qui change l’état global à <11,22>, avec un 2 dans la file de sortie du client
 Etc.
Files FIFO et
sans pertes
10
?3
!4
!1
20
!3
C12
…
?4
11
21
…
?2
12
INF6001 Chap 2
?1
!2
C21
22
37
État initial
Files FIFO et
sans pertes
10
?3
!4
!1
20
!3
C12
…
?4
11
21
…
?2
?1
!2
C21
22
12
<10,20>,<ε, ε>
La trace est vide
Quelles sont les prochaines transitions?
INF6001 Chap 2
38
Prochain état
Files FIFO et
sans pertes
10
?3
!4
!1
C12
…
20
!3
1
?4
11
21
…
?2
?1
!2
C21
12
22
L’état courant est: <11,20>,<1, ε>
La trace courante est: <!1>
Transitions possibles?
INF6001 Chap 2
39
Prochain état
Files FIFO et
sans pertes
10
?3
!4
!1
20
!3
C12
…
?4
11
21
…
?2
?1
!2
C21
12
22
L’état courant est: <11,21>,< ε, ε>
La trace courante est: <!1, ?1>
Transitions possibles?
INF6001 Chap 2
40
Prochain état, après avoir choisi !3
Files FIFO et
sans pertes
10
?3
!4
!1
20
!3
C12
…
?4
11
?2
21
…
3
?1
!2
C21
12
22
L’état courant est: <11,20>,< ε, 3>
La trace courante est: <!1, ?1, !3>
La seule transition possible nous ramène à un état déjà vu.
INF6001 Chap 2
41
Retrouver un état précédent
Après la trace: !1, ?1, !3, ?3 nous nous retrouvons à l’état global suivant:
Files FIFO et
sans pertes
10
?3
!4
!1
20
!3
C12
…
?4
11
21
…
?2
12
?1
!2
C21
22
Nous avons déjà vu cet état, il est l’état initial
<10,20>,<ε, ε>
INF6001 Chap 2
42
La machine globale du système
(composition asynchrone)
ε : canal vide
<10,20>,<ε, ε>
!1
<11,20>,<1, ε>
?1
?3
<11,21>,< ε, ε>
?4
!2
?4
!3
<11,22>,< ε, 2>
?2
<11,20>,< ε, 3>
<12,22>,< ε, ε >
Files FIFO et
sans pertes
10
?3
!4
!1
!4
20
!3
C12
…
?1
!1
21
11
…
?2
12
INF6001 Chap 2
<10,22>,< 4, ε >
?4
<11,22>,<[4,1], ε >
!2
C21
22
[4,1] :canal contenant 4 puis 1
43
Retour à un état
 Pourquoi sommes-nous retournés à un état précédent
après certaines transitions?
 Car nous avons détecté que le nouveau état était
identique à un état déjà trouvé avant
 Les deux machines sont dans les mêmes états et le
contenu des canaux est le même
 Deux états identiques permettent les mêmes traces
futures

Il y a aussi le concept d’états équivalents que nous verrons
plus tard
INF6001 Chap 2
44
Machines globales finies et infinies
 Contrôlez que C12 n’aura jamais plus de 2 messages
et C21 jamais plus d’1
 Nous avons ici une machine globale qui est finie



La machine globale d’un système n’est pas nécessairement
finie
Nous pouvons avoir un nombre infini d’états si les files
peuvent grandir à longueurs arbitrairement grandes
Le fait qu’une file puisse être infinie est une caractéristique à
prendre en considération (nous verrons…)
INF6001 Chap 2
45
Machines infinies
 Un canal peut grandir ‘à jamais’



Dans ce cas, il y aura (au moins) un chemin dans l’arbre
d’accessibilité dans lequel la machine pourra avoir un
nombre toujours grandissant d’états.
Dans ce chemin, la machine globale ne retournera jamais à
un état déjà vu
Donc, machine globale infinie.
La machine de
droite n’est pas
obligée à prendre
tout de suite
INF6001 Chap 2
!a
canaux
?a
46
Analyse d’accessibilité
 Le processus d’obtenir la machine globale à partir des
machines locales s’appelle

Analyse d’accessibilité, reachability analysis
 Le graphe obtenu faisant l’analyse d’accessibilité
s’appelle

Graphe d’accessibilité
INF6001 Chap 2
47
Critique du modèle de communication
asynchrone
 Le modèle de communication asynchrone représente bien la
façon de penser des ingénieurs de protocoles

Envoyer et continuer
 Plusieurs langages et outils de spec et V&V utilisent ce modèle

Notamment SDL
 Cependant il peut fausser la réalité:


Il force à mettre des files partout, même quand la communication devrait
être directe
Les files FIFO infinies et parfaites n’existent pas en réalité:
 Les médias de communication peuvent perdre des données et
peuvent permettre aux données de se chevaucher


Surtout dans le cas de transmission sans connections
Ils ne sont pas infinis, même si leur capacité peut être très grande
INF6001 Chap 2
48
Représentation de canaux avec pertes (lossy)
 Deux manières:

Représenter la perte ou autres dans une des deux machines
communicantes, p.ex. dans le récepteur:
?perte
Dans ce cas le message
est ignoré
?réception

Ou sinon définir les canaux comme troisième processus, voir
modèle synchrone
INF6001 Chap 2
49
Modèle de communication synchrone
 Dans le modèle synchrone, nous n’avons pas de canaux prédéfinis
 Les entités communiques directement par un mécanisme de
communication partagé
 La communication entre deux entités est un fait qui implique les deux
simultanément
 Une entrée et une sortie deviennent une seule action
Machine A
INF6001 Chap 2
Mécani
sme de
commu
nication
Machine B
50
Machine globale pour le cas synchrone
(aussi appelée composition synchrone)
10
20
?3
!4
!1
!3
?4
11
21
?2
12
?1
!2
10,20
22
3
4
La combinaison de
!1 et ?1 donne une
seule action 1
INF6001 Chap 2
1
11,21
2
12,22
51
Critique du modèle synchrone
 L’envoyeur et le récepteur sont bloqués ensemble
pendant l’exécution d’une opération en commun
 Parfois pas apprécié par les ingénieurs de télécom
car ils sont plutôt habitués à penser en termes de
envoyer-continuer
 Utilisé dans les algèbres de processus: CCS, CSP, LOTOS
INF6001 Chap 2
52
Rélation entre les deux modèles
 Le modèle synchrone peut simuler le modèle
asynchrone par l’utilisation d’entités ‘canaux’
intermédiaires
A
B
canaux
 Le modèle asynchrone avec files de longueur 0
correspond au modèle synchrone
INF6001 Chap 2
53
Conditions d’erreur dans les systèmes
synchrones
 Dans les systèmes synchrones, il y a essentiellement une seule possibilité d’erreur, l’impasse
(deadlock), le fait que il n’y a pas façon de sortir d’un état global
 Étant donné que normalement un système réparti est censé être toujours en fonctionnement, une
impasse est considérée un problème
10
20
?3
!6
!1
!3
?4
11
21
?2
12
?1
!2
22
10,20
3
1
11,21
2
INF6001 Chap 2
Impasse, pas
d’état successeur
12,22
54
Conditions d’erreur dans les systèmes
asynchrones
 Dans le cas asynch, il y a plusieurs cas d’erreur




Impasse = deadlock: un état accessible dans lequel tous les
canaux sont vides et aucun processus ne peut envoyer
Réception non spécifiée: il y a un message au début d’un
canal qui ne peut pas être reçu car il n’y a pas de transition
appropriée (spec incomplète)
Réception non-spécifiée bloquante: il y a une réception non
spécifiée et à cause de ça le système se trouve en impasse
Transitions non-exécutables: pas une erreur bloquante, mais
pourrait être un symptome d’un problème de conception
INF6001 Chap 2
55
Un CFSM très malade…
20
10
?d
!a
?b
C12
…
!b
?c
11
?b
!c
21
…
?b
?a
C21
!d
22
12
23
INF6001 Chap 2
?a
56
Arbre d’accessibilité partiel
<10,20>,< ε, ε >
!b
!a
<11,20>,<a, ε>
!c
<12,20>,<ac,ε>
etc.
Réceptions
non specifiées:
a ne peut pas
être reçu, mais il y
a d’autres actions
possibles
<10,21>,< ε,b>
!b
a!
?b
<11,21>,< ε, ε >
<11,21>,<a, b>
etc.
?b
!c
<12,21>,<a, ε >
?a
<12,22>,< ε, ε >
<12,21>,< c, ε >
Impasse,Réception
non spec bloquante: c ne
peut pas être reçu et il n’y a pas
d’autres actions possibles
Impasse
INF6001 Chap 2
Canaux vides,
Aucune action possible
57
Réception non-spécifiée bloquante
Après la trace !b, ?b, !c
?d
!a
?b
C12
…
!c
!b
c
11
?b
<12,21>,< c, ε >
20
10
?c
21
…
?b
?a
C21
!d
22
12
23
INF6001 Chap 2
Machine 2 ne peut pas recevoir le c
Machine 1 ne peut rien envoyer, ni
recevoir
?a
58
Impasse - deadlock
20
10
?d
!a
?b
C12
…
!b
?c
11
?b
!c
21
…
?b
?a
C21
!d
22
12
23
INF6001 Chap 2
<12,22>,< ε, ε >
Les deux machines ne peuvent
rien envoyer
Et il n’y a rien à recevoir dans les
files!
?a
59
Réception non spécifiée non bloquante
20
10
?d
!a
?b
C12
…
11
?b
!c
!b
c a
?c
21
…
?b
?a
C21
!d
22
12
23
INF6001 Chap 2
?a
<12,20>,<ac,ε>
La file C12 contient a au début mais
la machine 2 est dans son état 20 et
ne peut pas le recevoir
Ceci ne bloque pas le système car la
machine 2 peut envoyer un message
et prendre a plus tard
Possibilité d’erreur, cas à étudier
60
Dans une seule feuille…
20
10
?d
!a
?b
C12
…
!b
?c
11
?b
!c
21
…
?b
?a
C21
!d
22
12
23
?a
<10,20>,< ε, ε >
!b
!a
<11,20>,<a, ε>
!c
<12,20>,< ac,ε>
etc.
Réceptions
non specs
<10,21>,< ε,b>
?b
!b
<11,21>,< ε, ε >
<11,21>,<a, b>
etc.
?b
!c
<12,21>,<a, ε >
?a
<12,21>,< c, ε >
Réceptions
non spec
bloquante
<12,22>,< ε, ε >
INF6001 Chap 2
Impasse
61
Exercice (pas un devoir)
 Compléter le graphe d’accessibilité de ce
dernier exemple: la solution devrait
comprendre 34 transitions et 25 états
 Trouverez-vous d’autres erreurs?
 Vous trouverez aussi des transitions nonexécutables et des états non-atteignables
10
?d
 Calculez aussi la composition synchrone:


Allez-vous loin?
Modifiez la machine de gauche comme
montré ici:
 Quelles sont vos réflexion au sujet des deux
modèles, du point de vue d’analyse
d’accessibilité, détection d’erreurs, etc.
INF6001 Chap 2
!a
?b
11
a!
?b
!c
?b
12
62
Sources
 Le protocole client-serveur fut introduit dans:

P. Zafiropulo et al. Towards Analyzing and Synthetizing
Protocols. IEEE Trans. Comm. COM-28(4) 651-661, 1980
 Le protocole que nous venons de voir est présenté
dans:


http://lotos.site.uottawa.ca/ftp/pub/Lotos/Theses/hvds_phd/chapter_2.pdf
Ce chapitre de thèse contient aussi d’autres infos sur
l’analyse d’accessibilité
INF6001 Chap 2
63
Généralisation au cas de plusieurs
machines
 Jusqu’à présent, nous avons discuté le cas de 2 machines communicantes
 Les mêmes idées peuvent être généralisées au cas de 3, 4, … machines
communicantes
 Tant dans le cas de composition synchrone, que asynchrone
 Et effectivement, tout système de protocoles a besoin d’au moins 4
machines pour pouvoir être exprimé complètement:
Usager A
Usager B
Les machines pour les
usagers pourraient être
extrêmement simples:
Prendre des données,
les utiliser, prendre,
utiliser…
Protocole
INF6001 Chap 2
Protocole
64
Processus ‘environnement’
 On postule souvent l’existence d’un processus externe
non défini qui reçoit ou envoie des événements:
l’environnement
INF6001 Chap 2
65
Problèmes fondamentaux dans l’analyse
des protocoles
 Problèmes d’indécidabilité
 Problèmes d’explosion d’états
INF6001 Chap 2
66
Problèmes d’indécidabilité
 Une des conséquences de l’insolvabilité du problème de l’arrêt
de machines de Turing est que

déterminer si un canal est borné ou non est indécidable
 On peut chercher à construire la machine globale, si cette
construction s’achève nous saurons, mais cette construction
pourrait continuer à jamais
 Malheureusement, le problème de décider l’impasse, etc. pour
les protocoles dont les canaux ne sont pas bornés est aussi
indécidable
 Nous pouvons toujours faire l’analyse en faisant l’hypothèse
qu’aucun canal ne contienne jamais plus de n éléments, pour
un n donné
 Cette analyse ne sera pas complètement valable si un canal
peut en fait excéder cette borne
INF6001 Chap 2
67
Entrelacement d’événements et
explosion d’états
 Malheureusement, même dans le cas de canaux bornés, nous aurons toujours
l’explosion d’états, à cause du besoin de considérer toutes les possibilités
d’entrelacement d’événements qui ne sont pas directement reliés
 P. ex. considérer toutes les possibilités d’entrelacement d’exécution de 2 machines
de 2 états chaque peut demander de considérer jusqu’à 5 états globaux.
 Et ce nombre monte de façon exponentielle!
!m
A
X
!n
A,Y
B,X
!n
!m
B
A,X
Y
!m
!n
B,Y
Deux scénarios possibles
INF6001 Chap 2
68
Calcul du nombre d’état globaux
(Cas Synchrone)
 Dans le cas synchrone pour deux machines, les états
globaux sont de la forme <X,Y> où X est l’état d’une
machine et Y est l’état de l’autre
 Donc le nombre max d’états globaux est le produit des
nombre des états des machines communicantes
 Cependant il faudra avoir plus de machines, car il
faudra représenter les canaux en utilisant des
machines additionnelles
A
B
canaux
INF6001 Chap 2
69
Calcul du nombre d’état globaux
(Cas Asynchrone)
 Si nous composons deux machines de M et N états, nous
pourrions avoir pour ce fait un max de MxN états
 Ceci se trouve augmenté par le nombre de configurations
possibles des deux canaux

Pour calculer ce dernier, il faut faire une hypothèse concernant leur
longueur maximale
 Un canal de dimension maximale 1 et avec p messages
possibles peut être ou bien vide ou bien contenir un des
messages

Ceci fait p0+p1 possibilités
 Un canal de dimension maximale 2 et avec p messages
possibles peut être vide, ou peut contenir un message, ou peut
contenir 2 messages

Ceci fait p0+p1+p2 possibilités
INF6001 Chap 2
70
Formule générale de calcul
 Donc pour



deux machines de M et N états,
deux canaux de longueur m et n,
pouvant contenir respectivement p et q messages différents,

le nombre maximal d’états possibles est:
M x N x (p0+p1+...+pm) x (q0+q1+...+qn)
 Ceci implique que la construction de la machine globale en
principe est un problème de complexité exponentielle

Les longueurs des canaux se trouvent à l’exposant
INF6001 Chap 2
71
Exemple
 Dans le cas du protocole client-serveur déjà discuté, nous
avons:




M=N=3
p=2 (les deux messages sont 1 et 4)
q=2 (les deux messages sont 3 et 2)
Supposant qu’on sache que :
 Le canal C12 ne sera jamais plus long de2
 Le canal C21 ne sera jamais plus long de 1
 Le nombre maximum total d’états est:
3 x 3 x (20+21+22) x (20+21) = 9 x 7 x 3 = 189
Dont seulement 8 sont accessibles comme nous avons vu
Rappel dans la planche suivante
INF6001 Chap 2
72
La machine globale du système
(composition asynchrone)
ε : canal vide
<10,20>,<ε, ε>
!1
<11,20>,<1, ε>
?1
?3
<11,21>,< ε, ε>
?4
!2
?4
!3
<11,22>,< ε, 2>
?2
<11,20>,< ε, 3>
<12,22>,< ε, ε >
Files FIFO et
sans pertes
10
?3
!4
!1
!4
20
!3
C12
…
?1
!1
21
11
…
?2
12
INF6001 Chap 2
<10,22>,< 4, ε >
?4
<11,22>,<[4,1], ε >
!2
C21
22
[4,1] :canal contenant 4 puis 1
73
États accessibles
 Les concepts d’état global et état accessible sont importants
 Certains logiciels construisent avant tout l’espace global de tous
les états possibles, faisant l’hypothèse de certaines tailles
maximales de canaux, et puis calculent la relation d’accessibilité
 D’autres logiciels construisent les états accessibles au fur et à
mesure
 ‘À la volée’, ou ‘On the fly’ est une troisième manière de
procéder. L’algorithme ne garde pas en mémoire tout l’arbre,
mais seulement la partie sur laquelle il est en train de travailler.

L’algorithme est beaucoup plus complexe et ne se prête pas à certains
types de analyse
INF6001 Chap 2
74
En pratique
 Malgré la complexité élevée du problème de l’analyse
d’accessibilité, des logiciels optimisés disponibles
aujourd’hui permettent de construire le graphe
d’accessibilité de protocoles réels

Centaines de millions d’états
INF6001 Chap 2
75
Techniques pour réduire l’explosion d’états
 La réduction de l’explosion d’états est un domaine de recherche très
développé
 Quelques techniques sont:
 Chercher à établir des classes d’équivalence entre états (p.ex. états
symétriques)
 Chercher à spécifier les machines à composer avec le plus petit nombre d’états
possible (ignorer les détails moins importants, comme les transitions internes)
 Recherche aléatoire (random search): au lieu de chercher à explorer tous les
états, en explorer un sous-ensemble choisi aléatoirement
 Recherche ciblée: au lieu de chercher à explorer tout le graphe,


explorer seulement les parties dans lesquels nous sommes intéressés
(celles dans lesquels une erreur pourrait se cacher)
Explorer avant tout les transitions les plus probables
Limiter la profondeur de l’arbre d’accessibilité
 Nous pouvons aussi chercher à réduire l’espace demandé par la
représentation d’un état en mémoire
 Un seul bit par état, v. SPIN

INF6001 Chap 2
76
Critique du concept d’état
 Bien que les concepts d’état et transition soient la base de
toutes les recherches sur l’ingénierie de protocoles, il faut savoir
que dans la réalité les états et les transitions n’existent pas!
 P.ex. quand je lis l’écran il est utile de penser que l’écran reste
dans un certain état, puis fait une transition quand je pèse sur
une touche
 En réalité, ce que je vois est le résultat d’un flux continu de
courants
 C’est partiellement à cause de ce fait qu’il y a beaucoup de
variations dans les concepts d’états et transitions utilisés
 Et que la vérification faite sur la base du concept d’état n’est
pas infaillible
 Cependant le concept d’état est très utile pour la conception, et
pour éviter et dévoiler un grand nombre de possibilités d’erreur
INF6001 Chap 2
77
Question
 Dans le modèle asynchrone, pouvons-nous admettre que deux
événements, c’est-à dire deux transitions d’états, soient
simultanés?



Le modèle asynchrone discuté dans ce cours admet qu’une seul
événement, une seule transition d’états se produise à la fois dans le
système.
En informatique, celle-ci est une hypothèse commune. Cette hypothèse
est justifiée par le fait que deux événements exactement simultanés sont
rares ou non-existants en nature (il y en aura normalement un qui se
produit ou commence ‘un peu avant’ l’autre).
On étudie cependant parfois des modèles de parallélisme dits de
‘simultanéité véritable’ (true parallelism), où ceci est possible, mais ceci
n’est pas le sujet de ce cours.
INF6001 Chap 2
78
Pour en savoir plus …
 Vous trouverez beaucoup d’informations faisant une
recherche web sur:



Analyse d’accessibilité – protocoles
Protocol reachability analysis
Model checking
 Cependant ces sources discutent souvent des
techniques qui seront présentées plus tard dans le
cours
INF6001 Chap 2
79
Concepts importants de ce cours
 États et représentation de machines d’états
 Les protocoles comme machines d’états
communicantes
 Compositions synchrone et asynchrone
 Comment les calculer
 Machine globales et comment les obtenir
 Différents types d’erreurs:

Impasses, réceptions non-spécifiées
 Limites pratiques et théoriques pour ces techniques
INF6001 Chap 2
80
L’acquittement et le déni de service
Source: http://en.wikipedia.org/wiki/SYN_flood
Séquence normale
Séquence d’attaque
L’attaquant envoie une longue séquence de SYN et le récepteur naïf
alloue des ressources à chaque connexion potentielle.
Il sera puis incapable de desservir des usagers réguliers.
Cependant cette attaque est bien connue et elle est prévue par les parefeu d’aujourd’hui.
INF6001 Chap 2
81
Auteur
Документ
Catégorie
Без категории
Affichages
7
Taille du fichier
1 712 Кб
Étiquettes
1/--Pages
signaler