Limbajul Promela. Logici Temporale

Disertație
8/10 (1 vot)
Conține 1 fișier: doc
Pagini : 88 în total
Cuvinte : 22039
Mărime: 1.64MB (arhivat)
Cost: 9 puncte
UNIVERSITATEA PITESTI Facultatea de Matematică-INFORMATICĂ MASTER POSTUNIVERSITAR INFORMATICĂ

Cuprins

Introducere 5

Capitolul I - Programare secvenţială în PROMELA 6

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

1.1. Sistem mecatronic 6

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

2. SPIN - Simple Promela Interpreter: avantaje SPIN şi Promela 8

2.1. Ce este SPIN? 8

2.2. Promela (PROtocol/Process MEta LAnguage) 8

3. Modelul Promela - componente şi exemple 9

3.1. Variabile şi tipuri 10

3.2. Tipuri de instrucţiuni 12

3.3. Procese în Promela 13

4. Semantica proceselor modelate cu Promela. Proprietatea de excludere mutuală. 15

4.1. Semantica pentru intercalarea execuţiei proceselor concurente 15

4.2. Proprietatea de excludere mutuală 15

5. Instrucţiuni SPIN şi aplicarea lor pentru verificarea proprietăţilor unui sistem software; exemple practice 17

5.1. Instrucţiunea if 17

5.2. Expresiile condiţionale 19

5.3. Instrucţiunea do 19

5.3.1. Bucle numărabile 21

5.4. Enunţuri salt (goto) 23

5.5. Comunicarea cu channel 23

5.5.1 Alternări de biţi 26

5.6. Verificarea atomicităţii - instrucţiunea atomic 27

5.7. Instructiunea d_step 28

5.8 Instrucţiunea de control timeout 30

5.9 Instrucţiuni de verificare 30

5.9.1 Verificare: aserţiuni 30

5.9.2 Verificare: etichete stări finale 31

5.9.3 Verificare: etichete stări-progres 31

5.9.4 Stări etichetate cu accept. 32

5.9.5 Verificare: „never claim” 32

5.9.6 Verificare: aserţiuni despre urme 33

5.9.7 Verificarea invarianţilor 33

Capitolul II - Logici temporale 35

1. Logica temporală cu timp liniar (LTL) 35

2. Logica temporală (propoziţională) cu timp ramificat CTL, CTL* 43

2.1. Computation Tree Logic (CTL) 43

2.2. CTL* 53

Capitolul 3 - jSpin 56

1. Instalare şi executarea 56

1.1 Instalare simplificată pentru Windows: 56

1.2 Configurarea şi funcţionarea JSPIN 57

2. jSpin – prezentare generală 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 funcţionează SpinSpider 66

Rularea SpinSpider fără JSPIN* 66

Rularea FILTERSPIN fără JSPIN * 67

6. Verificarea unui program în jSpin 67

6.1. Simulare asistată 69

6.2 Afişarea unui calcul 70

7. Intercalare 71

7.1 Afişarea unui calcul 72

7.2 Simulare interactivă 73

7.3 Interferenţa între procese 74

7.4. Seturi de procese 75

Capitolul IV - Aplicaţii 77

1. Formule ca automate 77

2. Problema: Puzzle – Broaştele din iaz. 78

3. Problema soldaţilor 80

4. Automat vanzări bauturi. 81

5. Verificare: etichete stări finale 82

6. Verificare: etichete stări-progres 83

7. Verificare: cicluri fair 83

8. Verificare: cicluri fair accept 84

Concluzii 85

Anexă 86

Bibliografie 88

Extras din document

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.

Preview document

