Grupa laboratoryjna: ŚR 13:15 Wrocław, 1 czerwca 2016 r.
inż. Michał Polański, nr albumu: 200852
Data oddania:
inż. Elżbieta Tchorowska, nr albumu: 171067
Modelowa weryfikacja systemów w UPPAAL
Modelowanie i analiza systemów informatycznych  Logika temporalna i automaty czasowe
Wydział Elektroniki | Politechnika Wrocławska
Prowadzący:
dr inż. Paweł Głuchowski
Zadanie 1. W zadaniu należało wykonać model systemu zawierającego:
" szablon serwera (1 instancja);
" szablon klienta (określona liczba instancji);
" szablon sesji (liczba instancji tyle, co szablon klienta).
Zachowanie systemu:
1. Połączenie klienta przy pomocy procedury handshakingu (jednocześnie tylko jeden klient może nawiązywać
połączenie z serwerem);
2. Uruchomienie automatu sesji przez serwer dla zalogowanego klienta;
3. Klient przez losowo określony czas minimalny i zadany czas maksymalny jest połączony z sesją;
4. Klient rozłącza się z sesją, która przechodzi w stan nieaktywny;
Należy wykorzystać m.in. następujące elementy:
" jednokierunkowe lub dwukierunkowe synchronizowanie automatów przy pomocy odpowiednich kanałów;
" określenie dozwolonego i nakazanego czas aktywności stanu przy pomocy zegara, dozoru przejścia i niezmien-
nika stanu;
" losowanie czasu aktywności stanu przy pomocy pola select w opisie przejścia.
Rozwiązanie:
W wykonanym systemie synchronizacja pomiędzy klientem (rys. 1a), a serwerem (rys. 1b), czyli procedura
handshakingu, została wykonana za pomocą kanałów SYN, SYNACK oraz ACK. W ten sposób tylko jeden klient może
nawiązywać połączenie w danym czasie. Podczas tej procedury klient zapisuje swojeidw zmiennejcurrent_client,
przez co serwer może aktywować odpowiednią sesję dla użytkownika.
Komunikacja pomiędzy instancjami sesji (rys. 1c), a serwerem zrealizowana jest poprzez globalny kanał roz-
głoszeniowy run_session. Wprowadzenie tablicy status zawierającej dane pomocnicze dla akcji w systemie oraz
polom guard pozwala na aktywowanie przez serwer odpowiedniej sesji pomimo używania kanału rozgłoszeniowego.
W momencie, kiedy klient zostanie podłączony, losuje on liczbę całkowitą z zakresu [0,maxtime], a następnie
przypisuje ją do zmiennej mintime oraz zeruje lokalny zegar timer. Kiedy czas osiągnie wartość mintime wyjście
(przejście) ze stanu connected może zostać odpalone. Z powodu dodania niezmiennika stanu (timer <= maxtime),
automat nie może zostać w tym czasie dłużej niż określa to stała maxtime. Klient następnie ustawia odpowiednią
wartość w tablicy status oraz używa kanału rozgłoszeniowego close_session w celu zamknięcia swojej sesji.
Tabela 1: Znaczenie wartości w tablicy status.
Wartość Opis
status[x] = 0 Sesja o id = x jest nieaktywna
status[x] = 1 Klient o id = x połączył się z serwerem
status[x] = 2 Sesja o id = x jest aktywna
status[x] = 3 Klient o id = x rozłączył się
Deklaracje lokalne: 
Deklaracje lokalne: clock timer; int mintime;
Parametry: 
Parametry: const int[0,num_clients-1] id
(b) Szablon automatu serwera  Server.
(a) Model automatu klienta  Client.
Deklaracje lokalne: 
Parametry: const int[0,num_clients-1] id
(c) Model automatu sesji  Session.
Rysunek 1: Szablony automatów dostępnych w systemie.
2
Listing 1: Deklaracje globalne.
const int maxtime = 30;
const int num_clients = 3;
chan SYN, SYNACK, ACK;
broadcast chan run_session, close_session;
int[0,num_clients-1] current_client;
int status[num_clients] = {0, 0, 0};
Listing 2: Deklaracje instancji automatów.
system Client, Server, Session;
Poprzez nieuzupełnienie parametru stałej całkowitej id o określonym zakresie dla automatów klienta i sesji,
program UPPAAL automatycznie utworzy odpowiednią ilość instancji tych automatów. Zakres ten wyznacza stała
num_clients.
Zadanie 2. Przeprowadz
weryfikację zbudowanego modelu badając jego własności typu bezpieczeństwo, osią-
galność oraz żywotność.
Dla każdej własności podaj:
" typ,
" opisującą ją formułę CTL (zgodnie ze składnią UPPAAL),
" intuicyjne znaczenie (słownie),
" wynik automatycznej weryfikacji.
1. Możliwość wystąpienia blokady w systemie.
" Typ: osiągalność;
" Formuła CTL: E<> deadlock;
" Wynik: własność nie jest prawdziwa.
2. Procedura handshakingu może zostać przeprowadzona pomyślnie.
" Typ: osiągalność;
" Formuła CTL: E<> Server.handshake_success;
" Wynik: własność jest prawdziwa.
3. Czy sesja może stać się aktywna?
" Typ: osiągalność;
" Formuła CTL: E<> forall (i:int[0,2]) Session(i).active
" Wynik: własność jest prawdziwa.
4. Nigdy więcej niż jeden klient nie może naraz łączyć się z serwerem.
" Typ: bezpieczeństwo;
" Formuła CTL: A[] forall (i:int[0,2]) forall (j:int[0,2]) Client(i).connecting &&
Client(j).connecting imply i==j;
" Wynik: własność jest prawdziwa.
5. Klient może być nieaktywny, kiedy jego czas połączenia z serwerem trwał krócej niż mintime.
" Typ: osiągalność;
" Formuła CTL: E<> forall (i:int[0,2]) Client(i).inactive &&
Client(i).timer < Client(i).mintime
3
" Wynik: własność nie jest prawdziwa.
6. Po zakończeniu procedury handshakingu, musi zostać uruchomiona sesja.
" Typ: żywotność;
" Formuła CTL: Server.handshake_success --> exists (i:int[0,2]) Session(i).active
" Wynik: własność jest prawdziwa.
7. Rozłączanie się klienta powoduje zamknięcie sesji.
" Typ: żywotność;
" Formuła CTL: Client(0).disconnecting --> Session(0).inactive (poprawne dla każdego klienta)
" Wynik: własność jest prawdziwa.
8. Czy klient może być połączony dłużej niż maxtime?
" Typ: osiągalność;
" Formuła CTL: E<> forall (i:int[0,2]) Client(i).connected &&
Client(i).timer > maxtime
" Wynik: własność nie jest prawdziwa.
9. Czy może pozostać niezamknięta sesja, kiedy klienci są rozłączeni?
" Typ: osiągalność;
" Formuła CTL: E<> forall (i:int[0,2]) forall (j:int[0,2])
Client(i).inactive && Session(j).active
" Wynik: własność nie jest prawdziwa.
10. Czy serwer może być stale nieobciążony?
" Typ: bezpieczeństwo;
" Formuła CTL: E[] Server.waiting
" Wynik: własność jest prawdziwa.
4