PWiR lab 3: Spin - weryfikacja
Literatura
Pytania
Cel
- zaznajomienie się ze środowiskami graficznymi dla spina
- weryfikacja prostych własności: blokada, asercje, livelock
- weryfikacja własności wyrażonych w LTL, wzmianka o konstrukcji never { ... }
- głębsze poznanie Promeli
Spis treści
- Pliki, z których będziemy korzystać
- Dyskusja rozwiązań zadania o kanibalach
- Środowisko graficzne ispin
- Środowisko graficzne jspin (opcjonalnie)
- Acceptance cycles
- Wzajemne wykluczanie - weryfikacja z użyciem formuł LTL (ćwiczenie samodzielne)
- Protokół ABP (ćwiczenie samodzielne)
Pliki, z których będziemy korzystać
W niniejszym scenariuszu będziemy korzystać z następujących przykładowych
programów (do pobrania tutaj):
- increment-par.pml
- 2 procesy inkrementujące zmienną globalną w przeplocie.
- step7-chan.pml
- Komunikacja przez kanały.
- cannibals.pml
- Rozwiązanie zadania o kanibalach.
- peterson.pml
- Algorytm Petersona.
- abp.pml
- Alternating Bit Protocol.
Dyskusja rozwiązań zadania o kanibalach
Zwrócić uwagę na użycie atomic{ ... }.
Środowisko graficzne ispin
- Uruchomic ispin, otworzyc plik, np. increment-par.pml
- Zakładka Edit/View
- Można używać zewnętrznego edytora i przycisku Reopen
- Syntax-check: parsuje program w Promeli
- Check Redundancies: dokonuje analizy programu (metoda: slicing), próbując wykryć zmienne/instrukcje obojętne dla sprawdzanych własności.
- Dodać np. assert (finish>=0); na poczatku WaitForFinish albo assert (n>=10); na koncu, jak poprzednio
- Zakładka Simulate/Reply
- Przy symulacji losowej trzeba jawnie podać seed
- Odznaczyć lub zaznaczyć Track Data Values, po prawej wcisnąć Run
- W oknie na dole można skakać po krokach symulacji, można przewijać do początku itd.
- Output filtering: można oglądać tylko niektóre procesy/zmienne. Wyrażenia regularne, tzn. np. 1|2
- MSC: załadować step7-chan.pml, uruchomić symulację. Pojawi się Message Sequence Chart oparty na kanałach. Klikajac w cegiełki
mozna skoczyć w odpowiednie miejsce symulacji.
- Zakładka Verification
- Przy opcjach domyślnych wcisnąć Run.
- Przećwiczyć veryfikację poprawności zakończenia procesów (braku blokady) (np: finish == 3 w
increment-par.pml) i asercji (juz było)
- Wczytać cannibals.pml i wykonać weryfikację asercji. Uwaga: trzeba wyłaczyć sprawdzanie end states.
- Asercje xr, xs: dotyczą kanałów (wyłączność na czytanie / pisanie do kanałów)
- Dotychczas były proste własności bezpieczeństwa (ang. safety properties, something (bad) will never happen).
Teraz własności żywotności (ang. liveness properties, something (good) will ewentually happen).
- Non-progress cycles: w każdym nieskończonym obliczeniu, procesy napotkają etykietę progress...: nieskończenie wiele
razy. Wczytaj plik peterson.pml i sprawdź, że spin wygrywa non-progress cycle. Zmien etykietę again: na progress_again:
i sprawdź ponownie.
- to samo przy załozeniu weak fairness: Wynik: trochę dłuższy cykl.
- Acceptance cycles: weryfikator zgłosi błąd, jeśli jest możliwe, że w obliczeniu procesy nieskonczenie wiele razy odwiedzą etykietę accept...:
Środowisko graficzne jspin
Powtórz powyższe eksperymenty w jspinie. Zwróć uwagę na podobieństwa i różnice.
Acceptance cycles
W jspinie, wpisz w okienko LTL formula przykładową formułę, a następnie naciśnij Translate.
Zobaczysz automat odpowiadający negacji formuły. Słowo kluczowe never należy rozumieć tak, że
automat opisuje zachowanie systemu, które nigdy nie powinno mieć miejsca. Czyli jeśli takie zachowanie faktycznie jest możliwe, to jest to błąd
i może zostać zwrócone przez spina jako kontrprzykład na poporawność systemu.
(Negowanie formuł można wyłączyć w menu Settings/Negate LTL.)
Spróbuj zrozumieć odpowiedniość między formułą a automatem.
Równoważnie, z linii komend:
> spin -a -f "negacja formuły"
Wzajemne wykluczanie - weryfikacja z użyciem formuł LTL (ćwiczenie samodzielne)
Otwórz plik peterson.pml albo swoją implementację wzajemnego wykluczania.
Dla każdej z poniższych własności napisz odpowiednią formułę LTL i wykonaj weryfikację (acceptance cycles).
Sprawdź, czy opcja weak fairness zmienia wynik weryfikacji?
(Chyba najlepiej napisać formuły wraz ze studentami na tablicy, przynajmniej niektóre.)
- Wzajemne wykluczanie: w sekcji krytycznej zawsze jest co najwyżej jeden proces.
- Brak zagłodzenia: jesli proces rozpocznie protokół (flag[_pid] = 1), to w koncu wejdzie do sekcji krytycznej.
- Brak blokady: jeśli jeden z procesów zakończy się poza sekcją krytyczną (i protokołem), to drugi zawsze będzie mógł wejść do sekcji krytycznej, o ile będzie chciał.
- Podpowiedź: jest tu kilka możliwości. Po pierwsze można użyc niedeterminizmu, przed rozpoczęciem protokołu sekcji krytycznej:
if
:: skip
:: true -> false
fi
aby wybrać, czy proces kontynuuje, czy się ,,zawiesza''.
Po drugie można użyć dodatkowych zmiennych. Po trzecie, można użyc predykatu nazwa_procesu@etykieta w formule LTL. Np. formuła
[] proces@etykieta
mówi, że proces proces pozostaje na zawsze w etykiecie etykieta:. (Uwaga: być może trzeba wyłączyć weak fairness!)
- Ograniczone wyprzedzanie: podczas gdy jeden z procesów czeka na wejście do sekcji krytycznej, drugi proces nie wejdzie do niej dwukrotnie.
- Podpowiedź: użyj U.
- Przykładowe rozwiązanie:
ltl { [] (flag[0] == 1) -> (!(cs[1]) U ( (cs[1]) U (!(cs[1]) U (cs[0])))) }
Protokół ABP (ćwiczenie samodzielne)
Obejrzyj plik abp.pml -- opisuje protokół działający na łączu z błedami (utraty komunikatów).
Predefiniowana zmienna timeout służy do wykrycia globalnej blokady. Typ wyliczeniowy mtype. Inline.
Zweryfikuj Non-progress cycles.
Gdzie należy umieścić etykietę progress: ? Wynik weryfikacji powinien być negatywny.
Następnie zmodyfikuj schemat strat komunikatów tak, żeby dokładnie co trzeci komunikat dochodził do celu. Czy wynik weryfikacji jest inny?
Samodzielnie dokonaj którejś spośród poniższych modyfikacji:
- W obecnej wersji straty pojawiają się tylko na kanale nadawca --> odbiorca, a kanał powrotny, służący do przesyłania potwierdzeń, jest bezbłędny.
Dodaj straty na na kanale powrotnym.
- Pojemność obydwu kanałów wynosi 1. Zmodyfikuj model tak, żeby:
- pojemność kanałów była dowolna (zdefiniowana w #define),
- możliwe były dowolne opoźnienia w przesyłaniu komunikatów, np. po wysłaniu 3 komunikatów przez nadawcę możliwe jest, że odbiorca wciąż nie widzi żadnego z nich, choć wcale nie zaginęły
- poza opóźnieniami, możliwe były wciąż straty komunikatów
- Rola nadawcy i odbiorcy nie jest symetryczna: nadawca wykonuje retransmisje, podczas gdy odbiorca biernie czeka na następny komunikat. Zmodyfikuje odbiorcę tak, żeby był symetryczny względem nadawcy.
Ostatnia modyfikacja: 02/03/2013