Limbajul Promela. Logici Temporale

Cuprins disertatie Cum descarc?

Introducere 5
Capitolul I - Programare secventiala in PROMELA 6
1. Fazele dezvoltarii de produse software pentru sisteme mecatronice si verificarile lor: nevoia unui model checker 6
1.1. Sistem mecatronic 6
1.2. Modele pentru dezvoltarea de software - unde verificam? Viziunea traditionala si cea moderna 6
2. SPIN - Simple Promela Interpreter: avantaje SPIN si Promela 8
2.1. Ce este SPIN? 8
2.2. Promela (PROtocol/Process MEta LAnguage) 8
3. Modelul Promela - componente si exemple 9
3.1. Variabile si tipuri 10
3.2. Tipuri de instructiuni 12
3.3. Procese in Promela 13
4. Semantica proceselor modelate cu Promela. Proprietatea de excludere mutuala. 15
4.1. Semantica pentru intercalarea executiei proceselor concurente 15
4.2. Proprietatea de excludere mutuala 15
5. Instructiuni SPIN si aplicarea lor pentru verificarea proprietatilor unui sistem software; exemple practice 17
5.1. Instructiunea if 17
5.2. Expresiile conditionale 19
5.3. Instructiunea do 19
5.3.1. Bucle numarabile 21
5.4. Enunturi salt (goto) 23
5.5. Comunicarea cu channel 23
5.5.1 Alternari de biti 26
5.6. Verificarea atomicitatii - instructiunea atomic 27
5.7. Instructiunea d_step 28
5.8 Instructiunea de control timeout 30
5.9 Instructiuni de verificare 30
5.9.1 Verificare: asertiuni 30
5.9.2 Verificare: etichete stari finale 31
5.9.3 Verificare: etichete stari-progres 31
5.9.4 Stari etichetate cu accept. 32
5.9.5 Verificare: ,,never claim" 32
5.9.6 Verificare: asertiuni despre urme 33
5.9.7 Verificarea invariantilor 33
Capitolul II - Logici temporale 35
1. Logica temporala cu timp liniar (LTL) 35
2. Logica temporala (propozitionala) cu timp ramificat CTL, CTL* 43
2.1. Computation Tree Logic (CTL) 43
2.2. CTL* 53
Capitolul 3 - jSpin 56
1. Instalare si executarea 56
1.1 Instalare simplificata pentru Windows: 56
1.2 Configurarea si functionarea JSPIN 57
2. jSpin - prezentare generala 57
3. Rularea SPIN 59
3.1 Simularea 59
3.2 Verificarea 60
3.3 Formule LTL 61
4. SpinSpider 61
5. Programe PROMELA pentru SpinSpider. 65
Cum functioneaza SpinSpider 66
Rularea SpinSpider fara JSPIN* 66
Rularea FILTERSPIN fara JSPIN * 67
6. Verificarea unui program in jSpin 67
6.1. Simulare asistata 69
6.2 Afisarea unui calcul 70
7. Intercalare 71
7.1 Afisarea unui calcul 72
7.2 Simulare interactiva 73
7.3 Interferenta intre procese 74
7.4. Seturi de procese 75
Capitolul IV - Aplicatii 77
1. Formule ca automate 77
2. Problema: Puzzle - Broastele din iaz. 78
3. Problema soldatilor 80
4. Automat vanzari bauturi. 81
5. Verificare: etichete stari finale 82
6. Verificare: etichete stari-progres 83
7. Verificare: cicluri fair 83
8. Verificare: cicluri fair accept 84
Concluzii 85
Anexa 86
Bibliografie 88


Extras din disertatie Cum descarc?

