Modelowanie systemów współbieżnych w języku Alvis
Marcin Szpyrka
oprawa: miękka
format: B5
stron: 236
rok wydania: 2013
wydawnictwo: AGH
Praca zawiera podsumowanie wyników wieloletnich badań autora w obszarze zastosowania metod formalnych w inżynierii oprogramowania. Autor zaproponował w niej nowy formalny język modelowania (Alvis) i pokazał potencjalne korzyści wynikające z jego praktycznego zastosowania w procesie wytwarzania oprogramowania. Wprawdzie język Alvis został zainspirowany algebrami procesów i sieciami Petriego, ale opracowano go przede wszystkim z myślą o wygodzie stosowania z inżynierskiego punktu widzenia. Najistotniejszą zaletą proponowanego podejścia, pomijając kwestie dotyczące syntaktyki, jest starannie opracowana formalna semantyka języka, w szczególności metoda wyrażania stanów systemów i definicje przejść między stanami. W monografii można również znaleźć inne wartościowe wyniki naukowe, takie jak metoda reprezentowania i weryfikacji systemów regułowych z użyciem języka Haskell oraz metoda weryfikacji grafów LTS. Omówiono nie tylko klasyczne podejście bazujące na technikach weryfikacji modelowej (logika temporalna), ale również nowatorskie - z użyciem funkcji filtrujących implementowanych w Haskellu.
SPIS TREŚCI:
1. Wprowadzenie 9
1.1. Metody formalne 11
1.2. Geneza i charakterystyka języka Alvis 20
1.3. Zawartość książki 24
2. Podstawy modelowania w języku Alvis 29
2.1. Proces modelowania i weryfikacji systemów 29
2.2. Model z komunikacją asynchroniczną 31
2.3. Model z komunikacją synchroniczną 37
2.4. Podsumowanie 40
3. Diagramy komunikacji 41
3.1. Niehierarchiczne diagramy komunikacji 41
3.2. Hierarchiczne diagramy komunikacji 46
3.3. Usuwanie hierarchii 53
3.4. Podsumowanie 62
4. Definiowanie dynamiki agentów 63
4.1. Struktura warstwy kodu 64
4.2. Parametry 65
4.3. Komunikacja 67
4.4. Instrukcje pętli i instrukcja skoku 69
4.5. Instrukcje wyboru 71
4.6. Procedury 74
4.7. Pozostałe instrukcje 76
4.8. Podsumowanie. 77
5. Model w języku Alvis 79
5.1. Model i jego stan 79
5.2. Semantyka przejść 91
5.3. Etykietowane systemy przejść 105
5.4. Podsumowanie 112
6. Modele z systemem regułowym 113
6.1. Tablice decyzyjne 114
6.2. Implementacja tablic decyzyjnych w Haskellu 117
6.3. Analiza systemów regułowych 120
6.4. Podsumowanie126
7. Modelowanie systemów czasu rzeczywistego 127
7.1. Czas w instrukcjach języka Alvis 127
7.2. Czas realizacji instrukcji 129
7.3. SR-grafy 132
7.4. Semantyka przejść 136
7.5. Podsumowanie 142
8. Modelowanie dynamiki otoczenia 143
8.1. Porty graniczne 143
8.2. Diagramy komunikacji z portami granicznymi 147
8.3. Stan modelu 149
8.4. Semantyka przejść 150
8.5. Iteracyjne konstruowanie modeli 154
8.6. Podsumowanie162
9. Weryfikacja 163
9.1. Ograniczony rachunek 164
9.2. CADP evaluator 168
9.3. Funkcje filtrujące 176
9.4. Podsumowanie 182
10. Wnioski końcowe 183
A. Programowanie funkcyjne w języku Haskell 187
A.1. Podstawy programowania i środowisko pracy 188
A.2. Definiowanie funkcji 191
A.3. Listy 197
A.4. Krotki 202
A.5. Definiowanie typów danych 202
B. Oprogramowanie 205
B.1. Alvis Editor 205
B.2. Alvis Translator 208
