PROGRAMUL DE STUDII UNIVERSITARE DE LICENȚĂ: INFORMATICĂ [609172]

UNIVERSITATEA DIN PITE ȘTI
FACULTATEA DE Ș TIINȚE, EDUCAȚIE FIZICĂ ȘI
INFORMATIC Ă

PROGRAMUL DE STUDII UNIVERSITARE DE LICENȚĂ: INFORMATICĂ

LUCRARE DE LICENȚĂ

Coordonator științific,
Prof.univ .dr. Tudor BĂLĂNESCU

Absolvent: [anonimizat]
2019

UNIVERSITATEA DIN PITEȘTI
FACULTATEA DE ȘTIINȚE, EDUCAȚIE FIZICĂ ȘI
INFORMATICĂ

PROGRAMUL DE STUDII UNIVERSITARE DE LICENȚĂ: INFORMATICĂ

Verificarea modelelor
sistemelor de programme
(model checking)

Coordonator științific,
Prof.univ.dr. Tudor BĂLĂNESCU

Absolvent: [anonimizat]
2019

DECLARAȚIE

UNIVERSITATEA …………………………………………………………………………………………………………..
FACULTATEA ………………………………………………………………………………………………………………..
PROGRAMUL DE STUDII ………………………………………………………………………………………………
NUMELE ȘI PRENUMELE ………………………………………………………………………………………………
PROMOȚIA ……………………………………………………………………………………………………………………
SESIUNEA DE LICENȚĂ/DISERTAȚIE …………………………………………………………………………..
DENUMIREA LUCRĂRII DE LICENȚĂ/DISERTAȚIE …………………………………………………….
………………………………………………………………………………………………………………………………………..
………………………………………………………………………………………………………………………………………..

Prin prezenta declar că prezenta Lucrarea de licență/disertație este rezultatul m uncii proprii,
pe baza cercetărilor mele și pe baza informațiilor obținute din surse care au fost citate și indicate
conform regulilor de evitare a plagiatului:
− toate fragmentele de text reproduse exact, chiar și în traducere proprie din altă limbă, sunt
scrise între ghilimele și dețin referința precisă a sursei;
− reformularea în cuvinte proprii a textelor scrise de către alți autori deține referința precisă;
− rezumarea ideilor altor autori deține referința precisă la textul original.
Declar că nu s -a folosit în mod tacit sau ilegal munca altora și că nicio parte din prezentate
lucrare nu încalcă drepturile de proprietate intelectuală ale altcuiva, persoană fizică sau juridică.
Declar că lucrarea de licență/disertație nu a mai fost prezentată niciodată l a o altă facultate
sau instituție de învățământ superior din țară sau străinătate.
În cazul constatării ulterioare a unor declarții false, voi respecta rigorile legii.

PITEȘTI,
data
Absolvent: [anonimizat]
_______________________________
(semnătura în original)

Cuprins
Lista Figurilor ……………………………………………………………………………………………………………….. 5
Introducere ……………………………………………………………………………………………………………………. 6
I. Verificarea Sistemelor ………………………………………………………………………………………………… 8
Model Checking ……………………………………………………………………………………………………………… 8
Caracteristici ale Model Checking …………………………………………………………………………………… 10
II. Elemente de teorie …………………………………………………………………………………………………… 14
Sisteme de tranziție ………………………………………………………………………………………………………… 14
Proprietăți linear -temporale …………………………………………………………………………………………….. 16
III. Aplicație ………………………………………………………………………………………………………………… 26
UPPAAL ………………………………………………………………………………………………………………………. 26
Studiu de Caz ………………………………………………………………………………………………………………… 32
Concluzii ……………………………………………………………………………………………………………………… 39
Bibliografie ………………………………………………………………………………………………………………….. 40

Lista Figurilor
Figură 1: Reprezentare schematică a metodei model -checking ……………………………………… 9
Figură 2 – Interfața Applicației UPPAAL …………………………………………………………………. 26
Figură 3 – Exemplul becului ……………………………………………………………………………………. 27
Figură 5 – Obiectul „Mașină” ………………………………………………………………………………….. 33
Figură 6 – Obiectul „Stradă” …………………………………………………………………………………… 34
Figură 7 – Modelul în curs de simulare …………………………………………………………………….. 35
Figură 8 – Exemplu de executare a simulării …………………………………………………………….. 36
Figură 9 – Verificare deadlock ………………………………………………………………………………… 37
Figură 10 – Verificare suprapunere ………………………………………………………………………….. 37
Figură 11 – Verificarea lungimi străzii ……………………………………………………………………… 38

Vlad Rădulescu
6 Introducere
Lumea în care trăim se bazează din ce în ce mai mult pe sisteme informatice și de
comunicare, iar această dependență se află într -o creștere rapidă. Aceste sisteme devin din ce în
ce mai complexe și mai preponderente în viața de zi cu zi datorită internetului și a diferitelor
sisteme incorporate precum carduri inteligente, calculatoare portabile, telefoanele mobile,
televizoare și electrocasnice de performanță etc. În anul 1995 se estima că, în medie, o persoană
interacționează cu 25 astfel de sisteme în fiecare zi. Servicii bancare și cumpărături sunt
disponibi le online, aproximativ 1012 milioane de dolari se transferă prin intermediul internetului
zilnic, iar aproximativ 20% din costurile pentru dezvoltarea sistemelor de transport moderne sunt
dedicate sistemelor informatice.
Aceste sisteme sunt omniprezente și cruciale atât în domenii economice, de transport și
medicale, dar și din punct de vedere social. Pe lângă eficiența la care funcționează sistemele in
ceea ce privește timpurile de răspuns și capacitatea de a procesa informații, lipsa erorilor este
unul di ntre principalele semne ale calității. Astfel de erori pot avea efecte negative atât din punct
de vedere economic cât și de siguranță când vine vorba de sistemele care gestionează zborul avioanelor, uzine și centrale industriale, controlul traficului, sist eme de alertă etc.
Concluzia este că fiabilitatea sistemelor informatice este un aspect critic în procesul de
proiectare. Magnitudinea unui sistem crește în tandem cu complexitatea sa, iar acestea sunt
adeseori în comunicare cu alte sistem e și componente. Acest fapt crește probabilitatea apariției
erorilor. Fenomene esențiale ale modelării sistemelor care interacționează reciproc precum
concurența și nedeterminismul devin mult mai greu de aborda în acest context.
Tehnic i de verificare care intervin în proiectarea sistemelor informatice, pe scurt, se
utilizează pentru a asigura că un produs în proces de construcție îndeplinește anumit e proprietăți.
Aceste proprietăți pot fi relativ elementare, precum evitarea situațiilor de deadlock (sistemul nu
mai poate progresa), și provin în mare din specificația sistemului. Specificarea spune ce trebuie și ce nu trebuie să facă sistemul, astfel constituind o bază a activității de verificare. Dacă sistemul
nu îndeplinește una dintre cerințele specif icației, acesta este un defect, iar sistemul se consideră
corect în momentul în care îndeplinește toate cerințele obținute din specificație. De aceea se poate

Vlad Rădulescu
7 spune că corectitudinea se află în raport cu specificația, fiind relativă față de aceasta și nu o
propri etate absolută.
În cadrul acestei lucrări, voi aborda tehnica de verificare numită model checking
(verificarea modelelor), care pleacă de la o specificație formală. De menționat este că pe lângă
această metodă mai există și tehnici alternative, precum ver ificarea software (peer review) sau
verificarea hardware (emulare, simulare, analiză structurală ).
Primul capitol va fi alcătuit dintr -o prezentare a conceptului de model checking, în ceea ce
constă metoda de verificare bazată pe modele de sistem în mare, etapele ce trebuie parcurse în
realizarea unui model și avantajele și dezavantajele abordării model checking ca metodă de verificare a corectitudinii comportamentului unui sistem.
Al doilea capitol va prezenta în detaliu mai mult noțiunile teoretice ce intervin în domeniul
verificării bazate pe modele de sistem, definind mulți dintre termenii folosiți și explicând
concepte fundamentale legate de proiectarea și realizarea unui model de sistem și a enunțării
proprietăților de verificat în modelul respectiv.
Al treilea capitol va cuprinde o introducere a utilitarului UPPAAL, cuprinzând principalele
caracteristici ale acestuia, modul în care noțiunile teoretice sunt implementate practic și felul în
care se poate efectua proiectarea, simularea și validarea unui m odel, urmată apoi de un studiu de
caz reprezentat de un exemplu concret al unui model de sistem realizat în utilitarul UPPAAL ce demonstrează noțiunile prezentate anterior în legătură cu proiectarea modelelor de sistem și
verificarea proprietăților acestor a.

