11_Verificare_protocoale

Universitatea Politehnica Bucureti - Facultatea de Automatic i Calculatoare

Protocoale de comunicaie Curs 10 1

Verificarea protocoalelor



Verificarea protocoalelor

Modele de specificare a protocoalelor: Tranziionale: execuia unor aciuni la producerea unor evenimente.

Algoritmice: limbaje de nivel nalt.

Hibride.

Tehnici formale tranziionale pentru specificarea si validarea protocoalelor: Model automat cu stri finite:

Fiecare entitate de protocol se afl ntr-o stare specific;

Starea e determinat de valorile tuturor variabilelor;

O tranziie trece entitatea dintr-o stare n alta;

Exist o stare iniial.

Model reele Petri: Digraf (graf dirijat bipartit) cu 2 tipuri de noduri, locuri i tranziii;

Starea este dat de marcajul locurilor.

Explozie a strilor pentru protocoale complexe.



LOTOS

Language Of Temporal Ordering Specification: Standard ISO [IS8807].

O parte de control (Algebre de proces - CCS, CSP).

O parte de date (ACT ONE).

Manier ierarhic de modelare a sistemului: Subsistemele ruleaz n paralel i comunic prin mesaje.

Expresii de comportament fr constrngeri temporale.

Verificarea proprietilor: Axiomatic (Proof-theoretic).

Bazat pe stri (Model-checking).

De testare.

Setul de utilitare CADP: Dezvoltat la INRIA Rhones-Alpes, Grenoble, Frana.

Portabilitate platforme SUN, LINUX si Windows.

Disponibil la http://www.inria.fr/vasy/CADP.html.

Principalele instrumente sunt: CAESAR, CAESAR.ADT (compilatoare), ALDEBARAN (verificare). TERMINATOR, EXHIBITOR, XSIMULATOR, EVALUATOR "on the fly".



LOTOS

Exemple de grafuri:



Modelul automatului finit

FSM: Finite State Machine (exemplu pentru protocolul 3). Stri:

Transmitator: (0, 1): corespunde cadrului trimis; Receptor: (0, 1): corespunde cadrului ateptat; Canal: (0, 1, A, -): corespunde coninutului canalului.

Stare iniial: (0,0,0)



Proprieti

Exist o secven de operare normal:

Se poate determina vizual.

Nu se livreaz niciodat 2 pachete impare fr un pachet par intermediar (i invers):

Echivalent: nu exist 2 tranziii 1 fr o tranziie 3 ntre ele (i reciproc).

S nu existe schimbri de stare la emitor (0->1->0) fr schimbri corespunztoare la receptor:

Protocolul ar pierde nedetectat 2 pachete.

S nu existe interblocri (deadlock).



Modelul diagramelor de tranziii

stabilire

transfer

terminare

staia 1 -> staia 2 staia 2 -> staia1

enq

invalid

nak

ack

eot

mesaj

invalid

nak

ack



Modelul transmitorului / receptorului

bcc

bcc

etb

1

2 3 6 7

4 5 8 9

stx

soh

stx etb

etx

Aciuni: a - iniializare tampon mesaj;

b - iniializare tampon text i variabile text;

c - start text transparent;

d - primul caracter; pune contor pe valoarea 1;

e - alte caractere de text; increment contor;

f - sfrit antet, memoreaz i interpreteaz nceput text;

g - verificare erori;

k - sfrit bloc/text; ateapt caracter verificare.



Tabel aciuni

9

9 g 8

7

7 g 6

8 k 6 k 5 5 e 5

4 5 d 4

6 k 3 3 e 4 f 3

2 3 d 2

10 c 4 b 2 a 1

bcc itb etx etb syn dle stx soh stare\intrare

stare urmtoare / aciune



Reele Petri



Reele Petri

Propuse n forma iniial de Carl Adam Petri n 1962;

Au evoluat spre mai multe variante:

Reele Petri elementare;

Reele Petri generalizate;

Reele Petri cu arce inhibitoare;

Reele Petri colorate;

Reele Petri continue;

Reele Petri cu predicate;

