Laborator SVI-SW

L2. Bazele procesului de validare

2.1. Sisteme de tranzitii

Sistemele de tranzitii (mai poarta denumirile de automate sau masini cu stari) sunt de regula utilizate in descrierea comportamentului sistemelor informatice. Sunt grafuri orientate, unde nodurile reprezinta stari, iar muchiile tranzitii. O stare contine informatii despre sistem, intr-un anumit moment al vietii sale. De exemplu, pentru programe secventiale, starile contin valorile curente ale tuturor variabilelor locale, impreuna valoarea curenta a contorului de program, care indica urmatoarea instructiune de executat. Tranzitiile indica modul in care sistemul evolueaza de la o stare la alta.
In literatura exista mai multe propuneri de sisteme de tranzitii. In cadrul acestei lucrari, ne vom referi la sisteme de tranzitii avand nume de actiuni drept tranzitii si propozitii atomice drept stari. Actiunile sunt utilizate pentru descrierea mecanismelor de comunicatie intre procese (pentru notatii, vom utiliza caractere din alfabetul grecesc). Propozitiile atomice exprima intuitiv date simple privind starile sistemului considerat (si sunt reprezentate prin caractere din alfabetul latin).

Definitia 2.1. Sistem de Tranzitii Kripke

Un sistem de tranzitii TS este un tuplu (S, Act, →, I, AP, L) unde:

S este multimea starilor
Act este multimea actiunilor
→ ⊆ S × Act × S este functia de tranzitie
I ⊆ S reprezinta multimea starilor initiale
AP este multimea propozitiilor atomice si
L : S → 2^AP este functia de etichetare.

Sistemul de tranzitii se numeste finit daca S, Act si AP sunt finite.
Comportamentul automatului este urmatorul: sistemul porneste dintr-o stare initiala s₀ ∈ I si evolueaza conform functiei de tranzitie →. Daca s este starea curenta, atunci o tranzitie (s, α, s')∈→ este selectata in mod nedeterminist, se executa actiunea α iar sistemul trece in starea s'. Procedura de selectie continua in toate starile urmatoare si se incheie atunci cand sistemul ajunge intr-o stare din care nu mai sunt posibile alte tranzitii. In cazul in care sunt posibile mai multe tranzitii dintr-o stare, urmatoarea este aleasa intr-o maniera pur nedeterminista.
Daca multimea starilor initiale este vida, sistemul nu va avea nici un comportament, intrucat nu se poate selecta nici o stare initiala. Pentru tranzitii vom utiliza notatia alternativa:

Functia de etichetare L asociaza o multime L(s) ∈ 2^AP de propozitii atomice fiecarei stari s. L(s) reprezinta acele propozitii atomice care sunt satisfacute de starea s. Considerand Φ o formula a logicii propozitionale, spunem ca s satisface formula Φ daca aceasta este adevarata in evaluarea L(s), adica: s ⊨ Φ ⇔ L(s) ⊨ Φ

Nota: cu ajutorul propozitiilor atomice se vor exprima toate proprietatilor sistemului care se doresc a fi verificate.

Fie exemplul simplist al automatului cu bere din figura urmatoare. Starile sunt reprezentate prin elipse, iar tranzitiile prin sageti. Numele fiecarei stari este trecut in interiorul elipsei.

Starile initiale sunt indicate prin sageti care nu au nici o sursa.
Spatiul starilor este S = { plateste, alege, bere, suc }. Multimea starilor initiale va contine un singur element: I = { plateste }. Actiunea pune_moneda denota introducerea unei monezi de catre utilizator, in timp ce actiunile (automatului) ia_berea si ia_sucul sugereaza livrarea berii, respectiv a sucului. Tranzitiile ale caror etichete nu sunt de interes in cazul nostru, sugerand actiuni interne ale automatului, se vor nota cu simbolul τ.
Multimea actiunilor va fi: Act = { pune_moneda, ia_berea, ia_sucul, τ} Exemple de tranzitii pot fi:

Trebuie mentionat faptul ca, in acest exemplu, automatul alege in mod nedeterminist bautura pe care o va servi.
Propozitiile atomice din cadrul sistemului de tranzitii depind de proprietatile luate in considerare. O alegere simpla poate fi utilizarea numelor starilor ca propozitii atomice (L(s) = {s}). Daca singurele proprietati relevante se refera la bauturi, este suficient setul de propozitii atomice AP = {platit, livrat}, avand functia de etichetare:
L(plateste) = ∅, L(suc) = L(bere) = {platit, livrat}, L(alege) = {platit} Aici platit indica faptul ca utilizatorul a introdus deja moneda, dar nu si-a ridicat inca bautura.
Foarte important in modelarea sistemelor hardware si software este nedeterminismul, care in acest context reprezinta mai mult decat un concept teoretic: nedeterminismul este utilizat in modelarea executiei paralele a proceselor prin intretesere si pentru modelarea unor conflicte care pot interveni (de exemplu, accesarea simultana a unei resurse comune de mai multe procese). In afara de paralelism, nedeterminismul este util in subspecificarea proceselor si modelarea interfetei cu un mediu necunoscut sau impredictibil (de exemplu, utilizatorul uman). Termenul de subspecificare se refera la fazele timpurii ale definirii modelului, cand modelul poate prezenta diverse optiuni sau comportamente nedeterministe.

Definitia 2.2. Predecesori si succesori directi

Pentru s ∈ S si α ∈ Act, se poate defini multimea α-succesorilor lui s astfel: Post( s, α ) = {s' ∈ S | (s, α, s') ∈ → } Multimea tuturor succesorilor lui s va fi