Vlad Rădulescu
8 I. Verificarea Sistemelor
Model Checking
Proiectarea sistemelor software și hardware complexe implică mai mult timp dedicat
verificării și testării decât a construcției sistemelor în sine. Metode formale de verificare oferă
posibilitatea integrării acesteia în procesul de proiectare din timp, de a fi mai eficiente și de a
reduce timpul necesar pentru verificare.
Metodele formale pot fi considerate partea de matematică aplicată a modelării și analizei
sistemelor informatice; scopul lor este de a doved i corectitudinea unui sistem cu rigurozitate
matematică.
În ultimii treizeci de ani, studiile realizate în domeniul metodelor formale au condus la
dezvoltarea unor tehnici ce facilitează detectarea timpurie a erorilor și a unor instrumente software care p ot automatiza anumiți pași din procesul de verificare.
Tehnicile de verificare bazate pe modele ( model -based) au la bază modele ce descriu
comportamentul unui sistem într -un mod precis din punct de vedere matematic și lipsit de
ambiguitate . Deseori se observă că modelarea corectă a unui sistem permite descoperirea unor
lipsuri , ambiguități și inconsistențe în specificarea informală a unui sistem până să se efe ctueze
orice fel de verificare. Modelele de sistem sunt însoțite de algoritmi care explorează în mo d
sistematic toate stările modelului, formând un temei pentru mai multe tehnici de verificare.
Mulțumită îmbunătățirilor algoritmilor și a structurilor de date ce stau la bază și a disponibilitatea
calculatoarelor mai rapide și cu mai multă memorie disponibilă, metodele bazate pe modele care
acum câțiva ani se puteau aplica numai unor exemple foarte simple pot acum fi folosite asupra
proiectelor plauzibile.
Având în vedere că punctul de pornire a acestor tehnici este un model al sistemului studiat,
este evi dent că orice verificare folosind metode bazate pe modele depinde calitativ de modelul
furnizat . Ca o metodă de verificare, model checking cercetează toate stadiile unui sistem prin
forță brută pentru a dovedi că un model al unui sistem într -adevăr satisfa ce o anume cerință.

Vlad Rădulescu
9 Proprietățile care pot fi verificate folosind model checking sunt de obicei calitative (Dacă
rezultatul generat este satisfăcător, dacă sistemul poate ajunge într -un stadiu de blocaj) dar pot fi
și de natură cronometrică (Dacă un blocaj poate să aibă loc într -o perioadă de timp, dacă un
răspuns este întotdeauna primit până într -un termen limită). Verificarea pe bază de model
necesită un enunț clar și neambiguu pentru a examina o proprietate.
Modelul sistemului este de obicei generat automat de către o descriere a modelului
precizată într -un limbaj de programare sau descriere hardware. Specificarea proprietăților
prescrie ce are trebui să facă sistemul, iar descrierea modelului precizează cum se comportă
acesta. Verificatorul testează toate stările relevante ale sistemului pentru a vedea dacă satisfac
proprietatea precizat ă, iar dacă se găsește o stare în care încalcă proprietatea se oferă un
contraexemplu (o cărare de execuție) care arată cum sistemul poate ajunge în starea nedorit ă. Cerințe Sistem
Specificarea
proprietății Model al
sistemului
Neîndeplinită +
contraexemplu Eroare de
locație Formalizare Modelare
Model Checking
Simulare Îndeplinită
Figură 1: Reprezentare schematică a metodei model -checking

Vlad Rădulescu
10 Caracteristici ale Model Checking
În aplicarea model checking unui proiect, se disting următoarele etape:
• Etapa de modelare:
o Sistemul de testat se modelează folosind limbajul de descriere a modelelor
respectiv;
o Se efectuează simulări pentru o evaluare inițială rapidă a modelului;
o Proprietatea de testat se formalizează folosind limbajul de specificare a
proprietăților.
• Etapa de rulare: Verificatorul de modele se rulează pentru a verifica validitatea
proprietății în m odelul sistemului.
• Etapa de analiză:
o Dacă proprietatea este îndeplinită, se trece la următoarea proprietate de
verificat, dacă există;
o Dacă este încălcată:
1. Contraexemplul generat se analizează prin simulare;
2. Modelul, planul sau proprietatea se corectează;
3. Procedura se repetă.
o Dacă capacitatea de memorie este depășită, se încearcă reducerea modelului și se reia analiza.
Modelele de sisteme descriu comportamentul sistemelor într -un mod precis și neambiguu.
De obicei se exprimă folosind automate cu număr finit de stări și un set de tranziții. Stările conțin
informații despre valorile curente ale variabilelor, ultima instrucțiune executată, etc. Tranzițiile descr iu cum sistemul trece dintr -o stare în alta . În scopuri practice, automatele finite sunt
exprimate cu ajutorul unui limbaj de descriere modele precum C, Java etc.
Pentru a îmbunătății un model, acesta poate fi simulat înaintea verificării sale. Simularea
poate elimina erorile de modelare mai simple, reducând costurile de memorie și timp ale
verificării.
În scopul unei verificări riguroase, proprietățile trebuie descrise cu precizie și fără
ambiguitate. Acest lucru se realizează de obicei cu un limbaj de specificare al proprietăților. În
mod special se urmărește folosirea logicii temporale c a limbaj de specificare a proprietăților. Din
punct de vedere al logicii matematice, se verifică dacă descrierea sistemului este un model al unei

Vlad Rădulescu
11 formule de logică temporală; de aici reiese denumirea de model checking. Logica temporală este
o extindere a l ogicii propoziționale cu operatori care fac referire la comportamentul unor sisteme
pe parcursul timpului. Aceasta face posibilă precizarea mai multor proprietăți relevante sistemelor precum corectitudinea funcțională (dacă sistemul efectuează cerințele pentru care a
fost proiectat), atenuabilitate (dacă este posibilă blocarea sistemului), siguranță (evitarea
consecințelor nedorite), vivacitate (dacă va avea loc ceva dorit la un moment dat), obiectivitate
(dacă un eveniment poate avea loc de mai multe ori î n diferite condiții) și proprietăți de timp real
(dacă sistemul acționează în timp).
Rularea verificatorului de modele se efectuează după inițializarea sa cu opțiunile și
directivele ce for fi utilizate pentru a realiza o testare completă. Verificarea modelului în sine este o abordare pur algoritmică prin care validitatea proprietății urmărite este verificată în toate stările
modelului sistemului.
În principiu, există trei rezultate posibile: proprietatea ori este validă în modelul furnizat,
ori nu, ori modelul este prea mare pentru a se încadra în limitele de memorie ale calculatorului.
Dacă proprietatea este validă se poate trece la următoarea proprietate de verificat dacă mai
există sau modelul poate fi considerat ca având toate proprietățile dorite.
Atun ci când o proprietate este invalidată, acest lucru poate fi datorat mai multor cauze. Este
posibilă existența unei erori de modelare , modelul fiind nereprezentativ față de sistem. În acest
caz, modelul trebuie corectat și verificarea reîncepută, inclusiv v erificarea acelor proprietăți care
au fost deja verificate în cadrul modelului eronat, deoarece este posibil ca corectarea modelului să
le fi invalidat. Dacă nu există discrepanțe între proiectarea sistemului și modelul său, este posibil
să se fi descoperi t o eroare de design sau să fi avut loc o eroare de proprietate . Dacă eroarea este
de design, verificarea s -a sfârșit cu un rezultat negativ iar sistemul împreună cu modelul său
trebuie îmbunătățite. Este de asemenea posibil ca proprietatea căutată nu reflectă cerința informală ce trebuie validată, implicând o modificare a proprietății și o nouă ve rificare a
modelului.
Atunci când modelul este prea mare pentru a fi verificat, există mai multe moduri de a
proceda. Una dintre acestea implică exploatarea regularităților implicite din structura modelului.
De asemenea se pot folosi abstractizări riguroas e ale modelului complet. Aceste abstractizări
trebuie să rețină validitatea sau nonvalidi tatea proprietăților de verificat. O altă metodă de a