Introducere
Multe calculatoare sunt utilizate in domeniul sistemelor integrate, care sunt compuse de hardware, software, senzori, controlere si display-uri, si care sunt destinate a fi folosite la nesfarsit si fara supraveghere continua. Trebuie doar sa ne gindim la avioane, monitoare medicale, precum si retelele de telefoane mobile pentru a aprecia complexitatea sistemelor integrate. Invariabil, aceste sisteme contin mai multe procese care trebuie sa probeze senzori si sa efectueze calculele aproximativ in acelasi timp, de exemplu, un control medical probeaza monitorizarea ritmului cardiac, tensiunea arteriala si temperatura, si stabileste daca acestea sunt intr-un interval prestabilit. Programarea pentru sisteme de multiprocess este numita programare concurenta.
In mod frecvent, sistemele integrate contin mai multe procesoare; microprocesoare au devenit atat de ieftine incat este posibil sa se dedice un procesor separat pentru fiecare subsistem. In plus, multe sisteme precum retelele de telefonie mobila sunt, prin natura dispersate geografic, bazandu-se pe retele de comunicatii pentru a transmite date intre procesoare. Programarea pentru astfel de sisteme se numeste programare distribuita. 
SPIN sustine modelarea ambele sisteme: concurente si distribuite. Aceasta lucrare este referitoare la scrisul si verificarea programelor concurente; utilizarea canalelor cu modelul sistemelor distribuite.
In capitolul I, intitulat "Programare segventiala in Promela" se prezinta limbajul de modelare Promela. Capitolul II, intitulat ,,Logici temporale" abordeaza Logica temporala cu timp liniar (LTL), Computation Tree Logic - logica temporala cu timp ramificat (CTL) si CTL* din punct de vedere semantic si sintactic. 
Capitolul III intitulat ,,jSpin" prezinta programul si modalitatea de aplicare a unor verificari cu ajutorul acestui program. Verificatorul jSPIN executa verificarea si validarea modelului si ofera utilizatorului rezultatele. Desi este proiectat pentru verificarea modelelor si sistemelor distribuite concurente, vom introduce verificarea elementara in cadrul programelor secventiale. Acest capitol arata cum sa se exprime corectitudinea specificatiilor folosind afirmatii si descrie procedura pentru efectuarea unei verificari in jSPIN. In Capitolul IV sunt prezentate programe reprezentative de implementare complexe. In anexa se prezinta configurarea fisierelor.
Capitolul I - Programare secventiala in PROMELA
1. Fazele dezvoltarii de produse software pentru sisteme mecatronice si verificarile lor: nevoia unui model checker
1.1. Sistem mecatronic 
Un sistem mecatronic reprezinta un ansamblu de componente mecanice coordonate de componente electronice programate prin software, ce interactioneaza intre ele si, acelasi timp, ca tot unitar, interactioneaza cu mediul in care este integrat. 
Exemple de sisteme mecatronice pot fi vazute pretutindeni in jurul nostru: de la masini de spalat si automate de cafea - uzuale in peisajul lumii moderne, pana la avioane, nave spatiale sau dispozitive pentru realizarea de operatii cu laser la distanta ale caror functionare corecta si performanta sunt critice. 
Din definitia sistemelor mecatronice putem usor observa faptul ca programarea corecta si verificarea corectitudini programelor ce dirijeaza activitatea acestor sisteme sunt chestiuni vitale. 
Printre greselile cele mai frecvente din designul sistemelor mecatronice se numara: 
- deadlock-ul - blocajul sistemului - de exemplu, doua componente astepta una de la alta un raspuns sau o actiune 
- livelock-ul - sistemul nu mai evolueaza 
- underspecification - subspecificarea - nu sunt prevazute toate scenariile de folosire a sistemului si exista evenimente ale caror aparitie nu este tratata; apar astfel mesaje de eroare neasteptate
- overspecification - supraspecificare - scrierea de "cod mort", care nu produce nimic
- violarea constrangerilor - de memorie, latime de banda etc. - ce duc la depasirea bufferelor alocate sau a limitelor unor vectori definiti 
- presupuneri ce tin de viteza sistemului - un sistem poate fi total corect din punct de vedere al specificarii sale logice, dar sa nu tina cont de performanta in timp real, fapt critic mai ales in sistemele mecatronice folosite in medicina. 
Majoritatea acestor greseli pot fi insa detectate folosind tehnici de model checking. O verificare exhaustiva a tuturor posibilitatilor de comportament ale unui sistem este aproape imposibila ( problema exploziei de stari). 
Totul revine la urmatoarele intrebari: "Unde anume in ciclul dezvoltarii de software este cel mai potrivit sa facem model checking?", "Cum se poate evita explozia de stari?" si "Care este cel mai potrivit limbaj pentru model checking? Ce trebuie el sa contina?" 
1.2. Modele pentru dezvoltarea de software - unde verificam? Viziunea traditionala si cea moderna 
In viziunea clasica a dezvoltarii de proiecte - modelul cascada - ce cuprinde fazele de:
- Analiza, 
- Design, 
- Implementare, 
- Testare, 
- Intretinere
in mod traditional, model checking-ul se facea in fazele de analiza, design si implementare. Astfel, pornind de la analiza specificatiilor se crea un model abstract, ce era apoi verificat si rafinat prin model checking pentru ca implementarea sa sa fie cat mai aproape de optim. Evident, si aceasta era ulterior verificata prin model checking, daca este conforma cu modelul sau abstract, activitate ce ulterior era practic verificata in cadrul fazei de testare. 
Viziunea moderna asupra model checking-ului plaseaza aceasta activitate intre faza de implementare si cea de testare. Modelul abstract este construit, in aceasta abordare, din implementarea insasi - modelul implementat prin module de program in Java, C# etc. Se presupune ca abstractizarea modelului din viziunea traditionala intre analiza si implementare are loc implicit, prin nevoia de modularizare presupusa de limbajele de nivel inalt puternic modularizate care sunt folosite in prezent la crearea de software.


Fisiere in arhiva (1):

  • Limbajul Promela. Logici Temporale.doc

Imagini din aceasta disertatie Cum descarc?

Banii inapoi garantat!

Plateste in siguranta cu cardul bancar si beneficiezi de garantia 200% din partea Diploma.ro.


Descarca aceasta disertatie cu doar 8 €

Simplu si rapid in doar 2 pasi: completezi adresa de email si platesti.

1. Numele, Prenumele si adresa de email:

Pe adresa de email specificata vei primi link-ul de descarcare, nr. comenzii si factura (la plata cu cardul). Daca nu gasesti email-ul, verifica si directoarele spam, junk sau toate mesajele.

2. Alege modalitatea de plata preferata:



* La pretul afisat se adauga 19% TVA.


Hopa sus!