Similar, se va defini multimea predecesorilor lui s: Pre( s, α ) = {s' ∈ S | (s', α, s) ∈ → } , Fiecare stare s' ∈ Post ( s, α ) se numeste α-succesor direct al lui s. Prin urmare, fiecare stare s' ∈ Post ( s ) va purta numele de succesor direct al starii s. Pe baza acestor definitii, putem spune ca un automat determinist este acela care are cel mult o stare initiala, iar toate starile sale au cel mult un α-succesor, ∀ α ∈ Act.

Definitia 2.3. Stari finale

O stare s dintr-un sistem de tranzitii se numeste finala daca si numai daca Post(s) = ∅.
Cu alte cuvinte, starile finale ale unui automat sunt sunt starile din care nu mai sunt posibile alte tranzitii.

Definitia 2.4. Fragment de executie

Fie TS = (S, Act, →, I, AP, L) un sistem de tranzitii. Un fragment finit de executie ϱ a lui TS este o secventa alternanta de stari si actiuni care se incheie intr-o stare.
ϱ = s₀, α₁, s₁, α₂, s₂, α₃, ... α_n,s_n, asfel incat,

∀ 0 ≤ i < n, unde n ≥ 0 este lungimea fragmentului.
Un fragment infinit de executie ρ al lui TS este o secventa infinit alternanta de stari si actiuni:
ρ = s₀, α₁, s₁, α₂, s₂, α₃, ... α_n,s_n, asfel incat,

∀ 0 ≤ i.
Secventa s, unde s ∈ S, este un fragment finit de executie de lungime zero.

Definitia 2.5. Fragment maxim si fragment initial de executie

Un fragment maxim de executie este fie un fragment finit de executie care se termina intr-o stare finala, fie un fragment infinit de executie.
Un fragment de executie se numeste initial daca incepe cu o stare initiala (daca s₀ ∈ I).

De exemplu, pentru automatul de bere de mai sus, avem fragmentele de executie:

Sunt initiale fragmentele ρ₁ si ϱ.
Fragmentul ϱ nu este maxim, intrucat nu se termina intr-o stare finala.
Presupunand ca fragmentele ρ₁ si ρ₂ sunt infinite, putem spune ca acestea sunt maxime.

Definitia 2.6. Executie

Se numeste executie a sistemului de tranzitii TS un fragment initial, maxim de executie.
In exemplul anterior, doar fragmentul ρ₁ poate fi considerat executie.

Definitia 2.7. Stari accesibile

Fie TS = (S, Act, →, I, AP, L) un sistem de tranzitii. O stare s ∈ S se numeste accesibila daca in cadrul sistemului de tranzitii exista un fragment initial, finit de executie astfel incat

Explozia masinilor cu stari.