Vlad Rădulescu
12 aborda spații de stări prea mari este de a sacrifica precizia rezultatului prin verificări
probabilistice.
Puncte le forte ale verificării bazate pe modele sunt:
• Este o abordare generală de verificare care se poate aplica unei game largi de
aplicații;
• Suportă verificare parțială, adică verificarea proprietăților individuală, permițând concentrarea asupra proprietățilo r cele mai esențiale.
• Furnizează informații diagnostice atunci când o proprietate nu este validată.
• Are potențialul de a fi folosită fără o mare implicare din partea utilizatorului sau de multă cunoștință tehnică.
• Se bucură de interes continuu din partea i ndustriei.
• Poate fi integrată cu ușurință în cicluri de dezvoltare preexistente.
• Are un fundament solid matematic.
Slăbiciunile verificării bazate pe modele sunt:
• Este mai adecvată aplicațiilor control intensive și mai puțin adecvată aplicațiilor
date inte nsive.
• Aplicabilitatea sa depinde de probleme de decidabilitate: verificare bazată pe modele în general nu se poate computa pentru sisteme cu stări infinite sau pentru a
argumenta be baza tipurilor de date abstracte.
• Verifică modelul unui sistem, nu sis temul în sine. Orice rezultat obținut depinde de
calitatea modelului. Sunt necesare tehnici complementare precum testarea pentru a găsi defecte de fabricare în hardware sau erori de cod în software.
• Verifică doar cerințele specificate, ne asigurând completitu dine. Nu se poate
exprima validitatea proprietăților care nu sunt verificate.
• Suferă de problema exploziei de stări: numărul de stări necesare modelării sistemului cu acuratețe poate depăși capacitatea de memorare a calculatorului. Deși există metode eficiente de a combate această problemă, modelarea sistemelor reale
încă impune probleme de memorie.

Vlad Rădulescu
13 • Utilizarea sa implică un grad de expertiză în găsirea abstractizărilor pentru a obține
modele de sistem mai mici și pentru a enunța proprietățile în domeniul formalismelor logice.
• Nu este garantată obținerea rezultatelor corecte. Ca orice instrument, verificatorul de modele poate conține defecte software.
• Nu permite verificarea generalizărilor. În general, verificarea sistemelor cu un număr arbitrar de componente sau a sistemelor parametrizate nu poate fi abordată.
În ciuda limitărilor menționate mai sus, se poate conclude că verificarea bazată pe modele
este o tehnică eficace pentru expunerea erorilor de proiectare și poate crește nivelul de încredere
în des ignul unui sistem.

Vlad Rădulescu
14 II. Elemente de teorie
Sisteme de tranziție
Sistemele de tranziție sunt adesea utilizate în domeniul informaticii ca modele pentru a
descrie comportamentul unor sisteme. Acestea sunt în esență grafuri orientate în care nodurile
reprezi ntă stări iar muchiile reprezintă tranziții sau schimbări de stare. O stare descrie informații
despre un sistem la un moment în timp cu referire la comportamentul acestuia. Ca un exemplu, starea unui semafor indică culoarea pe care acesta o afișează. În același fel, o stare unui program
secvențial indică valorile curente ale variabilelor de program împreună cu valoarea curentă a contorului programului care indică următoarea comandă de executat. Într -un circuit hardware
sincron, o stare reprezintă de obicei valoarea curentă a regiștriilor împreună cu valorile biților de
intrare. Tranzițiile specifică modul în care sistemul poat e evolua dintr -o stare în alta.
Noi folosim sisteme de tranziție cu nume de acțiuni pentru tranziții și propoziții atomice
pentru stăr i. Numele de acțiuni sunt folosite pentru a descrie mecanismele de comunicare între
procese și acțiunile sunt notate folosind alfabetul grecesc. Propozițiile atomice exprimă în mod intuitiv adevăruri cunoscute despre stările sistemului studiat. Acestea sun t notate cu litere din
alfabetul arab.
Un sistem de tranziție TS reprezintă un tuplu (S, Act
→ I, AP, L) unde
• S este o serie de stări;
• Act este o serie de acțiuni;
• →⊆ S × Act × S este o tranziție de relație;
• I ⊆ S este un set de stări inițiale
• AP este un set de propoziții atomice;
• L: S → 2AP este o funcție de etichetare.
TS se cheamă finit dacă S, Act și AP sunt finite.

Vlad Rădulescu
15 Comportamentul intuitiv al unui sistem de tranziție poate fi descris în felul următor:
Sistemul începe într -o stare inițială s 0 ∈ I și e voluează conform relației de tranziție →. Deci, dacă
s este starea curentă, o tran ziție 𝑠𝛼→𝑠′ cu originea în s este selectată nedeterminist și luată;
acțiunea α este efectuată și sistemul de tranziție evoluează din starea s în starea s '. Această
procedură de selecție se repetă în starea s' și se termină odată ce se găsește o stare care nu are
tranziții de ieșire. De reținut este că dacă o stare are mai multe tranziții de ieșire, tranziția
următoare es te aleasă în mod nedeterminist, deci rezultatul procesului de selecție nu este
cunoscut apriori.
Funcția de etichetare L corespunde un set de propoziții atom ice 𝐿 (𝑠)∈2𝑎𝑝 oricărei stări s.
L(s) reprezintă în mod intuitiv chiar acel e propoziții 𝑎 ∈𝐴𝑃 care sunt satisfăcute de către starea
s. Φ fiind o formulă de logică propozițională, s satisface formula Φ dacă evaluarea indusă de
către L(s) face ca formula Φ să fie adevărată.
𝑠 |=Φ if L(s) |=Φ
Un rol crucial în modelarea sistemelor hardware sau software de tranziție îl joacă
nedeterminismul. Alegeri nedeterministe au rolul de a modela execuția în paralel a unor activități
independente prin interfoliere și de a modela situațiile de conflict care apar. Interfolierea
înseamnă alegerea nedeterministă a ordinii în care acțiunile unui proces care rulează în paralel sunt executate. Pe lângă paralelism, nedeterminismul mai este important pentru abstractizare,
subspecificare, și pentru a modela interfețe cu un mediu necunoscut sau nepre vizibil.
23