Reele Petri cu capaciti;

Reele Petri cu prioriti.

Unele variante sunt echivalente ntre ele, altele nu.

Se folosesc pentru analiza (automat) a proprietilor sistemelor concurente, bazate pe evenimente:

Caz particular: verificarea protocoalelor.



Definiii (1)

O reea Petri RP este un cvadruplu RP = (L, T, I, O), unde:

L, mulime finit de locuri (locaii), reprezentare cercuri; T, mulime finit de tranziii, L T = , reprezentare bare; I, funcie de inciden nainte I : L x T {0, 1}, reprezentare arce; O, funcie de inciden napoi O: T x L {0, 1}, reprezentare arce.

Marcajul M al unei RP asociaz fiecrui loc un numr natural: functie M : L N:

M(l) este marcajul locului l, reprezentat prin puncte n cerc.

Pentru fiecare tranziie t din T se definesc 2 mulimi de locuri:

Mulimea locurilor de intrare: Pre(t) = {l L | I(l, t)0}; Mulimea locurilor de ieire: Post(t) = {l L | O(t, l)0}.

Reprezentare: * *

t1

t2

t3

t4

l1

l2

l3

l4

l5



Definiii (2)

Tranziia t este executabil pentru marcajul M dac:

M(l) >= I(l,t), l L (fiecare loc de intrare are cel puin un punct).

Execuia tranziiei t pentru M schimb marcajul n M':

M'(l) = M(l) - I (l,t) + O (t,l), l L.

Pentru execuia unei tranziii se folosete notaia:

M -t-> M'

O secven posibil de execuii din M n M', notat M =$=> M', este $ = t

1, t

2, t

3, ... t

n dac marcajele M

1, M

2, M

3, ... M

n a..

M -t1-> M

1 -t

2-> M

2 -t

3-> M

3 ... -t

n-> M

n=M'

Fie RP i M0 un marcaj iniial. Clasa marcajelor accesibile din M

0

este notat A(M0).


Fie:

Locurile l1, l2, l3; Marcajul iniial M = [2, 0, 1]; Tranziia t, executabil.

Execuia este instantanee.


Execuia unei tranziii

Marcajul dup execuia tranziiei M' = [1, 1, 2].

Fiecare loc de intrare pierde un punct; Fiecare loc de ieire primete un punct.

l1

l2

l3

t



Ce modelm?

Paralelismul: P1 i P

2 se execut n paralel.

Sincronizarea:

Rendez-vous. Semafor.

P

2

P

1

t1

t2

*

t1 t

P1

P2

A B

C D

A

C

S



Ce mai modelm?

Memorarea unei condiii i a opusului su.

Citirea unei condiii, fr modificarea ei.

Excluderea mutual.

A C E B D

1

4

2

3

*

C t3

A'

B'

*

C not C

t1

t2

A

B

Iniial resursa liber, nimeni nu o folosete Resursa e acaparat,

o folosete doar un utilizator Resursa e eliberat,

poate fi refolosit



Analiza prin RP a unui sistem simplu (1)

Pe o mas de biliard se pot deplasa fr frecare 2 bile identice, n lungul axei mesei, cu viteze identice (sau nule).

Reguli:

Tranziiile modeleaz evenimente care se pot produce n sistem;

Locurile modeleaz condiiile necesare producerii evenimentelor;

Marcajul reprezint starea sistemului.

Evenimentele sunt ciocniri:

ntre bila roie i marginea stng;

ntre bila galben i marginea dreapt;

ntre bile.

Condiiile:

Starea de micare.



Stnga

Dreapta Stnga

Repaus

Dreapta

Analiza prin RP a unui sistem simplu (2)

Stare iniial: bila roie spre dreapta, bila galben spre stnga. Stare iniial: bila roie spre stnga, bila galben spre dreapta. Stare iniial: bila roie spre dreapta, bila galben n repaus. Stare iniial: bila roie spre dreapta, bila roie spre stnga.



Alte probleme

Productor consumator:

Productorul produce produse;

Productorul depune produsele n buffer;

Consumatorul preia produse din buffer;