Una dintre problemele cele mai importante ale procesului de validare a sistemelor este aceea a dimensiunii spatiului starilor.
Fie Var multimea variabilelor unui proces. Vom nota dom(x) domeniul valorilor unei variabile x ∈ S. Practic, facand abstractie de operatiile executate de un anumit proces, numarul starilor acestuia va fi de ordinul:

Numarul starilor creste exponential cu numarul variabilelor unui proces. Pentru N variabile cu domenii de k valori posibile, se obtine un numar de pana la k^N stari. Aceasta crestere exponentiala poarta denumirea de problema a exploziei spatiului starilor.
De exemplu, un sistem simplu, cu trei variabile logice (boolean) si sase variabile intregi (cu domenii de valori {0,.. 9}) are un spatiu de stari de ordinul 2³ ‧ 10⁶ (milioane de stari).
Modelele sistemelor reale presupun de regula executia in paralel a mai multor procese. Asincronismul acestora, sau posibilitatea comunicarii dintre procese prin intermediul variabilelor partajate vor conduce la accentuarea acestei probleme.
Pentru reducerea dimensiunii spatiilor de stari se folosesc doua tehnici: 1) reprezentarea spatiului de stari prin diagrame de decizie binare(BDD); 2) reducerea partiala a ordinului(POR) automatelor, prin evaluarea echivalentei fragmentelor de executie. In acest caz tehnica de validare poarta numele de "model checking" simbolic.

Spuneti cate stari sunt generate de urmatorul cod Promela:

init{
	byte i = 0;
	do
	::	i = i + 1
	od
}

Verficati raspunsul prin simulare. Ce observati ? Este dependenta simularea de tipul variabilei i ?

2.2. Validarea in SPIN

Fie codul (din cadrul primei lucrari; aici - fisierul 30.pml sau p96.1.pml):

byte stare = 1;

proctype A() {
    (stare == 1) -> stare = stare + 1
}
proctype B() {
    (stare == 1) -> stare = stare - 1
}

init {
    run A();
    run B();
}

Procesul de validare in SPIN poate fi impartit in trei etape:

Modelarea in Promela si generarea verificatorului:
```
$ spin -a 30.pml
```
Compilare verificator
```
$ gcc -o pan pan.c
```

Verficare efectiva

$ ./pan
hint: this search is more efficient if pan.c is compiled -DSAFETY
pan:1: invalid end state (at depth 4)
pan: wrote 30.pml.trail

(Spin Version 6.0.1 -- 16 December 2010)
Warning: Search not completed
    + Partial Order Reduction

Full statespace search for:
    never claim         	- (none specified)
    assertion violations	+
    acceptance   cycles 	- (not selected)
    invalid end states	+

State-vector 24 byte, depth reached 5, errors: 1
        6 states, stored
        0 states, matched
        6 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

    2.501	memory usage (Mbyte)


pan: elapsed time 0 seconds

Documentatia pentru procesul de verificare se gaseste la adresa http://spinroot.com/spin/Man/Pan.html
Explicatie - rezultatul verificarii:

Prima linie corespunde situatiei in care nu se doreste detectia ciclurilor (si cazul nostru); la compilare poate fi folosita, alternativ, linia
```
$ gcc -DSAFETY -o pan pan.c
```

In mod implicit se considera stare finala valida numai sfarsitul blocului de program (marcat cu } ), altfel validatorul considera toate executiile posibile ca fiind eronate. Fisierul .trail poate fi utilizat pentru a simula in mod ghidat modelul (refacerea pasilor acestei executii eronate):

$ spin -t -p 30.pml
Starting A with pid 1
  1:	proc  0 (:init:) 30.pml:11 (state 1)	[(run A())]
Starting B with pid 2
  2:	proc  0 (:init:) 30.pml:12 (state 2)	[(run B())]
  3:	proc  2 (B) 30.pml:7 (state 1)	[((stare==1))]
  4:	proc  2 (B) 30.pml:7 (state 2)	[stare = (stare-1)]
  5: proc 2 terminates
spin: trail ends after 5 steps
#processes: 2
	stare = 0
  5:	proc  1 (A) 30.pml:4 (state 1)
  5:	proc  0 (:init:) 30.pml:13 (state 3) 
3 processes created