Vlad Rădulescu
16 Proprietăți linear- temporale
În scopul verificării, modelul sistemului de tranziție studiat trebuie să fie acompaniat de
către o specificare a proprietății urmărite spre a fi verificată.
Programele secvențiale care nu sunt supuse divergenței au o stare terminală, care nu are
tranziții de ieșire. Pentru sisteme paralele însă operațiile de calcul de obicei nu se termină. Pentru
astfel de sisteme, stări terminale nu sunt urmărite și se consideră o eroare de proiectare.
Exceptând erori triviale de proiectare, în care nu s -au precizat anumite activități, aceste stări
terminale de obicei reprezintă un blocaj (deadlock). Un blocaj are loc atunci când sistemul complet se află într -un stadiu terminal, însă cel puțin o com ponentă se află într -un stadiu local
neterminal. Așadar, sistemul întreg se oprește în timp ce o componentă are posibilitatea de a opera în continuare. În mod tipic, scenariile de deadlock au loc atunci când componente se
așteaptă una pe cealaltă să progreseze.
Pentru a analiza un sistem informatic reprezentat printr -un sistem de tranziție, poate fi
urmărită fie o abordare bazată pe acțiuni fie o abordare bazată pe stări. Abordarea bazată pe stări
abstractizează acțiunile, luând în considerare doar etichetele din secvența de stări. Abordarea
bazată pe acțiuni abstractizează stările și face referire doar la etichetele de acțiune ale tranzițiilor.
Se poate de asemenea considera o abordare combinată bazată atât pe acțiuni cât și pe stări, însă
conduce la defini ții și concepte mai detaliate și de aceea se preferă în majoritatea cazurilor să se
abstractizeze fie etichetele de acțiune fie cele de stări. Majoritatea formalismelor de specificare și metode de verificare asociate pot fi formulate corespunzător din ambe le puncte de vedere.
Graful de stare a unui sistem de tranziție TS are un nod pentru fiecare stare din TS și o
muchie între nodurile s și s ' de fiecare dată când s' este un succesor direct al lui s în TS pentru o
acțiune α. Se obține astfel din TS omițând toate etichetele de stare (propozițiile atomice),
etichetele de tranziție (acțiunile) și ne luând în seamă dacă o stare este inițială sau nu. De asemenea, mai multe tranziții cu etichete de acțiune diferite între stări sunt reprezentate de o
singură muchie .
O execuție reprezintă o secvență alternantă alcătuită din stări și acțiuni. Acțiunile sunt
folosite în principal pentru a modela posibilitatea interacțiunii, fie prin comunicare sincronă sau
asincronă. Interacțiunea însă nu este de interes principal, ci în schimb ne vom axa pe stările
vizitate în timpul execuțiilor. Stările în sine nu sunt „observabile”, ci doar propozițiile lor atomice.

Vlad Rădulescu
17 Așadar, în locul unei execuții de forma 𝑠0𝛼0��𝑠1𝛼1��𝑠2… vom considera secvențele de forma
𝐿(𝑠0)𝐿(𝑠1)𝐿(𝑠2…) care înre gistrează setul proprietăților atomice valide pe parcursul execuției.
Aceste secvențe se numesc urme.
Proprietățile linear temporale specifică ce urme un sistem de tranziție trebuie să prezinte.
Informal, se poate spune că o proprietate linear temporală pr ecizează comportamentul permis sau
dorit al sistemului luat în considerare
Se va considera un set fix de propoziții AP. O proprietate linear temporală (LT) reprezintă o
cerință asupra urmei sistemului de tranziție. O astfel de proprietate poate fi înțeleas ă ca o cerință
asupra tuturor cuvintelor supra AP, și se definește ca setul cuvintelor peste AP admisibile.
O proprietate linear temporală (proprietate LT) peste un set de propoziții atomice AP este
un subset al ( 2𝐴𝑃)𝜔.
Aici, ( 2𝐴𝑃)𝜔 denotă setul cuvintelor ce reies din concatenarea infinită a cuvintelor din 2AP.
O proprietate liniar temporală este așadar un limbaj de cuvenite infinite peste alfabetul 2AP. De
notat este că este de ajuns să fie considerate doar cuvintele infinite și nu cele finite, deoarece
sistemele de tranziție fără stări terminale sunt considerate. Îndeplinirea unei proprietăți linear
temporale de către un sistem de tranziție se definește în felul următor:
F i e P o p r o p r i e t a t e l i n e a r t e m p o r a l ă p e s t e A P ș i T S = ( S , A c t , →, AP, L) un sistem de
tranziție fără stări terminale. Așadar, TS = (S, Act, →, AP, L) satisface P, notat TS |= P, dacă
Urme(TS) ⊆ P. Starea 𝑠 ∈𝑆 𝑠𝑎𝑡𝑖𝑠𝑓𝑎𝑐𝑒 𝑃, notat s |= P, atunci când Urme(s) ⊆ P.
Așadar, un sistem de tranziție satisface pro prietatea linear temporală P dacă toate urmele
sale respectă P, adică dacă toate comportamentele sale sunt admisibile. O stare satisface P atunci când toate urmele care încep din acea stare îndeplinesc P.
Proprietățile de siguranță sunt deseori caracterizate prin idea de „să nu se întâmple nimic
rău”. Proprietatea de excluziune reciprocă, adică cel mult un proces se află în secțiunea sa critică
la orice moment, este o proprietate de siguranță tipică. Această enunță că lucrul nedorit, și anume
să existe două sau mai multe procese în secțiunea lor critică, nu are loc niciodată. O altă
proprietate de siguranță tipică este lipsa deadlockurilor.

Vlad Rădulescu
18 Proprietățile de siguranță exemplificate mai sus sunt de fapt de un tip special și se numesc
invarianți. Invarianții sunt acele proprietăți linear temporale care sunt date de o condiți e Φ pentru
stări și mențin ca Φ să fie adevărată pentru toate stă rile care se pot atinge.
O proprietate linear temporală P inv peste AP este un invariant dacă există o formulă de
logică propozițională Φ peste AP astfel încât:
𝑃𝑖𝑛𝑣=�𝐴0𝐴1𝐴2… ∈(2𝐴𝑃)𝜔�∀ 𝑗 ≥0.𝐴𝑗 |=Φ �
Φ se numește condiție invariant a lui P inv.
Condiția Φ trebuie să fie îndeplinită de către toate stadiile inițiale iar satisfacerea lui Φ nu
variază cu tranzițiile din fragmentul atenuabil al sistemului de tranziție dat. Așadar, dacă Φ este
îndeplinită de pentru starea sursă s a tranziției 𝑠𝛼→𝑠′, atunci Φ este îndeplinită și pentru starea
țintă s'.
În mod informal putem spune că proprietățile de siguranță asigură că „ceva rău nu se
întâmplă”, de exemplu în algoritmul de excluziune reciprocă existența a două procese în
secțiunea critică sau în cazul unui semafor atunci când indicarea luminii roșii nu este precedată de
indicarea luminii galbene. Un algoritm poate îndeplini cu ușurință o proprietate de siguranță pur
și simplu ne făcând nimic, deoarece în acest fel nu se va putea ajunge niciodată la o s ituație
nedorită. Deoarece acest comportament este de obicei nedorit, proprietățile de siguranță trebuie
să fie complementate de proprietăți care cer să se efectueze un anume progres. Aceste proprietăți
se numesc proprietăți de vivacitate sau de progres În mod intuitiv, acestea enunță condiția că
„ceva bun” se va efectua pe viitor. În timp ce proprietățile de siguranță sunt încălcate în timp finit,
adică în derularea unui sistem finită, proprietățile de vivacitate sunt încălcate în timp infinit, adică
de către derulări de sistem infinite.
Sunt definite mai multe noțiuni neechivalente de proprietăți de vivacitate. În acest caz vom
urmări abordarea lui Alpern și Schneider [ 121]. Aceștia au creat o noțiune formală a
proprietăților de vivacitate care se bazează pe concepția că proprietățile de vivacitate nu
constrâng comportamentele finite, ci necesită o anumită condiție pe comportamentele infinite. Un
exemplu tipic de o proprieta te de vivacitate este cerința ca anumite evenimente să aibă loc infinit
de des. În acest sen, evenimentul dorit al unei proprietăți de vivacitate este condiția pe

