Grupa laboratoryjna: ŚR 13:15

inż. Michał Polański, nr albumu: 200852
inż. Elżbieta Tchorowska, nr albumu: 171067

Wrocław, 1 czerwca 2016 r.

Data oddania:

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 swoje id w zmiennej current_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: clock timer; int mintime;

Parametry: const int[0,num_clients-1] id

(a) Model automatu klienta – Client.

Deklaracje lokalne: —

Parametry: —

(b) Szablon automatu serwera – Server.

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.

Przeprowadź 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