Model Checking în Specificațiile TLA

Model checking este o metodă de verificare care este:

• bazată pe modele, automată, verifică proprietăţi, folosită mai mult pentru sisteme concurente, reactive (iniţial a fost folosită în faza de post-dezvoltare).

Ce este o specificaţie?

O specificaţie este o descriere scrisă despre ce ar trebui un sistem sa facă. Este o idee buna sa înţelegem cum funcţionează un sistem, înainte de a-l construi, deci este oportun să scriem o specificaţie a sistemului înainte de a-l implementa.

Pentru a scrie o specificaţie este nevoie de mult efort. Scopul scrierii unei specificaţii este pentru a ajuta la prevenirea apariţiei erorilor. Aici avem unele soluţii care pot face acest lucru:

- scrierea unei specificaţii TLA+ poate ajuta la procesul designului. Descrierea un design precis, adesea ne va crea probleme. Aceste probleme sunt mai uşor de corectat când sunt descoperite în faza de design decât după ce s-a început implementarea propriu-zisă.

- o specificaţie TLA+ ne poate aduce un mijloc clar şi concis de comunicare a designului . Ne ajută sa fim siguri că designerii sunt de acord pe designul făcut şi oferă un ghid valoros inginerilor care vor implementa şi vor testa sistemul. De asemenea va ajuta şi utilizatorii să inţeleagă mai bine sistemul.

- o specificaţie TLA+ este o descripţie formală, pentru anumite unelte care pot fi aplicate pentru a ajuta la găsirea erorilor in design şi pentru a ajuta la testarea sistemului. Cea mai folositoare unealtă este TLC model checker (modelul de verificare TLC).

Prezentare generală TLA+

TLA – Temporal Logic of Actions

Logica temporală implică existenţa unei logici (la baza logicii temporale) care să manipuleze concepte matematice uzuale, formule „lungi” (cu care matematicienii nu sunt obisnuiţi) modularizarea specificaţiilor mari – legătura cu limbajele de programare TLA+ - util pentru specificarea unei clase largi de sisteme – de la interfeţe de program (API) la sisteme distribuite.

Specificarea unui sistem – îmbinarea unei baze matematice „consistente” existente cu câteva aspecte de logică temporală. TLA oferă o bază matematică pentru a descrie sisteme.

Probleme în specificarea "software" utilizând TLA+

Principala problemă ridicată de dezvoltatorii de programe este specificarea unui API (Aplication Programming Interface) în TLA+, problemă datorată în principal numărului mic de articole şi lucrări publicate conţinând exemple de astfel de specificaţii. O altă problemă întâlnită este cum poate fi utilizată o specificaţie API în specificarea unui sistem care apelează API-ul

Scrierea specificaţiilor

După ce am ales partea de sistem ce trebuie specificată si nivelul de abstractizare, suntem gata sa începem scrierea specificaţiei TLA+. Sa ne reamintim paşii de scriere a unei specificaţii TLA+: În primul rând vom alege variabilele şi vom defini tipul invariant şi predicatul initial. În timp ce facem acest lucru vom determina parametrul stabil. De asemenea trebuie să definim anumite constante adiţionale. Vom continua cu scrierea următoarei condiţii, care formează volumul specificaţiei. În primul rând trebuie să decidem cum să descompunem următoarea acţiune a condiţiei, ca o disjuncţie de acţiuni, ce descrie diferite lucruri în sistemul de operare. Apoi vom defini aceste acţiuni. Scopul este să facem o definiţie a acţiunii cât mai uşor de citit şi de înţeles. O posibilitate de a reduce mărimea specificaţiei este de a defini predicatele condiţiei şi funcţiile condiţiei, care sunt folosite în câteva acţiuni diferite ale definiţiei. Când scriem definiţia acţiunii, vom determina care dintre modulele standard vor fi necesare şi vom adăuga declaraţia extinsă. De asemenea va trebui să definim nişte operatori stabili pentru structurile de date pe care le folosim. Trebuie scrisă şi partea temporală a specificaţiei. În final putem declara teoremele specificaţiei şi probabil vom dori sa adăugăm introducerea datelor problemei.

În primul rând trebuie sa înţelegem ce înseamnă compunerea specificaţiilor. De obicei spunem că o formulă TLA specifică comportamentul corect al sistemului. Totuşi un comportament de fapt reprezintă o posibilă istorie a întregului univers nu doar a sistemului. Construcţia unui sistem care implementează specificaţia F înseamnă construirea universului, astfel încât F să fie satisfăcut. Compunerea a două sisteme a căror specificaţii sunt F şi G înseamnă facerea universului ce satisface atât F cât şi G, care este echivalent cu satisface F ^ G. Scrierea unei specificaţii ca o compunere a componentelor sale înseamnă scrierea specificaţiei ca o conjuncţie. În timp ce idea de bază este simplă, detaliile nu sunt întotdeauna evidente.

Specificarea unui ceas care afişează numai ora

O simplă modalitate de a introduce unele din notaţiile TLA+ este de a analiza comportamentul unui ceas, care este un dispozitiv ce indică orele de la 1 la 12. Pentru a simplifica specificaţia este ignorat timpul real şi de asemenea nu se specifică când ecranul se poate schimba.

Un comportament tipic al ceasului este o secvenţă

(1.1) [hr = 11] → [hr = 12] → [hr = 1] → [hr = 2] → …

unde hr este variabila care reprezintă ce afişează ceasul.

Cazul în care [hr = 11] este o stare în care variabila hr are valoarea 11. O pereche de stări succesive, cum ar fi [hr = 1] → [hr = 2] se numeşte un pas. Pentru a specifica ceasul oră, vom descrie toate comportamentele sale posibile. Avem nevoie de a specifica valoarea posibilă iniţială de hr, precum şi o relaţie next de stare care specifică modul în care valoarea hr se poate schimba în orice pas.

Noi nu vrem să se precizeze exact ceea ce a ecranului citeşte iniţial; orice oră va fi. Deci, ne dorim predicatul iniţial să se afirme că hr poate avea orice valoare de la 1 până la 12. Să numim HCini predicatul iniţial. Am putea defini în mod informal HCini astfel:

Următoarea relaţie HCnxt de stare este o formulă care exprimă relaţia dintre valorile hr în vechia stare (primul) şi noua stare (al doilea) de la un pas. hr reprezintă starea veche şi hr’ reprezintă valoarea sa în noua stare ( ‘ în hr’ este citit prim). În următoarea relaţie de stări se afirme că hr’ este egal cu hr + 1 excepţie cazul în care hr este egal cu 12, caz în care hr’ ar trebui să fie egal cu 1. Relaţia de stare HCnxt este următoarea:

O astfel de formulă se numeşte o acţiune. O acţiune este adevărată sau falsă la un pas. Un pas care satisface acţiunea HCnxt se numeşte un pas HCnxt. Când un pas HCnxt are loc, am spune că, uneori, HCnxt este executat. Cu toate acestea, ar fi o greşeală să profite de această terminologie în serios. O acţiune este o formulă, şi formule nu sunt executate. Noi vrem ca specificaţia noastră să fi o singură formulă, nu pereche de formule HCini şi HCnxt. Această formulă trebuie să afirme despre un comportament (i) starea sa iniţială satisface HCini, şi fiecare din (ii) satisface paşi HCnxt. Exprimăm (i) în formula HCini, pe care noi o interpretăm ca o declaraţie cu privire la comportamente ce înseamnă că îndeplineşte starea iniţială HCini. Pentru a exprima (ii), folosim operatorul temporal logic (pronunţat box).