Vlad Rădulescu
19 comportamentele infinite, în timp ce evenimentul nedorit al unei proprietăți de siguranță , dacă are
loc, are loc în tr-un timp finit.
Un aspect important al sistemelor reactive este obiectivitatea. Presupuneri despre
obiectivitate elimină comportamente infinite care sunt considerate nerealiste, și sunt adesea
necesare pentru a stabili proprietăți de vivacitate. Conceptul de obiectivitate poate fi ilustrat
printr -o problemă deseori întâlnită în sisteme concurente.
Se consideră N procese P 1, …, P N care necesită un anume serviciu. Există un proces Server
de la care se așteaptă să se ofere servicii ac estor procese. Una dintre strategiile pe care Server o
poate realiza este următoarea: se verifică procesele începând cu P 1, apoi P 2 și așa mai departe, și
se servește primul proces astfel întâlnit care necesită serviciul. După ce procesul este servit,
procedura de selecție se repetă din nou cu verificarea lui P 1.Însă, dacă presupunem că P 1 cere
serviciul în permanență, strategia enunțată va însemna că Server servește pe P 1 în continuu.
Deoarece așadar un alt proces are de așteptat la nesfârșit să fie servit , se consideră că o astfel de
strategie nu este obiectivă. O strategie obiectivă are însemna ca Server va răspunde la un moment
dat la orice cerere din partea oricărui proces.
În cadrul verificării sistemelor concurente, adeseori suntem interesați doar de cărările în
care tranzițiile permise sunt executate într -o manieră obiectivă.
Pentru a obține o imagine realistă a comportamentului unui sistem paralel modelat de către
un sistem de tranziție este nevoie de o formă mai atenuată a relației de satisfacere pentru proprietăți linear temporale, care implică o rezolvare adecvată a deciziilor nedeterministe în
cadrul unui sistem de tranziție. Pentru a elimina calcule nerealiste, se impun constrângeri de
obiectivitate.
În general, o execuție sau urmă obiectivă este caracterizată de faptul că anumite
constrângeri de obiectivitate sunt îndeplinite. Constrângerile de obiectivitate sunt folosite pentru
a anula calcule care se consideră nerezonabile pentru sistemul luat în considerare. Aceste
constrângeri de obiectivitate pot fi de mai multe feluri:
• Obiectivitate necondițională – Fiecare proces își primește rândul infinit de des.
• Obiectivate puternică – Fiecare proces care este activat infinit de des își primește
rândul infinit de des.

Vlad Rădulescu
20 • Obiectivitate slabă – Fiecare proces care este activat continuu de la un anumit
moment de timp încolo își primește rândul infinit de des.
În acest context, termenul de „activat” poate fi înțeles ca noțiunea de a fi gata de a executa
o tranziție. Asemănător, „a -și primi rândul” înseamnă execuția unei tranziții arbitrare. Aceasta
poate fi, de exemplu, o acțiune noncritică, achiziționarea unei resurse comune, o acțiune în
secțiunea critică, sau o acțiune de comunicare.
Un fragment de execuție este obiectiv necondiționat față de o proprietate dacă acea
proprietatea este adevărată infinit de des. Este de remarcat faptul că nu se precizează nici o
condiție care să constrângă circumstanțele în care un proces își primește rândul infinit de des.
Obiectivitatea necondiționată se mai numește și imparțialitate.
Obiectivitate puternică înseamnă că dacă o activitate este activate infinit de des, dar nu
neapărat mereu (fiind o posibilitate să existe perioade finite în care activitatea nu este activată), atunci aceasta va fi executată infinit de des. Un fragment de execuție este obiectiv robust față de
o activitate α dacă nu este adevărat că α este activată infinit de des fără să fie trecută de un anumit
punct. Obiectivitatea robustă se mai numește și compasiune.
Obiectivitate slabă înseamnă că dacă o act ivitate, adică o tranziție într -un proces sau un
întreg proces în sine, este activată continuu, adică nu se permit perioade în care activitatea nu este
activă, atunci aceasta trebuie să fie executate infinit de des. Un fragment de execuție este slab obiect iv față de o activitate α dacă nu este adevărat că α este mereu activă după un anumit punct
fără să fie trecută de acel punct. Obiectivitate slabă se mai numește și justiție.
Constrângeri de obiectivitate se pot formula în mai multe feluri. Fie un set de a cțiuni A.
Fragmentul de execuție ρ este A -obiectiv necondiționat dacă o acțiune în A este executată infinit
de des în ρ.
Pentru a formula aceste noțiuni de obiectivitate în mod formal, este utilă următoarea
noțiune auxiliară. Pentru starea s, fie Act(s) se tul de acțiuni care sunt executabile în starea s:
𝐴𝑐𝑡(𝑠)={𝛼 ∈𝐴𝑐𝑡 | ∃ 𝑠
′∈𝑆.𝑠 𝛼→ 𝑠′}

Vlad Rădulescu
21 Ca un exemplu, putem lua în considerare două procese care rulează în paralel și au acces
comun la o variabilă întreagă x, inițializată cu valoarea 0:
𝑝𝑟𝑜𝑐 𝐼𝑛𝑐 =𝑤ℎ𝑖𝑙𝑒 (𝑥 ≥ 0 𝑑𝑜 𝑥≔𝑥+1) 𝑜𝑑
𝑝𝑟𝑜𝑐 𝑅𝑒𝑠𝑒𝑡 =𝑥≔ −1
Între paranteze este încadrată o secție atomică, adică procesul Inc efectuează o verificare
dacă x este pozitiv și incrementează valoarea lui x (dacă condiția este îndeplinită) î ntr-un singur
pas atomic. Dacă punem întrebarea terminării programului, putem observa că dacă nu se impun
constrângeri de obiectivitate, este posibil ca procesul Inc să se execute în permanență, iar
procesul Reset să nu își primească niciodată rândul, deci atribuirea x = – 1 nu va avea loc. În acest
caz, nu se poate garanta terminarea programului, și proprietatea este încălcată. Însă, dacă cerem obiectivate necondițională a proceselor, atunci fiecare proces își primește rândul și astfel se
asigură terminarea.
O considerare importantă asupra unei probleme de verificare este care dintre noțiunile de
obiectivitate va fi aleasă. Din nefericire, nu există un răspuns evident la această întrebare. Există
și alte formele de obiectivitate pe lângă cele prezentate anterior, acestea reprezentând doar un
fragment mărunt dar important al totalității noțiunilor de obiectivate care există. Dintre toate
variantele posibile, nu există o noțiune care se poate numi preferabilă peste toate celelalte pentru
toate situațiile. În sc opurile verificării, constrângeri de obiectivitate sunt însă esențiale. Ne
amintim că scopul constrângerilor de obiectivitate este a elimina anumite computații nerezonabile. Dacă constrângerea este prea puternică, computații relevante ar putea fi neluate î n
considerare. Dacă o proprietate este satisfăcută pentru un sistem de tranziție, este posibil ca o computație perfect rezonabilă dar ignorată deoarece a fost eliminată de către constrângerea de
obiectivitate să refută acea proprietate. Pe de altă parte, d acă constrângerea este prea slabă, este
posibil să se împiedice dovedirea unei proprietăți datorită unei computații nerezonabile care nu a fost eliminată din considerare și care o refută.
Relațiile dintre noțiunile de obiectivitate diferite este următoarea :
𝑂𝑏𝑖𝑒𝑐𝑡𝑖𝑣𝑖𝑡𝑎𝑡𝑒 𝐴 𝑛𝑒𝑐𝑜𝑛𝑑𝑖ț𝑖𝑜𝑛𝑎𝑙ă⇒ 𝑂𝑏𝑖𝑒𝑐𝑡𝑖𝑣𝑖𝑡𝑎𝑡𝑒 𝐴 𝑝𝑢𝑡𝑒𝑟𝑛𝑖𝑐 ă ⇒ 𝑂𝑏𝑖𝑒𝑐𝑡𝑖𝑣𝑎𝑡𝑒 𝐴 𝑠𝑙𝑎𝑏ă

Vlad Rădulescu
22 Altfel spus, orice fragment de execuție necondiționat A -obiectiv este de asemenea A –
puternic, iar fiecare fragment de execuție puternic A -obiectiv este slab A -obiectiv. În general,
reciproca nu este adevărată. De exemplu, un fragment de execuție care vizitează doar stările în
care nici o A -acțiune este posibile este puternic A -obiectiv , deoarece premiza A -obiectivității
puternice nu este îndeplinită, dar nu este A -obiectiv necondițional. De asemenea, un fragment de
execuție care vizitează un număr finit de stări în care unele A -acțiune sunt active dar nu execută o
A-acțiune este A -obiectiv slab, deoarece premiza A -obiectivității slabe nu este îndeplinită, dar nu
A-obiectiv puternică.

