Limbajul Promela. Logici Temporale

Introducere

Multe calculatoare sunt utilizate în domeniul sistemelor integrate, care sunt compuse de hardware, software, senzori, controlere si display-uri, şi care sunt destinate a fi folosite la nesfârşit şi fără supraveghere continuă. Trebuie doar să ne gîndim la avioane, monitoare medicale, precum şi reţelele de telefoane mobile pentru a aprecia complexitatea sistemelor integrate. Invariabil, aceste sisteme conţin mai multe procese care trebuie să probeze senzori şi să efectueze calculele aproximativ în acelaşi timp, de exemplu, un control medical probează monitorizarea ritmului cardiac, tensiunea arterială şi temperatura, şi stabileşte dacă acestea sunt într-un interval prestabilit. Programarea pentru sisteme de multiprocess este numită programare concurentă.

În mod frecvent, sistemele integrate conţin mai multe procesoare; microprocesoare au devenit atât de ieftine încât este posibil să se dedice un procesor separat pentru fiecare subsistem. În plus, multe sisteme precum reţelele de telefonie mobilă sunt, prin natură dispersate geografic, bazându-se pe reţele de comunicaţii pentru a transmite date între procesoare. Programarea pentru astfel de sisteme se numeşte programare distribuită.

SPIN susţine modelarea ambele sisteme: concurente şi distribuite. Această lucrare este referitoare la scrisul şi verificarea programelor concurente; utilizarea canalelor cu modelul sistemelor distribuite.

În capitolul I, intitulat “Programare segvenţială în Promela” se prezinta limbajul de modelare Promela. Capitolul II, intitulat „Logici temporale” abordează Logica temporală cu timp liniar (LTL), Computation Tree Logic - logica temporală cu timp ramificat (CTL) şi CTL* din punct de vedere semantic si sintactic.

Capitolul III intitulat „jSpin” prezintă programul şi modalitatea de aplicare a unor verificări cu ajutorul acestui program. Verificatorul jSPIN execută verificarea şi validarea modelului şi oferă utilizatorului rezultatele. Deşi este proiectat pentru verificarea modelelor şi sistemelor distribuite concurente, vom introduce verificarea elementară în cadrul programelor secvenţiale. Acest capitol arată cum să se exprime corectitudinea specificaţiilor folosind afirmaţii şi descrie procedura pentru efectuarea unei verificări în jSPIN. În Capitolul IV sunt prezentate programe reprezentative de implementare complexe. În anexă se prezintă configurarea fisierelor.

Capitolul I - Programare secvenţială în PROMELA

1. Fazele dezvoltării de produse software pentru sisteme mecatronice şi verificările lor: nevoia unui model checker

1.1. Sistem mecatronic

Un sistem mecatronic reprezintă un ansamblu de componente mecanice coordonate de componente electronice programate prin software, ce interacţionează între ele şi, acelaşi timp, ca tot unitar, interacţionează cu mediul în care este integrat.

Exemple de sisteme mecatronice pot fi văzute pretutindeni în jurul nostru: de la maşini de spălat şi automate de cafea - uzuale în peisajul lumii moderne, până la avioane, nave spaţiale sau dispozitive pentru realizarea de operaţii cu laser la distanţă ale căror funcţionare corectă şi performanţă sunt critice.

Din definiţia sistemelor mecatronice putem uşor observa faptul că programarea corectă şi verificarea corectitudini programelor ce dirijează activitatea acestor sisteme sunt chestiuni vitale.

Printre greşelile cele mai frecvente din designul sistemelor mecatronice se numără:

- deadlock-ul - blocajul sistemului - de exemplu, două componente aşteptă una de la alta un raspuns sau o acţiune

- livelock-ul - sistemul nu mai evoluează

- underspecification - subspecificarea - nu sunt prevăzute toate scenariile de folosire a sistemului şi există evenimente ale căror apariţie nu este tratată; apar astfel mesaje de eroare neaşteptate

- overspecification - supraspecificare - scrierea de "cod mort", care nu produce nimic

- violarea constrângerilor - de memorie, lăţime de bandă etc. - ce duc la depăşirea bufferelor alocate sau a limitelor unor vectori definiţi

- presupuneri ce ţin de viteza sistemului - un sistem poate fi total corect din punct de vedere al specificării sale logice, dar să nu ţină cont de performanţa în timp real, fapt critic mai ales în sistemele mecatronice folosite în medicină.

Majoritatea acestor greşeli pot fi însă detectate folosind tehnici de model checking. O verificare exhaustivă a tuturor posibilităţilor de comportament ale unui sistem este aproape imposibilă ( problema exploziei de stări).

Totul revine la următoarele întrebări: “Unde anume în ciclul dezvoltării de software este cel mai potrivit să facem model checking?”, “Cum se poate evita explozia de stări?” şi “Care este cel mai potrivit limbaj pentru model checking? Ce trebuie el să conţină?”

1.2. Modele pentru dezvoltarea de software - unde verificăm? Viziunea tradiţională şi cea modernă

În viziunea clasică a dezvoltării de proiecte - modelul cascadă - ce cuprinde fazele de:

- Analiză,

- Design,

- Implementare,

- Testare,

- Întreţinere

în mod tradiţional, model checking-ul se făcea în fazele de analiză, design şi implementare. Astfel, pornind de la analiza specificaţiilor se crea un model abstract, ce era apoi verificat şi rafinat prin model checking pentru ca implementarea sa să fie cât mai aproape de optim. Evident, şi aceasta era ulterior verificată prin model checking, dacă este conformă cu modelul său abstract, activitate ce ulterior era practic verificată în cadrul fazei de testare.

Viziunea modernă asupra model checking-ului plasează această activitate între faza de implementare şi cea de testare. Modelul abstract este construit, în această abordare, din implementarea însăşi - modelul implementat prin module de program în Java, C# etc. Se presupune că abstractizarea modelului din viziunea tradiţională între analiză şi implementare are loc implicit, prin nevoia de modularizare presupusă de limbajele de nivel înalt puternic modularizate care sunt folosite în prezent la crearea de software.