Consumatorul consum produsele;

Bufferul e finit.

Problema filozofilor:

Filozofii stau la mas, unde mnnc i gndesc, alternativ;

Pentru a mnca trebuie s foloseasc 2 furculie;

Nu se impun restricii de programare a activitilor;

Filozofii nu trebuie s moar de inaniie.

P C



Reele Petri pure

O tranziie impur are locuri de intrare care sunt i de ieire:

Pre(t) Post(t) .

O reea Petri e impur dac are cel puin o tranziie impur.

Reelele impure mai dificil de analizat purificare.

Algoritm de purificare (crete dimensiunea reelei!):

Se adaug un loc special L0, cu marcaj 1;

Se transform fiecare tranziie t ntr-un ansamblu de 2 tranziii t', t i un loc intermediar l, cu marcaj 0;

Se adaug un arc de la L0 la fiecare tranziie t' i un arc de la fiecare

tranziie t ctre L0.

Dac Ni, L

i pentru reeaua impur:

Np = 2 * N

i;

Lp = L

i + N

i + 1.

Exemplu: l1

t1 l1 t1 L0

t'1

l Purificare



Modelarea protocolului start-stop

Model algoritmic:

Transmitor: do { asteapta cerere emisie (ct,msg) pregateste mesaj (msg,m) transmite mesaj (m) asteapta confirmare (r) } forever;

Receptor: do { asteapta mesaj (m) pregateste raspuns (m,r, msg) transmite confirmarea (r) asteapta cerere receptie (cr) transfera mesaj (msg) } forever

Model de automat finit:

r /

/ m

A

B

C

ct, msg /

cr / msg

/ r

m /

D

E

F

A

B

C

D

E

F



Reeaua Petri asociat

E

t6

B

C

A

M

R

D

F

t2

t1

t3

t4

t5

*

*



Tranziiile i starea iniial

Tranziii:

t1 preluare mesaj produs de utilizatorul transmitor;

t2 transmitere mesaj mediului de comunicare;

t3 recepie mesaj de la mediu;

t4 transmitere confirmare;

t5 recepie confirmare;

t6 consumare mesaj de utilizator receptor.

Starea iniial i marcajul corespunztor unei stri iniiale M0:

Entitatea emitoare ateapt producerea unui mesaj (A);

Entitatea receptoare este pregatit pentru recepie (D);

Mediul de transmisie este gol.



Maina de puncte

Diagram de tranziii.

Exploreaz marcajele posibile.

Dificil de folosit la sisteme complexe.

AD

BF

AF

CE

CMD

BD

CRF CRD

CMF

t1

t2

t3

t4

t5

t6

t1

t2

t5

t6

t6

t6

E t6

B

C

A

M

R

D

F

t2

t1

t3

t4

t5

*

*



Validarea protocoalelor - proprieti generale

Mrginire:

Orice M accesibil din M0 i orice l din L, avem M(l)



Persistena

Conflicte efective:

Conflicte structurale, dar ne-efective:



Validarea protocoalelor - proprieti specifice

Invariani:

Pe locuri (L-invariani):

M(A) + M(B) + M(C) = 1, pentru orice M A(M0).

Component / reea conservativ.

Pe tranziii (T-invariani):

Avans sincron 0



Validarea protocoalelor - metode

Maina de puncte.

Arbori i grafuri de acoperire.

Calculul invarianilor (model algebric).

Reducerea modelelor.



Maina de puncte

Proprieti:

sigur;

viabil;

home state;

invariani?

AD

BF

AF

CE

CMD

BD

CRF CRD

CMF

t1

t2

t3

t4

t5

t6

t1

t2

t5

t6

t6

t6

E t6

B

C

A

M

R

D

F

t2

t1

t3

t4

t5

*

*



Arbori i grafuri de acoperire

Analiza reelelor nemrginite.

l1

l2

l3

t1

t2

t3

[100] M0

| t1

|

[011] M1

t2/ \t

3

/ \

[000] M2 [10&] M

0+

| t1

|

[01&] M1+

t2/ \t

3

/ \

[00&] M2+ [10&] M

