PWiR lab 3: Spin - weryfikacja

Literatura

• G. J. Holzmann, “The Spin Model Checker: Primer and Reference Manual”, Addison-Wesley 2004.
• M. Ben-Ari, “Principles of the Spin Model Checker”, Springer 2008.
• Strona internetowa wykładu Weryfikacja wspomagana komputerowo, 2010/2011 (serdeczne podziękowania dla Bartka Klina i Darii Walukiewicz za udostępnienie materiałów z laboratorium).
• Strona internetowa narzędzia Spin

Pytania

• Sławomir Lasota

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

1. Pliki, z których będziemy korzystać
2. Dyskusja rozwiązań zadania o kanibalach
3. Środowisko graficzne ispin
4. Środowisko graficzne jspin (opcjonalnie)
5. Acceptance cycles
6. Protokół ABP - weryfikacja z użyciem formuł LTL (ćwiczenie samodzielne)
7. Protokół ABP - modyfikacja (ćwiczenie samodzielne)
8. Wzajemne wykluczanie - weryfikacja z użyciem formuł LTL (ć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{ ... } oraz na makra. Wynik preprocesora można obejrzeć za pomocą spin -I cannibals.pml.

Środowisko graficzne ispin

1. Uruchomic ispin, otworzyc plik, np. increment-par.pml
2. 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
3. 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.
4. 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łączyć 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 wykrywa 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 nieskończenie 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"

Protokół ABP - weryfikacja z użyciem formuł LTL (ć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. Znów przydatne może być spin -I.

Zweryfikuj Non-progress cycles. Gdzie należy umieścić etykietę progress: ? Wynik weryfikacji powinien być negatywny.

Zweryfikuj własność żywotności: jeśli nadawca wyśle komunikat, to odbiorca w końcu go odbierze. (Należy przedyskutować, przy jakich założeniach własność zachodzi?)

Protokół ABP - modyfikacja (ćwiczenie samodzielne)

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:

1. 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.
2. 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
3. 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.

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?

1. Wzajemne wykluczanie: w sekcji krytycznej zawsze jest co najwyżej jeden proces.
2. Brak zagłodzenia: jesli proces rozpocznie protokół (flag[_pid] = 1), to w koncu wejdzie do sekcji krytycznej.
3. 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 jest tutaj

Ostatnia modyfikacja: 05/03/2014