Limbajul Promela. Logici Temporale - Pagina 1
Limbajul Promela. Logici Temporale - Pagina 2
Limbajul Promela. Logici Temporale - Pagina 3
Limbajul Promela. Logici Temporale - Pagina 4
Limbajul Promela. Logici Temporale - Pagina 5
Limbajul Promela. Logici Temporale - Pagina 6
Limbajul Promela. Logici Temporale - Pagina 7
Limbajul Promela. Logici Temporale - Pagina 8
Limbajul Promela. Logici Temporale - Pagina 9
Limbajul Promela. Logici Temporale - Pagina 10
Limbajul Promela. Logici Temporale - Pagina 11
Limbajul Promela. Logici Temporale - Pagina 12
Limbajul Promela. Logici Temporale - Pagina 13
Limbajul Promela. Logici Temporale - Pagina 14
Limbajul Promela. Logici Temporale - Pagina 15
Limbajul Promela. Logici Temporale - Pagina 16
Limbajul Promela. Logici Temporale - Pagina 17
Limbajul Promela. Logici Temporale - Pagina 18
Limbajul Promela. Logici Temporale - Pagina 19
Limbajul Promela. Logici Temporale - Pagina 20
Limbajul Promela. Logici Temporale - Pagina 21
Limbajul Promela. Logici Temporale - Pagina 22
Limbajul Promela. Logici Temporale - Pagina 23
Limbajul Promela. Logici Temporale - Pagina 24
Limbajul Promela. Logici Temporale - Pagina 25
Limbajul Promela. Logici Temporale - Pagina 26
Limbajul Promela. Logici Temporale - Pagina 27
Limbajul Promela. Logici Temporale - Pagina 28
Limbajul Promela. Logici Temporale - Pagina 29
Limbajul Promela. Logici Temporale - Pagina 30
Limbajul Promela. Logici Temporale - Pagina 31
Limbajul Promela. Logici Temporale - Pagina 32
Limbajul Promela. Logici Temporale - Pagina 33
Limbajul Promela. Logici Temporale - Pagina 34
Limbajul Promela. Logici Temporale - Pagina 35
Limbajul Promela. Logici Temporale - Pagina 36
Limbajul Promela. Logici Temporale - Pagina 37
Limbajul Promela. Logici Temporale - Pagina 38
Limbajul Promela. Logici Temporale - Pagina 39
Limbajul Promela. Logici Temporale - Pagina 40
Limbajul Promela. Logici Temporale - Pagina 41
Limbajul Promela. Logici Temporale - Pagina 42
Limbajul Promela. Logici Temporale - Pagina 43
Limbajul Promela. Logici Temporale - Pagina 44
Limbajul Promela. Logici Temporale - Pagina 45
Limbajul Promela. Logici Temporale - Pagina 46
Limbajul Promela. Logici Temporale - Pagina 47
Limbajul Promela. Logici Temporale - Pagina 48
Limbajul Promela. Logici Temporale - Pagina 49
Limbajul Promela. Logici Temporale - Pagina 50
Limbajul Promela. Logici Temporale - Pagina 51
Limbajul Promela. Logici Temporale - Pagina 52
Limbajul Promela. Logici Temporale - Pagina 53
Limbajul Promela. Logici Temporale - Pagina 54
Limbajul Promela. Logici Temporale - Pagina 55
Limbajul Promela. Logici Temporale - Pagina 56
Limbajul Promela. Logici Temporale - Pagina 57
Limbajul Promela. Logici Temporale - Pagina 58
Limbajul Promela. Logici Temporale - Pagina 59
Limbajul Promela. Logici Temporale - Pagina 60
Limbajul Promela. Logici Temporale - Pagina 61
Limbajul Promela. Logici Temporale - Pagina 62
Limbajul Promela. Logici Temporale - Pagina 63
Limbajul Promela. Logici Temporale - Pagina 64
Limbajul Promela. Logici Temporale - Pagina 65
Limbajul Promela. Logici Temporale - Pagina 66
Limbajul Promela. Logici Temporale - Pagina 67
Limbajul Promela. Logici Temporale - Pagina 68
Limbajul Promela. Logici Temporale - Pagina 69
Limbajul Promela. Logici Temporale - Pagina 70
Limbajul Promela. Logici Temporale - Pagina 71
Limbajul Promela. Logici Temporale - Pagina 72
Limbajul Promela. Logici Temporale - Pagina 73
Limbajul Promela. Logici Temporale - Pagina 74
Limbajul Promela. Logici Temporale - Pagina 75
Limbajul Promela. Logici Temporale - Pagina 76
Limbajul Promela. Logici Temporale - Pagina 77
Limbajul Promela. Logici Temporale - Pagina 78
Limbajul Promela. Logici Temporale - Pagina 79
Limbajul Promela. Logici Temporale - Pagina 80
Limbajul Promela. Logici Temporale - Pagina 81
Limbajul Promela. Logici Temporale - Pagina 82
Limbajul Promela. Logici Temporale - Pagina 83
Limbajul Promela. Logici Temporale - Pagina 84
Limbajul Promela. Logici Temporale - Pagina 85
Limbajul Promela. Logici Temporale - Pagina 86
Limbajul Promela. Logici Temporale - Pagina 87
Limbajul Promela. Logici Temporale - Pagina 88
Limbajul Promela. Logici Temporale - Pagina 89

Conținut arhivă zip

  • Limbajul Promela. Logici Temporale.doc

Te-ar putea interesa și

Principalele Caracteristici ale Diagramelor BPMN - Business Process Modeling Notation

Prezentaţi pe scurt principalele caracteristici ale diagramelor BPMN (Business Process Modeling Notation) şi evidenţiaţi diferenţele dintre acestea...

CDS

Capitolul 1 2016-2017 Rezumat •Definirea modelului abstract al calculului concurent. Modelul intreteserii. •Corectitudine •Implementarea...

Ai nevoie de altceva?