0+

Proprieti:

Locurile l1 i l

2 sunt mrginite; l

3 nu este;

Exist o infinitate de blocri (M2 si M

2+);

RP este cvasi-viabil.

*

* * * * * * *



Construire arbore de acoperire

construire_arbore_acoperire() {

calculeaza succesoarele lui M0;

for (fiecare succesor M) if (M>M0) marcheaza cu & fiecare componenta a lui M superioara componentei

corespunzatoare din M0;

while (exista un marcaj nou Mi, neconsiderat) if (nu exista pe calea de la M0 la Mi un marcaj Mj=Mi)

{

calculeaza succesoarele lui Mi;

for (fiecare succesor Mk al lui Mi) {

o componenta & a lui Mi ramine & in Mk;

if (exista un marcaj Mj pe calea de la M0 la Mk cu Mk>Mj) marcheaza cu & fiecare componenta din Mk superioara

componentei corespunzatoare din Mj;

}

}

}



Analiza RP prin calculul invarianilor

Fie RP o reea Petri pur (fr bucle), n care L i T sunt ordonate (arbitrar):

L: l1 < l2 < ...< lm,

T: t1 < t2 < ...< tn.

Matricea A : L x T Z cu A [li, tj] = O (tj, li) I (li, tj) este matricea de incidene a lui RP.

Notm:

A [li, -] = linia li;

A [-, tj] = coloana tj.

L-vector = o matrice coloan indexat dup L.

T-vector = o matrice coloan indexat dup T.



Modelul excluderii mutuale

Matricea de incidene:

A | 1 2 3 4

------------------------

a | -1 1

b | 1 -1

c | -1 1

d | 1 -1

e | -1 1 -1 1

A[a,1] = O[a,1]-I[a,1] = 0-1 = -1

A[b,1] = O[b,1]-I[b,1] = 1-0 = 1

...

b e

c

d

a

1

4

3

2



Aspecte de corectitudine

Aspecte de corectitudine:

Garantare c nu se pierd puncte;

Posibilitate reproducere marcaje.

Exemple:

RP fr pierderi de puncte dar cu marcaj nereproductibil.

RP fr pierderi de puncte i cu marcaj reproductibil;

RP cu pierderi de puncte i cu marcaj nereproductibil.

*

*

b c a t1

t2

**

b c a t

1 t2

t3



L-invariani

Pentru modelul excluderii mutuale, fie:

M i M' cu M -t> M',

M' = M + A[-, t];

invariantul M[a]+2M[b]+M[c]+2M[d]+M[e] = 3 (pentru orice M).

Pentru gT = [1, 2, 1, 2, 1] i M, M' reprezentai ca M-vectori

gT.M = gT.M' = gT.M + gT.A[-,t].

Rezult:

gT.A[-,t] = 0;

gT.A = 0 (relaia anterioar valabil pentru orice t).

g este L-invariant.

Un l-vector I este un L-invariant IT.A = 0.

Un L-invariant ne-negativ I se numete minimal nu exist un I' a.i. 0 < I' < I.



U|A | 1 2 3 4

-------------------------------

a | 1 0 0 0 0 -1 1

b | 0 1 0 0 0 1 -1

c | 0 0 1 0 0 -1 1

d | 0 0 0 1 0 1 -1

e | 0 0 0 0 1 -1 1 -1 1

-------------------------------

a+b | 1 1 0 0 0 0 0 0 0

b+e | 0 1 0 0 1 0 0 -1 1

Exemplul excluderii mutuale (1)

Pentru j=1 se adaug liniile a+b i b+e




U|A | 1 2 3 4

---------------------------------

c | 0 0 1 0 0 -1 1

d | 0 0 0 1 0 1 -1

a+b | 1 1 0 0 0

b+e | 0 1 0 0 1 -1 1

----------------------------------

c+d | 0 0 1 1 0

d+b+e| 0 1 0 1 1

Pentru j=3 se adaug liniile c+d i d+b+e




U|A | 1 2 3 4

--------------------------------

d+b+e| 0 1 0 1 1 0 0 0 0