Vlad Rădulescu
23 Automate Temporale
Multe sisteme reactive precum protocoale de comunicație, bancomate etc. au nevoie să
reacționeze într -un interval de timp – fiind numite temporal critice. Comportamentul acestor
sisteme temporal- critice este adesea supus unor constrângeri de timp stringente. Pentru o trecere
cu o cale ferată, este esențial ca la detectare a unui tren care se aproprie să se coboare bariera într –
un anume interval de timp pentru a opri traficul rutier înainte ca trenul să ajungă la trecere.
Pe scurt, corectitudinea în sisteme temporal critice nu depinde doar de rezultatul logic al
calculelor, dar și de timpul în care sunt produse rezultate.
Deoarece acționarea în timp este de importanță vitală sistemelor reactive, este esențial
constrângerile de timp ale sistemului să fie îndeplinite. Pentru a exprima astfel de constrângeri, se
vor extinde formalismele logice care permit exprimarea ordinii evenimentelor cu o noțiune de
timp cantitativ. Cu astfel de extinderi se permite formularea constrângerilor temporale de forma
„Semaforul va indica culoarea verde în următoarele 30 de secunde.”
Prima alege re care trebuie făcută este dacă domeniul temporal este discret sau continuu. Un
domeniu temporal discret este simplu din punct de vedere conceptual. Se folosesc sisteme de tranziție pentru a modela sisteme cronometrate unde se presupune că fiecare acțiune durează o
singură unitate de timp. Amânări mai generale se pot modela folosind o acțiune dedicată
neobservabilă τ (tick). O acțiune α care durează k > 1 unități de timp poate fi modelată sub forma
k-1 acțiuni tick urmate sau precedate de α. Această abordare de obicei conduce la sisteme de
tranziție foarte mari. Pentru sisteme sincrone, unde procesele se derulează în șir , domenii de timp
discrete sunt convenabile, fiecare unitate de timp corespunzând unui puls de cronometru.
Ca un formalism pentru modelarea sistemelor temporal critice a fost dezvoltată noțiunea de
automat temporal ca o extensie a sistemelor de tranziție cu variabile cronometru ce măsoară scurgerea timpului. Acest model include metode pentru a impune constrângeri pe temporizarea
acțiunilor.
Un automat temporal este de fapt un graf program echipat cu un set finit de variabile
cronometru de valori reale, numite cronometre. Cronometrele se diferențiază de variabilele obișnuite prin faptul că accesul la ele este limitat. Acestea pot fi doar inspec tate și resetate la zero.

Vlad Rădulescu
24 Cronometrele pot fi resetate la zero urmând ca apoi să își incrementeze valoarea implicit
cu demersul timpului. Toate cronometrele avansează cu o rată de unu, adică după scurgerea a d
unități de timp, toate cronometrele avansea ză cu d. Așadar, valoarea unui cronometru denotă cât
timp s -a scurs de la ultima sa resetare.
Condiții asupra va lorilor acestor cronometre pot fi folosite sub formă de condiții de
activare (guards) ale acțiunilor: acțiunea este activă și poate fi luată nu mai dacă condiția este
îndeplinită, iar în caz contrar, acțiunea este dezactivată. Astfel de constrângeri de cronometru mai
pot fi folosite pentru a limita timpul care poate fi petrecut într -o locație.
O constrângere de cronometru asupra unui set C de cronometre se formează conform
gramaticii
𝑔∷= 𝑥<𝑐 𝑥≤𝑐 𝑥>𝑐 𝑥≥𝑐 𝑔 ^ 𝑔
unde c ∈ ℕ și x ∈ C. Fie CC(C) setul de constrângeri de cronometru peste C.
Constrângeri de cronometru care nu conțin conjuncții sunt atomice. Fie ACC(C) setul
tuturor constrângerilor de cronometru atomice peste C.
În mod intuitive, un automat temporal este un graf de program modificat, ale cărui variabile
sunt cronometre. Cronometrele sunt folosite pentru a formula presupunerile de timp real asupra comportamentului sistemului. O muchie într -un automat temporal este etichetată cu un guard,
care indică când poate lua o muchie, o acțiune, care indică ce se petrece când muchia este luată, și un set de cronometre, cele care sunt de resetat. O locație estre înzestrată cu un in variant care
constrânge cantitatea de timp care poate fi petrecută în acea locație. Definit formal, un automat
temporal este un tuplu TA = (Loc, Act, C →, Loc
0, Inv, AP, L), unde:
• Loc este un set finit de locații;
• Loc 0 ⊆ Loc este un set de locații inițiale ;
• Act este un set finit de acțiuni;
• C este un set finit de cronometre;
• →⊆ Loc × CC(C) × Act × 2C × Loc este o relație de tranziție;
• Inv : Loc → CC(C) este o funcție de atribuire de invarianți;
• AP este un set finit de propoziții atomice;

Vlad Rădulescu
25 • L : Loc → 2AP este funcția de etichetare a locațiilor.
ACC(TA) denotă setul de constrângeri de cronometru atomice care pot avea loc fie într -un
guard fie intr -un invariant de locație al TA.
Un automat temporal este un graf de program cu un set de cronometre finit C. Muchiile
sunt etichetate cu tupluri (g, α, D) unde g este o constrângere pe cronometrele automatului
temporal, α este o acțiune iar D ⊆ C este un set de cronometre. Interpretarea intuitivă a 𝑙𝑔:𝛼,𝐷�⎯⎯�𝑙′
este că automatul temporal poate să se mute din locația l în locația l' atunci când constrângerea de
cronometru g este validă. Mai mult, când se mută din locația l în locația l ', orice cronometru din
D va fi resetat la zero iar acțiunea α efectuată. Funcția Inv conferă fiecărei locații un invariant de
locație care precizează cât timp automatul temporal poate rămâne acolo. Pentru locația l, Inv(l)
aplică o constrângere asupra cât timp poate fi petrecut în l. Cu alte cuvinte, locația l ar trebui să
fie părăsită până c a invariantul Inv(l) să devină invalid. Dacă acest lucru nu se poate face,
deoarece nu există nici -o tranziție de ieșire activă, nu se poate progresa mai departe. În semantica
formală a automatelor temporale, această situație face ca derularea timpului să înceteze. Deoarece
timpul nu mai poate progresa, această situație este cunoscută și sub numele de timelock.
682 that parallel junk

Vlad Rădulescu
26 III. Aplicație
UPPAAL
UPPAAL reprezintă un set de instrumente pentru verificarea sistemelor de timp -real
dezvoltat în colaborare de către Universitatea Uppsala și Universitatea Aalborg. Acesta a fost
folosit cu succes în studii de caz cuprinzând protocoale de comunicație și apl icații multimedia,
printre multe altele. Programul este creat pentru a verifica sisteme care pot fi modelate ca rețele
de automate temporale extinse cu variabile întregi, tipuri de date structurate, funcții definite de
utilizator și sincronizări de canale.
Prima versiune de UPPAAL a fost lansată în 1995, cu dezvoltate continuă până în prezent.
Programul dispune de o interfață Java și un motor de verificare scris în C++. Programul este
disponibil gratuit pe https://www.uppaal.com/ .
Figură 2 – Interfața Applicației UPPAAL

Vlad Rădulescu
27 Verificatorul de modele UPPAAL este bazat pe teoria automatelor temporale, iar limbajul
său de modelare oferă caracteristici adiționale precum variabile întregi mărginite și urgență.
Limbajul de interogare folosit de UPPAAL pentru a specifica proprietăți de a fi verificate este un
subset al TCTL (timed computation tree logic).
Un automat temporal este o mașină cu număr finit de stări extins cu variabile cronometru
care progresează sincron. În UPPAAL, un sistem este modelat ca o rețea de astfel de automate temporale în paralel. Modelul este extins mai departe cu variabile discrete mărginite care fac
parte din stare. Aceste variabile se folosesc precum în limbajele de programare: sunt citite, scrise
și se pot efectua operații aritmetice asupra lor. O stare a sistemului este definită de locațiile
tuturor automatelor, valorile cronometru, și valorile variabilelor discrete. Fiecare automat poate
lansa o muchie (tranziție) individual sau sincronizat cu alt automat, care conduce la o stare nouă.
Figura de mai jos reprezintă modelarea automat -temporală a unui bec simplu. Becul are trei
poziții: oprit, slab și puternic. Dacă utilizatorul apasă un buton, sincronizând cu „apasă?”, atunci
becul se aprinde. Dacă utilizatorul apasă butonul din nou, becul se stinge. Dacă utilizatorul apasă butonul rapid de două ori, becul se aprinde mai puternic. Utilizatorul poate apasă butonul
aleatoriu în orice moment sau poate să nu apese butonul deloc. Cronometrul y al becului este
folosit pentru a detecta dacă utilizatorul a apăsat rapid (y <5) sau lent ( y≥5).