pentru linia
```
+ Partial Order Reduction
```
semnul + inseamna ca a fost utilizat algoritmul de reducere partiala a ordinului. Se poate dezactiva la compilare cu -DNOREDUCE.
Urmatoarele linii specifica optiunile de verificare selectate/active (tot prin +).
Daca exista instructiuni care nu au putut fi executate(en dead code), vor fi specificate la sfarsitul verificarii. Nu este cazul pentru exemplul nostru, dar rezultatul poate arata astfel:
```
unreached in proctype ProcA
    line 7, state 8, "Gaap = 4"
    (1 of 13 states)
```

Trebuie mentionat faptul ca in mod implicit verificarea se opreste la prima eroare detectata si salveaza un singur trail. Printre optiunile de verificare (pan) de interes in cazul nostru se numara:

-a
find acceptance cycles (available if compiled without -DNP)
-cN
stop at Nth error (defaults to first error if N is absent)
-e
create trails for all errors encountered (default is first one only)
-i
search for shortest path to error (causes an increase of complexity)
-l
find non-progress cycles (requires compilation with -DNP)
-n
no listing of unreached states at the end of the run
-q
require empty channels in valid endstates

Exemplul(1) - detectia tuturor erorilor:

$ ./pan -c0
pan:1: invalid end state (at depth 4)


(Spin Version 6.0.1 -- 16 December 2010)
    + Partial Order Reduction

Full statespace search for:
    never claim         	- (none specified)
    assertion violations	+
    cycle checks       	- (disabled by -DSAFETY)
    invalid end states	+

State-vector 20 byte, depth reached 9, errors: 2
       16 states, stored
        2 states, matched
       18 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

    2.501	memory usage (Mbyte)

unreached in proctype A
    (0 of 3 states)
unreached in proctype B
    (0 of 3 states)
unreached in init
    (0 of 3 states)

pan: elapsed time 0 seconds

Exemplul(2) - verificare fara reducere partiala a ordinului:

$ gcc -DSAFETY -DNOREDUCE -o pan pan.c
$ ./pan -c0
pan:1: invalid end state (at depth 4)

(Spin Version 6.0.1 -- 16 December 2010)

Full statespace search for:
    never claim         	- (none specified)
    assertion violations	+
    cycle checks       	- (disabled by -DSAFETY)
    invalid end states	+

State-vector 20 byte, depth reached 9, errors: 3
       20 states, stored
        5 states, matched
       25 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

    2.462	memory usage (Mbyte)

unreached in proctype A
    (0 of 3 states)
unreached in proctype B
    (0 of 3 states)
unreached in init
    (0 of 3 states)

pan: elapsed time 0 seconds

Q1)Parcurgeti toti pasii anterior prezentati. Ce se observa pentru ultimul exemplu, cu si fara reducere partiala a ordinului? Pentru ultimle doua exemple, salvati si trails (./pan -c0 -e) si simulati ghidat (spin -t<[0-9]*]> -p <spec.pml>).

Q2) Folositi instructiunea goto pentru a crea o zona de cod nexecutabil (deadcode) in fisierul cu specificatia anterioara. Validati din nou modelul si observati cum este raportata acest tip de eroare.

Marcarea starilor finale

Starile finale arbitrare pot fi declarate valide prin marcare explicita cu ajutorul etichetelor incepand cu cuvantul cheie end.
Sintaxa:

end[a-zA-Z0-9_]*: statement

Fisierul 30.pml corectat ar trebui sa arate astfel:

byte stare = 1;

proctype A() {
    (stare == 1) -> stare = stare + 1;
end:
    skip
}
proctype B() {
    (stare == 1) -> stare = stare - 1;
end:
    skip
}

init {
    run A();
    run B();
}

Este posibila si alternativa:

proctype B() {
    (stare == 1) -> 
end:
                    stare = stare - 1;
}

Verificati noul model:

$ spin -a 31.pml 
$ gcc -DSAFETY -DNOREDUCE -o pan pan.c
$ ./pan -c0

Mai este detectata vreo eroare?

Eroare "deadlock" := o stare (invalida, nefinala) de blocare a sistemului(eroare) in care nicio actiune nu mai poate fi efectuata (i.e. nu exista instructiuni executabile). De exemplu, pentru o stare data lipsa unei tranzitii pentru consumarea unui mesaj din bufferul de receptie (FIFO); se mai numeste, in acest caz, eroare de subspecificare. Pentru detectarea acestei erori se pot folosi etichete end.

