MODELOWANIE SYSTEMÓW WSPÓŁBIEŻNYCH W JĘZYKU ALVIS

ISBN: 978-83-7464-607-9   235 stron format: B5 oprawa: miękka Rok wydania: 2013

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
1.1. Metody formalne
1.2. Geneza i charakterystyka języka Alvis
1.3. Zawartość książki

2. Podstawy modelowania w języku Alvis
2.1. Proces modelowania i weryfikacji systemów
2.2. Model z komunikacją asynchroniczną
2.3. Model z komunikacją synchroniczną
2.4. Podsumowanie

3. Diagramy komunikacji
3.1. Niehierarchiczne diagramy komunikacji
3.2. Hierarchiczne diagramy komunikacji
3.3. Usuwanie hierarchii
3.4. Podsumowanie

4. Definiowanie dynamiki agentów
4.1. Struktura warstwy kodu
4.2. Parametry
4.3. Komunikacja
4.4. Instrukcje pętli i instrukcja skoku
4.5. Instrukcje wyboru
4.6. Procedury
4.7. Pozostałe instrukcje
4.8. Podsumowanie

5. Model w języku Alvis
5.1. Model i jego stan
5.2. Semantyka przejść
5.3. Etykietowane systemy przejść
5.4. Podsumowanie

6. Modele z systemem regułowym
6.1. Tablice decyzyjne
6.2. Implementacja tablic decyzyjnych w Haskellu
6.3. Analiza systemów regulowych
6.4. Podsumowanie

7. Modelowanie systemów czasu rzeczywistego
7.1. Czas w instrukcjach języka Alvis
7.2. Czas realizacji instrukcji
7.3. SR-grafy
7.4. Semantyka przejść
7.5. Podsumowanie

8. Modelowanie dynamiki otoczenia
8.1. Porty graniczne
8.2. Diagramy komunikacji z portami granicznymi
8.3. Stan modelu
8.4. Semantyka przejść
8.5. Iteracyjne konstruowanie modeli
8.6. Podsumowanie

9. Weryfikacja
9.1. Ograniczony rachunek
9.2. CADP evaluator
9.3. Funkcje filtrujące
9.4. Podsumowanie

10. Wnioski końcowe

A. Programowanie funkcyjne w języku Haskell
A.1. Podstawy programowania i środowisko pracy
A.2. Definiowanie funkcji
A.3. Listy
A.4. Krotki
A.5. Definiowanie typów danych

B. Oprogramowanie
B.1. AWisEditor
B.2. Alvis Translator
B.3. GHC - The Glasgow Haskell Compiler
B.4. CADP
B.5. dot

Spis ważniejszych symboli

Literatura

Skorowidz