Figură 3 – Exemplul becului

Vlad Rădulescu
28 Limbajul de modelare UPPAAL extinde automatele temporale cu următoarele caracteristici
adiționale:
• Șabloane: Automatele sunt definite cu un set de parametri care pot fi de orice tip (int,
chan, etc.). Acești parametri sunt substituiți pentru un argument dat în declararea proceselor.
• Constante: Constantele sunt declarate ca „const nume valoare”. Prin definiție, constantele
nu pot fi modificate și trebuie să aibă o valoare întreagă.
• Variabile întregi mărginite: Declarate ca „int[min, max] nume ”, unde min și max
reprezintă marginea infe rioară și superioară respectiv.
• Sincronizare binară: canale se declară ca „chan c”. O muchie notată cu c! sincronizează cu
o altă muchie notată c?. O pereche de sincronizat se alege nedeterminist dacă există mai multe
combinații posibile.
• Canale de difuzare în masă: declarate ca „broadcast chan c”. În sincronizarea în masă, un
emițător c! poate sincroniza cu un număr arbitrar de receptori c?. Orice receptor care poate sincroniza în stadiul curent este obligat să se sincronizeze. Dacă nu există receptori, emițătorul
poate încă executa acțiunea c!.
• Sincronizare urgentă: canalele sunt declarate prefixând declarația lor folosind cuvântul
cheie „urgent”. Dacă tranziția de sincronizare este activată pe un canal urgent, nu se pot produce
întârzieri. Muchiile care folosesc canale urgente pentru sincronizare nu permit constrânge ri de
timp.
• Locații urgente: semantic echivalente cu un cronometru adițional x care este resetat pe
toate muchiile de intrare și care are un invariant x ≤0 pe locație. Așadar, timpul nu este permis să
avanseze când sistemul se află într -o locație urgentă.
• Locații dedicate: locații și mai restrictive față de locațiile urgente. Un stadiu este dedicat
dacă oricare dintre locațiile din stare este dedicat. O stare dedicată nu poate avea întârzieri iar
următoarea transmisie trebuie să includă o muchie de ieșire la cel puțin una din locațiile dedicate.
• Vectori: sunt permiși pentru cronometre , canale, constante și variabile întregi. Sunt
definiți anexând o dimensiune numelui variabilei.
• Inițializatori: folosiți pentru a inițializa variabile întregi și vectori de variabile întregi.
• Funcții definite de utilizator: definite fie global fie local unui șablon.

Vlad Rădulescu
29 În UPPAAL, expresiile se aplică asupra cronometrelor și a variabilelor întregi. Acestea se
folosesc cu următoarele etichete:
• Select : O etichetă select conține o listă de expresii „nume:tip” separate de virgule, unde
numele reprezintă numele unei variabile iar tipul este un tip definit, fie de utilizator fie implicit.
Aceste variabile sunt accesibile doar pe muchia asociată și vor primi o valoare nedeterministă în
câmpul asociat tipului lor.
• Guard: Reprezintă o expresie anume care satisface condițiile de a fi lipsită de efecte
secundare, de a evalua către un boolean, face referire doar la cronometre , variabile întregi sau
constante sau vectori de aceste tipuri, cronometre și diferențe de cronometre se compară doar cu
expresii întregi, iar guarduri asupra cronometre lor sunt în esență conjuncții, cu disjuncții permise
asupra condițiilor întregi. Un guard poate invoca o funcție fără efecte secundare care returnează
un boolean, însă în astfel de funcții nu sunt suportate constrângeri de cronometru .
• Sincronizare: O etichetă de sincronizare este fie de forma Expressie! sau Expressie? sau
este o etichetă vidă. Expresia trebuie să fie fără efecte secundare, trebuie să evalueze pe un canal
și să facă referire doar la întregi, constante și canale.
• Update: O etichetă update este o listă de expresii cu un efect secundar; expresiile trebuie
să facă referire doar la cronometre , variabile întregi și constant și să atribuie valori în tregi
cronometre lor. Pot de aseme nea apela funcții.
• Invariant: Un invariant este o expresie care satisface următoarele condiții: trebuie să fie
lipsită de efecte secundare, să facă referire doar la cronometre , variabile întregi sau constante, să
fie o conj uncție de condiții de forma x <e sau x ≤e unde x este o referință la un cronometru și e
evaluează către un întreg. Un invariant poate face apel la o funcție ce returnează un boolean, însă
constrângeri de cronometru nu sunt suportate în astfel de funcții.
Principalul scop al unui verificator de modele este a de a verifica modelul cu referire la o
specificare cerută. La fel precum modelul, specificarea trebuie exprimată într -un limbaj formal
bine definit care poate fi citit de către calculator. UPPAAL folosește o versiune simplificată a
limbajului TCTL.
Limbajul de interogări este alcătuit din formule de cărare și formule de stări. Formulele de
stări descriu stări individuale iar formulele de cărare cuantifică asupra cărărilor modelului.

Vlad Rădulescu
30 O formulă de stare este o expresie care poate fi evaluată pentru o stare fără a se lua în
considerare comportamentul modelului. De exemplu, aceasta poate fi o expresie simplă de forma
i == 7, care este adevărată într -o stare oricând i este egal cu 7.
În UPPAAL, deadlockul es te exprimat folosind o formulă de stare specială, alcătuită doar
din cuvântul cheie „deadlock” și care este satisfăcută pentru toate stările de deadlock.
Proprietățile de atenuabilitate sunt cele mai simple proprietăți. Acestea pun întrebarea dacă
o formul ă de stare dată φ poate fi satisfăcută de orice stare atenuabilă. Se mai poate formula ca o
întrebare de forma: Există o cărare de la starea inițială astfel încât φ ajunge să fie satisfăcută de- a
lungul acesteia?
Proprietățile de atenuabilitate sunt deseor i folosite în proiectarea unui model pentru a
asigura coerență logică. De exemplu, în modelarea unui protocol de comunicare care implică un
emițător și un receptor, este logic să se pună întrebarea dacă este posibil pentru emițător să trimită
un mesaj sau dacă un mesaj se poate primi de către receptor. Aceste proprietăți nu asigură
corectitudinea protocolului, dar validează comportamentul fundamental al modelului.
În UPPAAL, astfel de proprietăți se notează sintactic sub forma E <> φ,
Proprietățile de sigura nță au scopul de a asigura prevenirea situațiilor nedorite. De exemplu,
în modelarea unei centrale nucleare, o proprietate de siguranță ar fi asigurarea că temperatura de
operație este menținută constant sub un anumit prag. O variație a acestor proprietăți o reprezintă
idea asigurări că este posibil ca ceva să nu se întâmple. De exemplu, în cazul unui joc, o stare sigură este aceea în care jocul încă se poate câștiga, adică este posibil să nu se piardă.
În UPPAAL aceste proprietăți sunt formulate pozitiv, a dică ce dorim este invariabil
adevărat. Fie φ o formulă de stare. Spunem că φ trebuie să fie adevărată în toate stările care se pot
atinge cu formula de cărare A [] φ, iar E[] φ spune că trebuie să existe o cărare maximală astfel
încât φ este întotdeauna adevărată.
Proprietățile de vivacitate pot fi exprimate sub forma „ceva se va întâmpla până la urmă.”.
De exemplu, butonul de pornire pe telecomandă va porni televizorul, sau în cazul unui protocol
de comunicare, orice mesaj trimis va fi recepționat într -un final.