c+d | 0 0 1 1 0 0 0 0 0

a+b | 1 1 0 0 0 0 0 0 0

_ _ _ _ _ _

| 0 | | 0 | | 1 |

| 1 | | 0 | | 1 |

I1 = | 0 | I2 = | 1 | I3 = | 0 |

| 1 | | 1 | | 0 |

|_ 1 _| |_ 0 _| |_ 0 _|



Calcul invariani

calcul_invarianti() {

construieste matricea (U|A);

for (fiecare indice j al tranzitiei tj) {

adauga la matricea (U|A) attea linii i cte combinatii lineare de cte dou linii cu coeficienti intregi pozitivi in care se anuleaz elementul [i,j] exist;

elimin din matricea (U|A) liniile i n care elementul [i,j] este nenul.

}

}



Folosire invariani

Regul:

Dac M este un marcaj i I un L-invariant atunci pentru orice M' accesibil din M:

IT.M' = IT.M.

Utilizare:

Verificarea evitrii anumitor marcaje:

Dac exist un invariant I a.. IT.M' IT.M atunci M' nu poate fi accesibil din M.

Gsirea condiiilor necesare completrii unui marcaj M' accesibil din M i cunoscut parial;

Deducerea unor proprieti generale ale marcajelor accesibile.



Exemplu pentru excluderea mutual

Invarianii gsii sunt:

I1 = [0 1 0 1 1];

I2 = [0 0 1 1 0];

I3 = [1 1 0 0 0];

I = [1 2 1 2 1] (invariantul global al reelei).

Din relaia IT.M = IT.M0 obinem pentru cei trei invariani:

M[b] + M[d] + M[e] =1;

M[c] + M[d] = 1;

M[a] + M[b] = 1.

Relaiile exprim:

Condiia de excludere mutual (prima relaie);

Sigurana: M[li]



Reproducerea marcajelor

Efectul tranziiei 1, scris M0 + A[-,1] = M

1 este echivalent cu:

_ _

| 1 |

M0 + A. | 0 | = M1

| 0 |

|_ 0 _|

Efectul cumulat al tranziiilor 1 i 2 poate fi scris:

_ _

| 1 |

M0 + A. | 1 | = M0

| 0 |

|_ 0 _|



T-invariani

T-vectorul J care reprezint numrul de execuii ale tranziiilor i este o soluie a ecuaiei A.y = 0 este T-invariant:

_ _

| 1 |

J = | 1 |

| 0 |

|_ 0 _|

J este un T-invariant A.J = 0.

Un T-invariant ne-negativ J se numete minimal nu exist J' a.. 0 < J' < J.

Dac J este un T-invariant atunci exist un marcaj reproductibil prin execuia tranziiilor n conformitate cu J.

Pentru modelul excluderii mutuale, RP revine n marcajul iniial prin execuia tranziiilor 1 i 2 (J1) sau 3 i 4 (J2).



Calculul T-invarianilor

Din xT.A=0 i A.y=0 (sau yT.AT =0) rezult c:

T-invarianii asociai lui A sunt L-invarianii lui AT.

AT este matricea de incidene corespunztoare RP duale.

RP dual se obine astfel:

Fiecrui loc n RP i corespunde o tranziie n RP dual;

Fiecrei tranziii n RP i corespunde un loc n RP dual;

Fiecrui arc n RP i corespunde un arc orientat n sens contrar n RP dual.



Reducerea RP

Reducerea are ca scop scderea dimensiunilor reelei.

Reducerea trebuie s pstreze unele din proprietile reelei.

Reducere fr pstrarea invarianilor:

R1 (Reducerea unui loc);

R2 (Reducerea unui loc implicit);

R3 (Reducerea unei tranziii neutre);

R4 (Reducerea tranziiilor identice).

Reducere cu pstrarea invarianilor:

Ra (Reducerea unei tranziii impure);

Rb (Reducerea unei tranziii pure).



R1: Reducerea unui loc

Eliminarea unui loc l:

Dac l are j intrari i k ieiri, ele sunt nlocuite prin j*k tranziii, obinute prin contopirea unei tranziii de intrare cu una de ieire;

