L1. Introducere in PROMELA. Simularea in SPIN.

Procesul dezvoltarii unui sistem SW complex implica parcurgerea etapelor:

• realizarea diverselor studii (de oportunitate, risc, fezabilitate etc.). Desi aceasta faza nu este obligatorie, poate afecta nu doar organizarea intregului proces de dezvoltare, ci si resursele alocate proiectului
• specificarea cerintelor si analiza acestora;
• proiectarea sistemului – stabilirea arhitecturii, structurii si comportamentului algoritmilor utilizati;
• implementarea – sau in unele cazuri, prototipizarea si
• testarea (sau verificarea) sistemului.

Procesul de verificare este - in acest caz - unul a posteriori. In cadrul acestui laborator vom aborda procesul denumit model checking: o tehnica automatizata care, pornind de la modelul cu stari finite al unui sistem si o proprietate formala, verifica sistematic daca proprietatea este valida pentru acel model.

Sintaxa Spin - simulare

http://spinroot.com/spin/Man/Spin.html

spin [options] file 
spin -V

Simulation Options

• -B Suppresses the verbose printout at the end of a simulation run (giving process states etc.).
• -b Suppresses the execution of printf statements within the model (see also -T).
• -c Produce an ASCII approximation of a message sequence chart for a random or guided (when combined with -t) simulation run. See also option -M.
• -g Shows at each time step the current value of global variables (see also -w).
• -i Perform an interactive simulation, prompting the user at every execution step that requires a nondeterministic choice to be made. The simulation proceeds without user intervention when execution is deterministic.
• -jN Skip the first N steps of a random or guided simulation. (See also option -uN.)
• -l In combination with option -p, shows the current value of local variables of the process (see also -w).
• -M Produce a message sequence chart in Postscript form for a random simulation or a guided simulation (when combined with -t), for the model in file , and write the result into file.ps . See also option -c.
• -nN Set the seed for a random simulation to the integer value N. There is no space between the -n and the integer N. -p, shows the current value of local variables of the process.
• -p Shows at each simulation step which process changed state, and what source statement was executed.
• -qN In columnated output (option -c) and elsewhere, suppress the printing of output for send or receive operations on the channel numbered N.
• -r Shows all message-receive events, giving the name and number of the receiving process and the corresponding the source line number. For each message parameter, show the message type and the message channel number and name.
• -s Shows all message-send events.
• -T Suppress the default indentation of output from print statements. By default the output from process i is indented by i spaces. See also option -b.
• -t[N] Perform a guided simulation, following the error trail that was produces by an earlier verification run, see the online manuals for the details on verification. If an optional number is attached (no space between the number and the -t) the error trail with that sequence number is opened, instead of the default trail, without sequence number.
• -uN Stop a random or guided simulation after the first N steps. (See also option -jN.)
• -v Verbose mode, adds some more detail, and generates more hints and warnings about the model.
• -w Even more verbose output with options -l and -g (e.g., prints all variable values, not just those that change).

Introducere teoretica

http://spinroot.com/spin/Man/Manual.html
http://spinroot.com/spin/Man/promela.html
SPIN este o unelta pentru verificarea consistentei logice a sistemelor concurente, in special a protocoalelor de comunicatii de date. Descrierea sistemelor se face intr-un limbaj de modelare numit Promela (Process Meta Language). Limbajul permite crearea dinamica a proceselor concurente si comunicatia prin canale de mesaje sincrone sau asincrone.
Limbajul permite abstractizarea sistemelor modelate si eliminarea detaliilor care nu au legatura cu intractiile dintre procese. Pot fi specificate trei tipuri de obiecte:

• procese,
• canale de mesaje si
• variabile de stare.

Procesele sunt obiecte globale care definesc comportamentul sistemelor, in timp ce canalele de mesaje si variabilele descriu mediul in care functioneaza procesele.

Executabilitatea instructiunilor

in Promela nu exista nici o diferenta intre conditii si instructiuni. Chiar si conditii logice izolate pot fi utilizate ca instructiuni.
Executia unei instructiuni este conditionata de executabilitatea acesteia. De aceea, toate instructiunile Promela pot fi ori executabile, ori blocate, in functie de valorile curente ale variabilelor sau de continutul canalelor de mesaje.
Executabilitatea este mijlocul de baza pentru sincronizarea dintre procese. De exemplu, o bucla de asteptare in limbaj C:

while ( a != b) skip

este echivalenta cu instructiunea Promela

( a == b) 

Atata timp cat conditia nu este valida, aceasta va ramane in stare de blocare.

Tipuri de date

in Promela, variabilele sunt utilizate pentru stocarea informatiilor globale privind starea sistemului, sau local pentru informatii specifice proceselor. Exista sase tipuri predefinite de variabile:

	bit, bool, byte, short, int, chan

Primele cinci poarta denumirea de tipuri de baza. Al saselea este utilizat pentru specificarea canalelor de date, obiecte care pot stoca mai multe valori, grupate in structuri definite de utilizatori.
Declaratiile sunt de forma:

	bool fanion;
	int stare;
	byte mesaj;

Daca sunt declarate in afara definitiei proceselor, variabilele sunt globale.
in cadrul tabelului 3.1 sunt reprezentate principalele tipuri de date si domeniile de valori permise.

Nume	Dimensiune (biti)	Utilizare	Domeniu de valori
bit	1	fara semn	0 ÷ 1
bool	1	fara semn	0 ÷ 1
byte	8	fara semn	0 ÷ 255
short	16	cu semn	-215 ÷ 215-1
int	32	cu semn	-231 ÷ 231-1

Tipurile bit si bool sunt sinonime.

Variabilele pot fi definite si ca vectori. De exemplu,

	byte stare[N]

declara un vector de N octeti, care poate fi accesat prin instructiuni precum

	stare[1] = stare[0] - stare[2]

Domeniul de valori al indexului unui vector este 0 ÷ N-1.

Procese

Starile unor variabile sau canale de mesaje pot fi inspectate sau modificate de procese. Comportamentul unui proces poate fi definit prin intermediul declaratiei proctype, ca in exemplul urmator:

 proctype A(){
	byte stare;
	stare = 3
 }

Tipul de proces definit poarta numele A, declara o variabila locala stare pe care o initializeaza cu valoarea 3.
Caracterul ; este utilizat ca un separator (nu terminator) de instructiuni. Promela defineste doua tipuri de separatori: o sageata -> si caracterul punct si virgula ;. Separatorii sunt echivalenti, dar sageata poate fi utilizata pentru a indica o relatie cauzala intre doua instructiuni (conventie). Fie codul:

 byte stare = 2;
 proctype A(){
	(stare == 1) -> stare = 3
 }
 proctype B(){
	stare = stare - 1
 }

in cadrul exemplului de mai sus, sunt declarate doua procese de tipurile A si B. Procesul B contine o singura instructiune care decrementeaza valoarea variabilei de stare si este mereu executabil. Procesul A, in schimb, contine doua instructiuni separate de o sageata. Deoarece prima instructiune este o conditie, procesul A va fi blocat pana cand variabila de stare va avea o valoare corespunzatoare.

Executia proceselor

Directivele proctype specifica doar comportamentele proceselor, dar nu le si executa. Initial, un singur proces este executat, procesul init, care trebuie declarat explicit in fiecare specificatie in Promela. Cel mai simplu exemplu este:

 init { skip }

, unde skip este o instructiune nula.
Rolul procesului init este acela de a initializa variabilele globale si a pune in executie procese.
Operatia de instantiere a tipurilor proceselor se face cu ajutorul operatorului unar run, ca in exemplul urmator:

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

Operatorul run este mereu executabil (cu conditia ca tipul procesului sa poata fi instantiat) si intoarce o valoare pozitiva. Daca procesul nu poate fi instantiat, de exemplu daca nu exista suficiente resurse pentru crearea procesului, valoarea intoarsa va fi zero. Limbajul Promela nu defineste nici o limita pentru numarul de procese care poate fi instantiat, acesta depinzand de platforma de verificare utilizata. Numarul maxim de procese care pot fi active intr-un anumit moment, in SPIN, este limitat la 255.
Operatorul run poate fi utilizat si in cadrul definitiilor de procese. In aceasta situatie, procesul parinte nu-si va putea incheia executia decat dupa ce toate procesele instantiate de acesta si-au incheiat executiile.
Fiind un operator, run poate fi utilizat si pe post de conditie.
De asemenea, operatorul run permite pasarea de argumente catre procesele instantiate. Doar principalele tipuri de variabile (cele cinci de baza si tipul canal) pot fi oferite ca argumente pentru procese.