Vlad Rădulescu
31 În cea mai simplă formă, proprietățile de vivacitate sunt exprimate cu formula de cărare
A<> φ, adică φ va fi satisfăcută într -un final. O formulă mai utilă este proprietatea „conduce la”
sau de răspuns, notată φ –> ψ, citită ca „de fiecare dată când φ este satisfăcută, atunci și ψ va fi
satisfăcută până la urmă.
10

Vlad Rădulescu
32 Studiu de Caz
Se consideră următoarea problemă, descrisă în limbaj natural: Fie două mașini pe o stradă
care caută simultan un loc de parcare. Mașinile se pot deplasa în față sau în spate, iar senzorii lor
vor interoga un automat paralel ce modelează strada pe care se află. Când se găsește un loc de
parcare disponibil, se pot deplasa către acesta și efectua o par care. Se va considera că strada are o
dimensiune de 5 și două locuri de parcare adecvate, iar fiecare mașină are nevoie de o unitate de dimensiune pentru a parca. Autom atele paralele vor comunica prin canale partajate.
Pentru acest exemplu, avem nevoie de un mo del ce cuprinde două automate cu stări finite:
unul pentru obiectul mașină iar unul pentru stradă .
Obiectul mașinii va avea patru stări:
• Starea inițială „Start”, care se sincronizează pe un canal numit „deplasare”;
• Starea de căutare a unui loc de parcare „Găsește_parcare”. În cazul în care nu se
găsește un loc disponibil, rămâne în această stare prin sincronizarea „continuă”. Dacă există un loc disponibil, va trece în starea următoare prin sincronizarea „parchează”.
Dacă s -a ajuns la sfârșitul străzii, se va trece în ultima stare prin sincronizarea
„sfârșit_stradă”.
• Starea de parcare, numită „Efectuează parcare”. Se sincronizează cu starea
„Găsește_parcare” prin canalul „parchează” și odată ce se dorește ieșirea din parcare se întoarce în starea „Găsește_parcare” prin canalul „pornire”.
• Starea finală, ”Capăt_stradă”.
În declararea obiectului mașină se va defini un cronometru „așteaptă”, o variabilă întreagă
„poziție” și un boolean „parcat” pentru a ține seama de timpul pe care mașina îl petrece parcată,
poziția sa de- a lungul străzii și dacă se află în parcare sau nu, respectiv. La fiecare trecere
relevantă dintr -o stare în alta, variabila „poziție” se va incrementa cu 1, iar la efectuarea parcării
cronometrul „așteaptă” va fi resetat la 0 și booleanul „parca t” va primi valoarea „true”, urmând să
primească valoarea „false” la părăsirea parcării.

Vlad Rădulescu
33 Obiectul străzii va cuprinde următoarele stări:
• O stare inițială, „început_stradă”, care se va sincroniza pe canalul „deplasare” cu
obiectul mașină.
• Pentru fiecare loc de parcare, există trei stări:
o O stare în care parcarea este „vizibilă”, de unde o mașină poate efectua
parcarea, sincronizând pe canalul „parchează” sau, dacă parcarea este
ocupată, poate conti nua mai departe pe stradă.
o O stare care indică locul de parcare în sine, care se sincronizează pe canalul „parchează” pentru a fi ocupat și pe canalul „pornire” pentru a fi eliberat.
o O stare de continuare, la care se ajunge de la oricare dintre cele două stări
enumerate mai sus, de unde se poate sincroniza pe canalul „continuă” pentru
a se ajunge mai departe.
• O stare finală, care se sincronizează prin canalul „sfârșit_stradă”.

Figură 4 – Obiectul „Mașină”

Vlad Rădulescu
34 În declarațiile obiectului stradă nu este nevoie decât de o variabilă „lungime_stradă”,
inițializată cu valoarea 0, care va fi incrementată la fiecare muchie între stări relevantă pentru a
ține seama de parcursul mașinilor pe stradă.
În declarațiile global e ale modelului se vor declara cele cinci canale de sincronizare
utilizate de automate și două variabile booleene, inițializate ca false, care vor ține cont de starea locurilor de parcare. Acestea vor fi setate ca fiind true sau false atunci când o mașină efectuează o
parcare pe un loc sau părăsește un loc, respectiv, și vor fi evaluate pentru a asigura dacă un loc este deja ocupat sau nu.
Figură 5 – Obiectul „Stradă”

Vlad Rădulescu
35 Deoarece sunt două mașini, vor fi necesare două instanțe ale obiectului mașină și două
instanțe ale străzii, care pot fi gândite ca fiind două benzi de circulație: mașinile se pot afla în
același spațiu pe stradă, dar nu același loc de parcare.
Odată ce componentele sistemului au fost definite și instanțele lor create, modelul
sistemului poate fi simulat, fie manual fie automat de către utilitarul simulator al programului
UPPAAL. Astfel se pot depista situații de deadlock nedorite și se poate asigura că sistemul se
comportă conform așteptărilor.

Figură 6 – Modelul în curs de simulare

Vlad Rădulescu
36
Figură 7 – Exemplu de executare a simulării

Vlad Rădulescu
37 După simulare, dacă modelul se comportă conform specificării, se poate efectua verificarea
bazată pe model folosind utilitarul de verificare UP PAAL. Utilitarul permite introducerea
interogări lor pentru a specifica proprietăți și verificarea validității acestora. De asemenea se poate
introduce un comentariu pentru a enunța proprietatea căutată în limbaj natural.
Prima proprietate pe care am verificat -o este aceea că sistemul ajunge în situație de
deadlock doar atunci când ambele mașini au ajuns la capătul străzii. Proprietatea este satisfăcută.

Figură 8 – Verificare deadlock
A doua proprietate verificată a fost aceea că nu există o situație în care ambele mașini să fie
parcate și acestea să ocupe aceeași poziție. Și această proprietate este satisfăcută în cadrul
sistemului proiectat.

Figură 9 – Verificare suprapunere

Vlad Rădulescu
38 Ultima proprietate verificată a fost aceea că nu se poate ca lungimea străzilor să depășească
cele 5 unități posibile. De asemenea și această proprietate este satisfăcută.

Figură 10 – Verificarea lungimi străzii

Vlad Rădulescu
39 Concluzii
Metoda verificării modelelor de sistem rep rezintă o abordare puternică în detectarea
erorilor de proiectare a sistemelor software sau hardware. Aceasta oferă posibilitatea de a asigura
validitatea unor proprietăți urmărite în specificația programului cu certitudine și rigurozitate
matematică . Veri ficarea modelelor este îndeosebi importantă în realizarea acelor aplicații care
sunt de importanț ă mare, unde greșeli de implementare pot avea consecințe costisitoare sau chiar
dezastroase, sau în acele aplicații unde efortul de verificare a comportamentul ui sistemului
implică un efort și cost de timp și resurse prea mare pentru a fi efectuat cu alte metode.
Odată cu siguranța și claritatea oferită de abordarea model checking însă vine și necesitatea
unui efort sporit de proiectare și planificare care o poa te face o alegere nepotrivită pentru anumite
domenii și aplicații. Este de reținut faptul că rezultatele obținute prin verificarea modelului unui
sistem sunt în raport direct cu nivelul de acuratețe și calitate al modelului în sine. Astfel, realizarea unui model, proces care la rândul său implică un efort de proiectare și necesită un nivel
sporit de cunoștințe tehnice de specialitate , poate reprezenta un pas superfluu în realizarea un ei
aplicații redusă din punct de vedere al complexității și al scopului pe ntru care este creată.

Vlad Rădulescu
40 Bibliografie
1. Baier, C., & Katoen, J.- P. (2008). Principles of Model Checking. Cambridge: MIT Press.
2. Behrmann, G., David, A., & Larsen, K. G. A Tutorial on Uppaal 4.0. Preluat pe Mai
2019, de pe https://www.it.uu.se/re search/group/darts/papers/texts/new -tutorial.pdf