Ieirile unei tranziii de intrare (ex. d - ieirea lui t1) devin ieiri ale tranziiei obinut prin contopire (t12).

a b

c d

l

a b

c d

t1 t2

t3 t4

t13 t23

t14 t24

* *

a a b

c d

e

e

b

d

t1

t2

t12



R2: Reducerea unui loc implicit

Loc implicit:

Marcajul su permite ntotdeauna execuia oricrei tranziii de ieire, care ar fi executabil dac se ignor l;

Marcajul su poate fi determinat din marcajul celorlalte locuri.

b

a

l

a

b

t1

t2

t3

t1

t2

t3



R3: Reducerea unei tranziii neutre

Tranziia t este neutr Pre(t) = Post(t).

Eliminare exist t't cu O(t',l)>=I(l,t) pentru orice l din Pre(t).

t'

t



R4: Reducerea tranziii identice

Tranziii identice: au aceleai locuri de intrare i de ieire.

Dac exist n tranziii identice, se elimin n-1 din ele.



Ra: Reducerea unei tranziii impure

O tranziie impur are locuri de intrare care sunt i de ieire:

Pre(t) Post(t) .

l1

t1

l1

Ra



Rb: Reducerea unei tranziii pure

Reducere tranziie pur:

Se elimin tranziia pur t;

Fiecrui cuplu de locuri li din Pre(t) i l

j din Post(t) i se asociaz un

loc li+l

j al crui marcaj este M(l

i)+M(l

j).

l1

t Rb

l2

l1+l

2



Cazuri ireductibile

Reea conservativ: M(l1)+M(l2)=1.

* * *

l1 + l2

l5 + l6

l7 + l8

t1

t2 t3

t4



Proprieti pstrate prin reducere

X X Invariani

X X X X Conservabilitatea

X X X X Starea de revenire

X X X X Evitarea blocrii

X X X X Cvasi-viabilitatea

X X X Viabilitatea

X X X Sigurana

X X X X Mrginirea

Rb Ra R4 R3 R2 R1 Reduceri

Proprieti



Exemplu reduceri (1)

t2

*

*

*

*

l1

l2 l3

l1

l4 l5

l2+l4 l3

l5

t3

t4 t4

t3

Dup Rb(t2)



Exemplu reduceri (2)

*

*

* **

l1

l2+l4 l3+l5

l1+l3+l5 l1+l2+l4

t4

t1

*

l1+l2+l4 l1+l3+l5

**

t1

Dup Ra(t1)

Dup Rb(t3)

Dup Rb(t4)



Reduceri pentru RP generalizate

Reducerea R'a (tranziie impur):

Reducerea R'b (tranziie pur):

p

q

p-q

q-p

ti

p1

li

p

q t

tk

lk

q1

ti

q.li+p.lk

p.q1

q.p1

tk



Exemplu reduceri RP generalizate (1)

l4 * **

l3

l1

l4

l2

t2

t1 t3

2

2

2

3

* **

l3

t2

t3

2

2

2

3

l1+l2

Se aplic Rb(t1): M(l1+l2) = 1*0+1*2 Ra(t3)



Exemplu reduceri RP generalizate (2)

*

**

l3

l1+l2

l4

t2

2

** **

l1+l2 l3+2.l4

t3

** **

l3+2.l4

t3

2

l1+l2

2

Rb(t2)

Ra(t3)

2

t3



Sumar

Verificarea protocoalelor se face naintea implementrii.

Modele de specificare a protocoalelor: Tranziionale; Algoritmice; Hibride.

Reele Petri: model tranziional care poate fi analizat prin:

Maina de puncte.

Arbori i grafuri de acoperire.

Calculul invarianilor (model algebric).

Reducerea modelelor.

n cazul sistemelor complexe are loc explozia strilor:

Analiza vizual imposibil;

Analiza automat prin programe (utilitare).

Date post:	13-Sep-2015
Category:	Documents
Upload:	florin-alex
View:	212 times
Download:	0 times

11_Verificare_protocoale

Documents