Cuvantul cheie active poate fi utilizat ca prefix in cadrul definitiilor tipurilor de procese, pentru a specifica necesitatea ca acestea sa fie active in starea initiala a sistemului. Prin intermediul acestui operator pot fi create instante multiple ale proceselor, ca si in cazul operatorului run, dar nu li se pot oferi argumente. De exemplu:

 active proctype A(int a) { ... }
 active [4] proctype B()  { ... }

Prima definitie implica realizarea unei singure instante a procesului A. Toate argumentele unui proces astfel instantiat vor fi initializate cu valoarea zero. Prin intermediul cuvantului cheie active pot fi create si instante multiple (4 in cazul procesului B din exemplu).

Secvente atomice

Executia in paralel a mai multor procese poate ridica numeroase probleme de sincronizare. Daca acestea sunt independente, dar au acces la o variabila comuna, rezultatul executiei poate fi unul imprevizibil.
Fie exemplul:

 byte stare = 1;
 proctype A() { (stare == 1) -> stare = stare + 1}
 proctype B() { (stare == 1) -> stare = stare - 1}
 init {run A(); run B();}

Simulatorul alege in mod pseudo-aleator ordinea de executie a segmentelor de cod nedeterminist, inclusiv a instructiunilor proceselor care ruleaza in paralel. Pe baza unor vectori de initializare identici, algoritmii pseudo-aleatori vor genera mereu aceleasi secvente de numere. In SPIN, vectorii de initializare sunt specificati de utilizator cu ajutorul unor numere intregi ( vezi seed din cadrul optiunilor simulatorului). Deoarece ambele procese modifica smultan aceeasi valoare, rezultatul operatiei poate fi 0, 1 sau 2, in functie de care procese trec de instructiunea conditionala si care nu. De asemenea, nu poate fi cunoscuta ordinea in care sunt executate operatiile de atribuire.
Aceasta problema poate fi partial remediata cu ajutorul secventelor atomice. O secventa se numeste atomica atunci cand toate instructiunile din cadrul sau pot fi executate fara intrerupere (se evita astfel intreteserea proceselor executate in paralel).
Exemplul anterior poate fi rescris astfel:

 byte stare = 1;
 proctype A() { atomic { (stare == 1) -> stare = stare + 1} }
 proctype B() { atomic { (stare == 1) -> stare = stare – 1} }
 init {run A(); run B();

Ca urmare a utilizarii secventelor atomice, unul singur dintre cele doua procese poate modifica valoarea starii, celalalt ramanand blocat. Rezultatul executiei va fi de aceasta data 0 sau 2, in functie de sectiunea atomica executata.
Doar prima instructiune dintr-o secventa atomica poate bloca, aceasta fiind si conditia ca procesele sa intre in sectiunile atomice.

Instructiuni de control al fluxului

in Promela este posibila si utilizarea instructiunilor de selectie, repetitie si salt neconditional.
Instructiunile de selectie vor fi de forma:

 if
 :: (a != b) -> optiunea1
 :: (a == b) -> optiunea2
 fi

in cadrul exemplului prezentat, sunt definite doua secvente de executie. O secventa poate fi selectata doar daca prima instructiune este executabila (poarta numele de garda). Nu este obligatoriu ca secventele de executie sa fie mutual exclusive. Daca sunt executabile mai multe secvente, va fi aleasa in mod aleator una dintre ele. Pe acest principiu al nedeterminismului se bazeaza de regula modelarea interactiunilor mediului inconjurator (sau factorului uman) cu sistemele verificate. In cadrul procesului de verificare sunt explorate toate secventele (caile de executie) posibile.
Atunci cand nici una din secvente nu este executabila, sectiunea de control se va bloca, pana cand o secventa devine executabila. In cazul in care nici o alta garda din cadrul selectiei nu este executabila, poate fi utilizat cuvantul cheie else, ca in exemplul:

 if
 :: (a > b) -> optiunea1
 :: (a < b) -> optiunea2
 :: else    -> optiunea3
 fi

Conditia else devine executabila doar daca toate celelalte conditii din cadrul structurii sunt false (pentru a==b in exemplul de mai sus).

Similar structurii conditionale, poate fi construita structura repetitiva, astfel:

 byte count;
 do
 :: count++
 :: count--
 :: (count == 0) -> break
 od

Iesirea dintr-o repetitie se poate face cu ajutorul instructiunii break. In exemplul precedent, repetitia se va termina eventual, deoarece chiar daca valoarea contorului va fi zero, va fi aleasa in mod aleator una dintre cele trei instructiuni executabile.
Ca o particularitate a verificatorului SPIN, nu este permisa validarea repetitiilor neconditionate, precum cea din exemplul precedent.

Definitia tipurilor de mesaje

in Promela este posibila utilizarea macro-definitiilor din cadrul limbajului de programare C. Astfel pot fi definite constante sau chiar functii de mici dimensiuni.
Ca alternativa la urmatoarele definitii:

 #define ack 	1
 #define nak 	2
 #define err 	3
 #define  ok 	4

, poate fi utilizata definitia:

  mtype = { ack, nak, err, ok }

Ca rezultat, sunt create aceleasi constante simbolice, avand exact aceleasi valori.
Este preferabila o definire formala a tipurilor mesajelor in locul uneia particulare, intarziind necesitatea luarii unor decizii in privinta valorilor acestora pana in momentul implementarii.

Canale de mesaje

Sintaxa definitiei canalelor de mesaje este urmatoarea:

 chan nume = [ const ] of { tip [, tip]* }

Poate fi creat astfel un canal cu numele nume si avand o capacitate de const mesaje. De asemenea, poate fi specificata structura mesajelor care urmeaza a fi transmise pe canal. Pot fi creati si vectori de canale.
De exemplu, prin definitia:

 chan q = [16] of {byte, int, chan}

se creaza un canal q care are un buffer de N = 16 mesaje, fiecare continand trei campuri: un octet, un intreg si un nume de canal.
Operatia de transmisie a mesajelor printr-un canal va fi de forma:

 q ! expr

, care transmite expresia expr pe canalul nou creat, in timp ce instructiunea

 q ? msg

va citi primul mesaj de pe canal si-l va stoca in variabila msg.
Canalele de mesaje sunt modelate ca liste de tipul FIFO: mesajele sunt extrase in aceeasi ordine in care au fost adaugate. Daca mesajele contin mai multe campuri, acestea vor fi specificate intr-o lista, separate prin virgula:

 q ! expr1, expr2, expr3
 q ? msg1,  msg2,  msg3

Daca sunt transmisi mai multi parametri decat ar putea fi stocati de canal, parametrii suplimentari vor fi eliminati. Similar se va intampla in cadrul receptiei: daca se citesc mai multe valori decat cele stocate pe canal, valorile in plus vor fi nedefinite, iar daca se citesc mai putine, valorile necitite se vor pierde.
Prin conventie, primul parametru al mesajelor poate fi considerat tip al mesajului, restul parametrilor fiind specificati intre paranteze, ca in exemplul:

 q ! expr1 (expr2, expr3)
 q ? msg1  (msg2,  msg3)

Operatiile de transmisie si receptie a mesajelor sunt executabile doar atunci cand canalul nu este plin, respectiv gol.
Optional, o parte din parametrii operatiei de citire pot fi constante. in acest caz, mai apare conditia de executabilitate ca toate campurile mesajelor specificate prin constante sa corespunda acestora. De exemplu instructiunea:

 q ? const1, var2, const3

va fi executabila daca expresiile 1 si 3 ale mesajului transmis sunt identice cu constrantele 1, respectiv 3.
Daca valoarea unui camp al mesajului nu este de interes si nu se doreste citirea acesteia, poate fi inlocuita cu _ . De exemplu, este de preferat a se utiliza instructiunea:

 q ? const1, var2, _

pentru operatia de citire, fiind o formulare mai corecta decat

 q ? const1, var2

Ambele instructiuni vor avea acelasi efect din punctul de vedere al executiei, dar in timpul procesului de validare se va considera ca ultimul camp al mesajului a fost omis in mod eronat in a doua instructiune.
Canalele pentru care dimensiunea buffer-ului este N > 0 permit comunicatia asincrona dintre procese. Totusi, este posibila sincronizarea proceselor si prin canale, atunci cand acestea au buffer-ul zero. In acest caz, operatiile de scriere vor fi executabile doar in momentul in care un alt proces doreste sa citeasca de pe canal.