Asertiuni

Sintaxa:

assert( conditie )

Aceste instructiuni sunt mereu executabile si nu au nici un efect asupra executiei codului. Sunt utilizate in cadrul procesului de validare, pentru a detecta situatii nedorite (conditia trebuie sa fie mereu adevarata). Stim deja ca rezultatul executiei codului din exemplul de mai sus este unul imprevizibil atunci cand nu sunt folosite sectiunile atomice. Putem verifica, la finalul executiei fiecarui proces, daca rezultatul este unul corespunzator sau nu:

byte stare = 1;

proctype A() {
    (stare == 1) -> stare = stare + 1;
    assert(stare == 2);
end:
    skip
}
proctype B() {
    (stare == 1) -> stare = stare - 1;
    assert(stare == 0);
end:
    skip
}

init {
    run A();
    run B();
}

Validati

$ spin -a 32.pml 
$ gcc -DSAFETY -DNOREDUCE -o pan pan.c
$ ./pan -c0 -e

De ce apar si erori invalid end state? Simulati ghidat.

Invarianti de sistem

O aplicatie mai generala a instructiunii assert este aceea de formalizare a invariantilor de sistem: conditii logice care trebuie sa fie adevarate in toate starile sistemului. Un exemplu ar putea fi:

proctype monitor(){
	assert(invariant)
}

In aceasta situatie trebuie mentionat faptul ca, indiferent de numele dat procesului monitor, asertiunea va fi executata in orice moment al verificarii. totusi, un efect al acestei forme de verificare va fi cresterea numarului de stari. Fie fisierul 33.pml (avand corectata greseala din exemplele anterioare), in cadrul caruia s-a adaugat si o variabila contor.

byte stare = 1;
byte count = 0;

proctype A() {
end:
    (stare == 1) -> stare = stare + 1;
    count++;
}

proctype B() {
end:
    (stare == 1) -> stare = stare - 1;
    count++;
}


init {
    run A();
    run B();
}

Teoretic, unul singur dintre cele doua procese ar trebui sa poata modifica variabila de stare, deci valoarea maxima pentru contor ar trebui sa fie 1. In consecinta, adaugand procesul monitor:

active proctype monitor(){
    assert(count <= 1)
}

Verificati si comparati numarul de stari cu cel de la exemplul precedent.

Eroare "livelock" (i.e. non-progress cycles)

Prin eroare "livelock" se intelege un ciclu invalid al secventei de executie format dintr-un numar finit de stari care se repeta la infinit. Prin ciclu de executie invalid se intelege, orice ciclu care nu include o stare finala sau o stare marcata explicit de tip progres si care nici nu a fost declarat explicit ciclu acceptabil.

Etichetele "progress"

Prin urmare, pentru a detecta erorile "livelock" au fost definite etichete progress, prin care se marcheaza explicit in specificatie care sunt acele instructiuni care constituie un progres in executia modelului (ex. incrementare, receptionare mesaj). Aceasta eticheta exprima criteriul de corectitudine "nu exista o bucla infinita care nu trece prin starea de progres".Un model poate avea mai multe instructiuni marcate progress, insa este suficient ca o secventa ciclica de executie sa includa o singura stare de progres pentru a nu fi susceptibila de a fi o eroare "livelock".
Sintaxa:

progress[a-zA-Z0-9_]*: statement

Etichetele "accept"

De asemenea, un ciclu de executie (non-progres)poate fi declarat explicit ca fiind valid prin etichete accept. Cu acest tip de etichete se poate specifica criteriul de corectitudine "instructiunea nu face parte dintr-o bucla infinita invalida".
Sintaxa:

accept[a-zA-Z0-9_]*: statement

Conditii temporale

Cele mai populare limbaje formale folosite pentru exprimarea conditiilor temporale sunt LTL(Linear Temporal Logic) si CTL(Computational Tree Logic). Expresivitatea acestor limbaje este complementara, asa cum este ilustrata in diagrama Venn de mai jos.

[in aceasta versiune a materialului este tratat numai LTL, incepand cu lucrarea urmatoare]