Verificare formală - Proiect 2

Să se modeleze şi verifice în SMV un protocol care asigură consistenţa unei baze de date accesată de două calculatoare.

Sistemul e compus din 5 module: un manager unic pentru baza de date, iar pe fiecare din cele 2 calculatoare, un proces de interfaţă cu baza de date şi un program aplicaţie. Pe lângă execuţia altor instrucţiuni, o aplicaţie poate transmite procesului de interfaţă cereri de citire sau scriere de înregistrări din/în baza de date, şi aşteaptă până când aceste cereri pot fi satisfăcute.

Procesul de interfaţă are la dispoziţie un număr limitat de zone tampon pentru a păstra înregistrări în memorie. Fiecare zonă tampon e etichetată cu una din 3 valori posibile: consistent, dacă înregistrarea nu a fost modificată de la citirea din baza de date; modificat, în caz contrar; şi invalid dacă tamponul nu conţine o înregistrare. O cerere de scriere de la aplicaţie are ca efect doar modificarea înregistrării în tampon; scrierea în baza de date intervine doar atunci când este necesar (de exemplu când tamponul trebuie reutilizat pentru altă înregistrare).

Procesul de interfaţă poate emite spre managerul bazei de date 3 tipuri de cereri relativ la o înregistrare: citire, scriere şi invalidare. O cerere de invalidare este emisă ca efect al unei cereri de scriere din partea aplicaţiei, dacă ar exista posibilitatea ca sistemul celălalt să aibe în folosinţă o valoare veche a aceleiaşi înregistrări; în acest caz, protocolul trebuie să asigure invalidarea acesteia.

Pentru a realiza un model abstractizat şi simplificat al sistemului se va ţine seama de următoarele indicaţii. (Corectitudinea simplificărilor descrise se poate argumenta formal; pentru moment, le vom accepta ca atare.)

• Fiecare proces de interfaţă are la dispoziţie o singură zonă tampon.
• Baza de date conţine doar două înregistrări. (E suficientă modelarea unei înregistrări arbitrare, despre care dorim să raţionăm, şi a unei alte înregistrări care reprezintă ``orice altceva'').
• Înregistrarea are două valori posibile (suficient pentru a raţiona despre modificarea ei).

Celălalte detalii de modelare (dialogul între procesele de interfaţă şi manager, (a)sincronia dintre diversele module, etc.) se lasă la latitudinea proiectantului. Se recomandă ca managerul să servească nedeterminist, dar echitabil cererile celor două procese de interfaţă.

Sistemul va fi proiectat pentru a verifica următoarele proprietăţi:

1. Cele două programe nu pot avea niciodată valori inconsistente pentru aceeaşi înregistrare.
2. O locaţie tampon modificată îsi menţine înregistrarea până când aceasta este fie invalidată, fie scrisă în baza de date.
3. Executia niciunui program nu este blocată la infinit.