Grupa laboratoryjna: ÅšR 13:15
Wrocław, 07 czerwiec 2016 r.
inż. Michał Polański, nr albumu: 200852
Data oddania:
inż. Elżbieta Tchorowska, nr albumu: 171067
Modelowa weryfikacja systemów w NuSMV
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.
Zbuduj model systemu złożonego z generatora losowych cyfr z zakresu od 0 do 9 i z automatu cyfrowego
zamka, który otwiera się po wprowadzeniu dowolnego ciągu cyfr kończącego się sekwencją 1783. Generator i
zamek powinny być osobnymi modułami. Zmienność zmiennych stanowych dla generatora zdefiniuj
bezpośrednio, a dla zamka zdefiniuj pośrednio.
RozwiÄ…zanie:
Model składa się z 3 modułów: generatora, zamka i modułu MAIN, który steruje dwoma pierwszymi
modułami. Do zaprojektowania systemu wykorzystano grafy użyte w laboratorium 1.
Moduł generator został zdefiniowany bezpośrednio. Odpowiada jedynie za wybranie cyfry z przedziału
od 0 do 9.
MODULE generator
VAR
wprowadzona_liczba: 0..9;
INIT wprowadzona_liczba in 0..9;
Rysunek 1: Moduł generator
Moduł zamek został stworzony jako moduł z parametrem, gdyż wartość wybrana w module generator
musi zostać przekazana do zamka. Poniżej przedstawiono graf modelu wykonany na laboratorium
pierwszym.
Rysunek 2: Schemat modułu zamek
Model zdefiniowany pośrednio na podstawie schematu:
MODULE zamek (wprowadzona_liczba)
VAR
blokada : {zamkniety, pierwsze, drugie, trzecie, otwarty};
ASSIGN
init(blokada):= zamkniety;
next(blokada):= case
wprowadzona_liczba=1 : pierwsze;
wprowadzona_liczba!=1 & blokada=zamkniety : zamkniety;
wprowadzona_liczba=7 & blokada=pierwsze : drugie;
wprowadzona_liczba!=1 & wprowadzona_liczba!=7 & blokada=pierwsze : zamkniety;
wprowadzona_liczba!=1 & wprowadzona_liczba!=8 & blokada=drugie : zamkniety;
wprowadzona_liczba=8 & blokada = drugie : trzecie;
wprowadzona_liczba!=1 & wprowadzona_liczba!=3 & blokada= trzecie : zamkniety;
wprowadzona_liczba=3 & blokada = trzecie : otwarty;
wprowadzona_liczba!=1 & blokada = otwarty : zamkniety;
esac;
Rysunek 3: Moduł zamek
Zmienna blokada definiuje wszystkie możliwe stany samej blokady zamka. Na początku zamek jest
zamknięty. Wybierając kolejno poprawne cyfry przechodzi się przez stany: pierwsze, drugie i trzecie.
Po wybraniu wszystkich 4 prawidłowych cyfr, zamek powinien znalez
ć się w stanie otwarty. Zmienna
wprowadzona_liczba jest zmienną przekazywaną z modułu generator.
Ostatnim modułem w zadaniu jest moduł MAIN, który sprawia, że pozostałe dwa moduły
współpracują ze sobą:
MODULE main
VAR
gen : generator;
zam: zamek(gen.wprowadzona_liczba);
DEFINE succed := zam.blokada = otwarty;
ASSIGN
Rysunek 4: Moduł main
Zmienne gen i zam odpowiadają za przekazanie wartości poszczególnych modułów do modułu MAIN.
Zmienna gen.wprowadzona_liczba oznacza liczbę wybraną w module generator. Do modułu zamek
należy ją przekazać za pomocą nawiasów.
Zdefiniowano także stałą succed, która odpowiada jedynie za wyświetlenie komunikatu o otwarciu
zamka. Zadeklarowanie succed nie jest konieczne do poprawnego działania systemu, jednak
zdecydowano się na nią z powodów wizualizacyjnych.
W celu sprawdzenia poprawności działania modelu, zadeklarowano kilka formuł CTL.
COMPUTE MIN [zam.blokada=zamkniety, zam.blokada=otwarty]; is 4
COMPUTE MAX [zam.blokada=zamkniety, zam.blokada=otwarty]; is infinity
COMPUTE MIN [zam.blokada=otwarty, zam.blokada=zamkniety]; is 1
Wynika z nich, że:
- minimalna ścieżka otwarcia zamku wynosi 4, co jest prawdziwe. Najszybciej można otworzyć zamek
po wprowadzeniu 4 cyfr.
- najdłuższa ścieżka otwarcia zamku jest nieskończona  nie ma przymusu wprowadzenia poprawnej
kombinacji
- istnieje możliwość przejścia z zamka zamkniętego do zamka otwartego
- wystarczy wprowadzenie 1 cyfry, by zamek ze stanu otwartego przeszedł do stanu zamkniętego
Zadanie 2
Poniższy model roku jest niedokończony i błędny. Popraw i rozbuduj go, aby:
·ð rok przestÄ™pny nastÄ™powaÅ‚ po 3 zwykÅ‚ych latach;
·ð rok zaczynaÅ‚ siÄ™ w styczniu, a koÅ„czyÅ‚ w grudniu;
·ð miesiÄ…ce nastÄ™powaÅ‚y po sobie w prawidÅ‚owej kolejnoÅ›ci i bez powtórzeÅ„.
Następnie zweryfikuj poprawność działania modelu przy pomocy odpowiednich formuł. Dla każdej
formuły podaj: jej typ (bezpieczeństwo, osiągalność, żywotność itd.), jej język (LTL, CTL itd.) i jej
intuicyjne znaczenie (słownie).
RozwiÄ…zanie:
Zdecydowano się na stworzenie modelu jednomodułowego. Model ma odwzorowywać zmiany
miesięcy i lat (z uwzględnieniem lat przestępnych). Zdefiniowano 4 zmienne, które odpowiadają za
opis roku (czy jest przestępny czy zwykły), opis miesięcy (liczbowo od 1 do 12) oraz dwa liczniki,
które odpowiadają za liczenie miesięcy i lat.
MODULE main
VAR
rok : {zwykly,przestepny};
miesiac : 1..12;
licznik_r : 1..4;
Rysunek 5: Deklaracja zmiennych
W pierwszym kroku zmieniają się miesiące od wartości 1 (styczeń) do wartości 12 (grudzień):
ASSIGN
init(miesiac) := 1;
next(miesiac) := case
miesiac<12 : miesiac+1;
miesiac=12 : 1;
esac;
Rysunek 6: Zmiana miesięcy
Początkowym miesiącem jest styczeń. W następnych krokach miesiące zmieniają się poprzez dodanie
stałej 1, która powoduje zmianę miesiąca na następny. Dzieje się tak do momentu, aż miesiąc nie
będzie oznaczony wartością 12 (grudzień). Wtedy następnym miesiącem jest miesiąc oznaczony jako 1
(styczeń).
Za odpowiednie zliczanie lat odpowiada zmienna licznik_r:
init(licznik_r) :=1;
next(licznik_r) := case
miesiac!=11 : licznik_r;
licznik_r=4 : 1;
miesiac=11 : licznik_r+1;
esac;
Rysunek 7:Zliczanie lat
Zmienna licznik_r powiększa się o 1 raz do roku. Zwiększanie następuje już w miesiącu nr 11
(listopadzie), gdyż opóz
nienia czasowe na modelu spowodują, że w efekcie zmiana roku nastąpi
dopiero w styczniu. W chwili, gdy licznik_r =4 (wystąpił rok przestępny), następną wartością osiąganą
jest wartość 1, a więc powrót licznika_r do stanu pierwotnego.
W chwili, gdy licznik_r osiągnie wartość 4, opis roku zmienia się ze zwykłego na przestępny:
init(rok) := zwykly;
next(rok) := case
licznik_r<4 : zwykly;
licznik_r=4 : przestepny;
esac;
Rysunek 8: Zmiana stanu roku
Osiągalna ścieżka stanów:
-- Loop starts here -> State: 1.39 <-
-> State: 1.20 <-
-> State: 1.1 <- miesiac = 3
miesiac = 8
rok = zwykly licznik_m = 3
licznik_m = 8
miesiac = 1 -> State: 1.40 <-
-> State: 1.21 <-
licznik_m = 1 miesiac = 4
miesiac = 9
licznik_r = 1 licznik_m = 4
licznik_m = 9
-> State: 1.2 <- -> State: 1.41 <-
-> State: 1.22 <-
miesiac = 2 miesiac = 5
miesiac = 10
licznik_m = 2 licznik_m = 5
licznik_m = 10
-> State: 1.3 <- -> State: 1.42 <-
-> State: 1.23 <-
miesiac = 3 miesiac = 6
miesiac = 11
licznik_m = 3 licznik_m = 6
licznik_m = 11
-> State: 1.4 <- -> State: 1.43 <-
-> State: 1.24 <-
miesiac = 4 miesiac = 7
miesiac = 12
licznik_m = 4 licznik_m = 7
licznik_m = 12
-> State: 1.5 <- -> State: 1.44 <-
licznik_r = 3
miesiac = 5 miesiac = 8
-> State: 1.25 <-
licznik_m = 5 licznik_m = 8
miesiac = 1
-> State: 1.6 <- -> State: 1.45 <-
licznik_m = 1
miesiac = 6 miesiac = 9
-> State: 1.26 <-
licznik_m = 6 licznik_m = 9
miesiac = 2
-> State: 1.7 <- -> State: 1.46 <-
licznik_m = 2
miesiac = 7 miesiac = 10
-> State: 1.27 <-
licznik_m = 7 licznik_m = 10
miesiac = 3
-> State: 1.8 <- -> State: 1.47 <-
licznik_m = 3
miesiac = 8 miesiac = 11
-> State: 1.28 <-
licznik_m = 8 licznik_m = 11
miesiac = 4
-> State: 1.9 <- -> State: 1.48 <-
licznik_m = 4
miesiac = 9 miesiac = 12
-> State: 1.29 <-
licznik_m = 9 licznik_m = 12
miesiac = 5
-> State: 1.10 <- licznik_r = 1
licznik_m = 5
miesiac = 10 -> State: 1.49 <-
-> State: 1.30 <-
licznik_m = 10 rok = zwykly
miesiac = 6
-> State: 1.11 <- miesiac = 1
licznik_m = 6
miesiac = 11 licznik_m = 1
-> State: 1.31 <-
licznik_m = 11
miesiac = 7
-> State: 1.12 <-
licznik_m = 7
miesiac = 12
-> State: 1.32 <-
licznik_m = 12
miesiac = 8
licznik_r = 2
licznik_m = 8
-> State: 1.13 <-
-> State: 1.33 <-
miesiac = 1
miesiac = 9
licznik_m = 1
licznik_m = 9
-> State: 1.14 <-
-> State: 1.34 <-
miesiac = 2
miesiac = 10
licznik_m = 2
licznik_m = 10
-> State: 1.15 <-
-> State: 1.35 <-
miesiac = 3
miesiac = 11
licznik_m = 3
licznik_m = 11
-> State: 1.16 <-
-> State: 1.36 <-
miesiac = 4
miesiac = 12
licznik_m = 4
licznik_m = 12
-> State: 1.17 <-
licznik_r = 4
miesiac = 5
-> State: 1.37 <-
licznik_m = 5
rok = przestepny
-> State: 1.18 <-
miesiac = 1
miesiac = 6
licznik_m = 1
licznik_m = 6
-> State: 1.38 <-
-> State: 1.19 <-
miesiac = 2
miesiac = 7
licznik_m = 2
licznik_m = 7
Kilka formuł CTL w celu sprawdzenia poprawności modelu:
COMPUTE MIN [miesiac=1, miesiac=12];
·ð Typ: żywotność
·ð Wynik: 11
·ð Opis: ile miesiÄ™cy musi upÅ‚ynąć miÄ™dzy styczniem a grudniem
COMPUTE MAX [rok=zwykly, rok=przestepny];
·ð Typ: żywotność
·ð Wynik: 36
·ð Opis: Ile miesiÄ™cy trwa suma lat zwykÅ‚ych
AG (miesiac=1 -> AF miesiac=12)
·ð Typ: osiÄ…galność
·ð Wynik: true
·ð Opis: StyczeÅ„ zawsze w koÅ„cu przejdzie do grudnia
AG (licznik_r=4-> AX rok=przestepny)
·ð Typ: osiÄ…galność
·ð Wynik: true
·ð Opis: gdy licznik_r zmienia siÄ™ na 4, to nastÄ™pny miesiÄ…c jest miesiÄ…cem w roku
przestępnym
AG ((AG licznik_r=4 & AG miesiac=12) -> AG(AX rok=zwykly & AX miesiac=1));
·ð Typ: osiÄ…galność
·ð Wynik: true
·ð Opis: po grudniu w roku przestÄ™pnym nastÄ™puje styczeÅ„ roku zwykÅ‚ego
Zadanie 3
Zbuduj model systemu komunikacji klient serwer wg poniższych wskazówek:
·ð Stwórz moduÅ‚ serwera, majÄ…cy 1 instancjÄ™.
·ð Stwórz moduÅ‚ klienta, majÄ…cy 1 instancjÄ™.
·ð W module serwera stwórz zegar, liczÄ…cy czas trwania poÅ‚Ä…czenia.
·ð Zachowanie modelu powinno być nastÄ™pujÄ…ce:
1. Klient nawiązuje połączenie z serwerem przy pomocy procedury handshakingu (sekwencja
sygnałów SYN, SYN-ACK, ACK).
2. Serwer losowo decyduje o sukcesie tej procedury.
3. Klient przez losowo wybrany czas 2 do 5 jednostek jest połączony z serwerem.
4. Klient może rozłączyć się z serwerem w trakcie czasu 2 do 5 jednostek.
5. Serwer rozłącza klienta po upływie maksymalnego czasu połączenia.
W modelu wykorzystaj m.in. następujące elementy:
·ð wysyÅ‚anie sygnaÅ‚u (np. SYN) miÄ™dzy moduÅ‚ami przez zmianÄ™ wartoÅ›ci logicznej odpowiednich
dwóch zmiennych (w obu modułach), wykonywaną przez moduł wysyłający;
·ð okreÅ›lenie czasu poÅ‚Ä…czenia z serwerem przy pomocy jego zegara (zerowanego w momencie
nawiązania połączenia) i przy pomocy struktury case.
RozwiÄ…zanie:
Stworzono jedną instancję klienta w postaci modułu nazwanego  klient oraz jedną instancję serwera
w postaci modułu nazwanego  serwer .
MODULE klient(SYN_serwer, SYNACK_serwer, ACK_serwer, rozlacz, serwer_polaczony)
VAR
klient_polaczony: boolean;
SYN: boolean;
SYNACK: boolean;
ACK: boolean;
Rysunek 9: Zmienne modułu klient
MODULE serwer(SYN_klient, SYNACK_klient, ACK_klient, klient_polaczony)
VAR
clock : 0..6;
maxtime : 3..5;
serwer_polaczony:boolean;
rozlacz: boolean;
SYN: boolean;
SYNACK: boolean;
ACK: boolean;
Rysunek 10: Zmienne modułu serwer
W obu modułach umieszczono zmienne SYN, SYNACK i ACK, które odpowiadają za łączenie się
modułów za pomocą handshakingu. Możliwe stany, które mogą przyjąć te zmienne to TRUE i FALSE,
czyli sukces danego etapu połączenia lub jego brak. W obu modułach występują także zmienne
XXX_połączony, który odpowiada za status połączenia. W module serwer znajduje się także zmienna
rozlacz, która odpowiada za sygnał, który ma spowodować rozłączenie klienta z serwerem. Wszystkie
te zmienne są przekazywane za pomocą parametrów do drugiego modułu. Moduł serwer posiada także
zegar clock o wartościach od 0 do 6 (większa ilość była zbędna), a także maxtime, który przyjmuje
wartość od 3 do 5 i oznacza czas, w którym musi nastąpić rozłączenie. (Połączenie może trwać od 2 do
5 sekund).
A
ączenie się za pomocą handshakingu wygląda następująco po stronach obu modułów:
init(SYN):=TRUE;
next(SYN):= case
rozlacz=TRUE : TRUE;
SYN=FALSE & SYN_serwer=FALSE & SYNACK_serwer=FALSE & ACK_serwer=FALSE &
klient_polaczony=FALSE & SYNACK=FALSE & ACK=FALSE & serwer_polaczony=FALSE :
TRUE;
TRUE : FALSE;
esac;
init(SYNACK):=FALSE;
next(SYNACK):= case
SYNACK_serwer=TRUE :TRUE;
SYNACK_serwer=FALSE : FALSE;
esac;
init(ACK):=FALSE;
next(ACK):= case
SYNACK=TRUE : TRUE;
SYNACK=FALSE : FALSE;
esac;
Rysunek 11: Hanshaking po stronie klienta
init(SYN):=FALSE;
next(SYN):= case
SYN_klient=TRUE : {TRUE, FALSE};
SYN_klient=FALSE : FALSE;
esac;
init(SYNACK):=FALSE;
next(SYNACK):=case
SYN=TRUE: TRUE;
SYN=FALSE: FALSE;
esac;
init(ACK):=FALSE;
next(ACK):= case
ACK_klient=TRUE :TRUE;
ACK_klient=FALSE :FALSE;
esac;
Rysunek 12: Handshaking po stronie serwera
W stanie początkowym, wszystkie zmienne ustawione są na FALSE, z wyłączeniem sygnału SYN
klienta, co oznacza, że już od początku klient wysyła żądanie połączenia do serwera. Poprzez
przekazywanie zmiennych za pomocą parametrów, kolejno wartość sygnałów jest przekazywana
między modułami. W momencie wysłania przez klienta sygnału SYN, serwer ma dwie ścieżki do
wyboru: odpowiedzieć pozytywnie na sygnał lub negatywnie  w sposób losowy. W dalszych krokach,
handshaking przebiega bez zakłóceń. Sygnał SYN wysyłany jest przez klienta tylko w momencie, w
którym nie trwa obecnie procedura handshakingu ani połączenie nie trwa w chwili obecnej.
Po pozytywnym przejściu handshakingu (ACK po stronie serwera na TRUE) zostaje uruchomione
połączenie, również po stronie serwera:
init(serwer_polaczony):=FALSE;
next(serwer_polaczony):= case
ACK=TRUE : TRUE;
rozlacz=TRUE :FALSE;
rozlacz=FALSE & klient_polaczony=TRUE : TRUE;
next(SYN_klient)=TRUE :FALSE;
SYN_klient=TRUE | SYNACK=TRUE | SYNACK_klient=TRUE | ACK_klient=TRUE | SYN=TRUE
:FALSE;
TRUE: TRUE;
esac;
Rysunek 13: Połączenie serwera
Serwer łączy się w momencie, w którym ACK serwera znajdzie się w stanie TRUE i będzie trwał tak
długo, aż nie pojawi się sygnał rozlacz. Pozostałe procedury służą blokadzie połączenia serwera w
momencie, gdy trwa dopiero nawiązywanie połączenia lub model systemu jest w ogóle nieaktywny.
Połączenie po stronie klienta zostaje nawiązane dopiero po połączeniu serwera:
init(klient_polaczony):=FALSE;
next(klient_polaczony):= case
rozlacz=TRUE : FALSE;
serwer_polaczony=TRUE : TRUE;
TRUE: FALSE;
esac;
Rysunek 14: Połączenie klienta
Klient jest połączony w momencie, gdy serwer jest połączony, a rozłącza się wtedy, gdy z serwera
zostaje wysłany sygnał o rozłączeniu.
Sygnał rozłączenia zależy od zegara umieszczonego w module serwer.
init(maxtime):= 3..5;
next(maxtime):= maxtime;
init(clock):=0;
next(clock):= case
clock>maxtime : 0;
klient_polaczony=TRUE :clock+1;
klient_polaczony=FALSE : 0;
esac;
Rysunek 15: Zadeklarowanie maksymalnego czasu połączenia I zegara
W momencie, w którym klient jest połączony, zegar zwiększa się o 1 z każdym przejściem. W
momencie rozłączenia klienta, zegar wynosi zero. Dodatkowo wprowadzono zabezpieczenie przed
przekroczeniem zakresu licznika w postaci zerowania, kiedy clock przewyższy maxtime. Sygnał
rozłączenia wygląda następująco:
init(rozlacz):=FALSE;
next(rozlacz):= case
serwer_polaczony=TRUE & clock=0 :FALSE;
klient_polaczony=TRUE & clock=maxtime : TRUE;
klient_polaczony=FALSE :FALSE;
TRUE : FALSE;
esac;
Rysunek 16: Rozłączanie serwera
Rozłączenie następuje w momencie, gdy klient jest połączony, a zegar dojdzie do wartości maxtime. W
przypadku, gdy klient jest niepołączony nie ma możliwości wysłania sygnału rozłączenia. Dodatkowo
wprowadzono warunek przy zerowym stanie zegara, gdyż następowało wtedy samoistne rozłączenie.
Moduł serwer i klient zostały zadeklarowane w zmiennych modułu MAIN:
MODULE main
VAR
serwer_inst: serwer(klient_inst.SYN, klient_inst.SYNACK, klient_inst.ACK,
klient_inst.klient_polaczony);
klient_inst: klient(serwer_inst.SYN, serwer_inst.SYNACK, serwer_inst.ACK,
serwer_inst.rozlacz, serwer_inst.serwer_polaczony);
ASSIGN
Rysunek 17: Moduł MAIN
Symulacje przedstawionego wyżej modelu:
Rysunek 18: Wybór stanu początkowego (czasu maxtime)
W stanie 3.1 klient nawiązuje żądanie połączenia poprzez sygnał SYN. W stanie 3.2 serwer odrzuca
żądanie. W stanie 3.3, klient ponownie żąda połączenia, a w stanie 3.4 serwer zgadza się. Kolejne
stany, do 3.8 włącznie to łączenie się za pomocą handshakingu. W 3.9 stan serwera zmienia się na
połączony, w stanie 3.10 stan klienta zmienia się. W 3.11 zaczyna być liczony czas połączenia do stanu
3.13. W 3.14 zostaje wysłane żądanie rozłączenia przez serwer. W 3.15 serwer i klient przestają być
połączone, a klient ponownie wysyła żądanie SYN.
Zadanie 4
Przeprowadz
weryfikację zbudowanego modelu, aby zbadać, czy zachowuje się tylko prawidłowo,
badając spełnienie jego własności typu bezpieczeństwo, osiągalność, żywotność i inne.
Dla każdej własności podaj: jej typ (bezpieczeństwo, osiągalność, żywotność itp.), opisującą ją formułę
logiczną lub wyrażenie NuSMV (zgodnie ze składnią NuSMV) i jej intuicyjne znaczenie (słownie).
Uwaga: formuły wyrażające poprawne działanie powinny być zweryfikowane pozytywnie (true), a
formuły wyrażające niepoprawne działanie powinny być zweryfikowane negatywnie (false).
Uwaga: aby sprawdzić ilościowe parametry czasowe systemu, skorzystaj z polecenia COMPUTE.
Kilka formuł CTL w celu sprawdzenia poprawności modelu:
COMPUTE MIN [klient_inst.SYN=tak, klient_inst.klient_polaczony=tak];
·ð Typ: żywotność
·ð Wynik: 7
·ð Opis: ile jednostek czasu musi minąć od żądania poÅ‚Ä…czenia od klienta do nawiÄ…zania
połącznia (6 na handshaking i 1 na połączenie serwera)
COMPUTE MAX [klient_inst.klient_polaczony=tak, serwer_inst.rozlacz=tak];
·ð Typ: żywotność
·ð Wynik: 6
·ð Opis: ile maksymalnie jednostek czasu musi minąć od poÅ‚Ä…czenia klienta do wysÅ‚ania
żądania rozłączenia (5 na czas połączenia + 1 na rozłączenie)
SPEC AG(klient_inst.SYN=tak -> EX serwer_inst.SYN=tak);
·ð Typ: osiÄ…galność
·ð Wynik: true
·ð Opis: może zdarzyć siÄ™ możliwość, że wysÅ‚anie żądania SYN przez klienta zakoÅ„czy siÄ™
odpowiedziÄ… poprawnÄ… serwera
SPEC AG(serwer_inst.SYN=tak -> AF serwer_inst.ACK=tak);
·ð Typ: osiÄ…galność
·ð Wynik: true
·ð Opis: jeÅ›li serwer odpowiedziaÅ‚ sygnaÅ‚em SYN, to procedura handshakingu zostanie
wykonana i dojdzie do ostatniego kroku odpowiedzi ACK przez serwer
SPEC AF(serwer_inst.serwer_polaczony=tak -> AX klient_inst.klient_polaczony=tak)
·ð Typ: osiÄ…galność
·ð Wynik: true
·ð Opis: jeÅ›li nastÄ…piÅ‚o poÅ‚Ä…czenie po stronie serwera, to w nastÄ™pnym stanie zostanie
połączony klient
SPEC EF(klient_inst.SYN=tak & (serwer_inst.SYN=tak | serwer_inst.SYNACK=tak |
serwer_inst.ACK=tak));
·ð Typ: bezpieczeÅ„stwo
·ð Wynik: false
·ð Opis: nie jest możliwe wysÅ‚anie żądania poÅ‚Ä…czenia przez klienta, jeÅ›li poÅ‚Ä…czenie
jest już nawiązywane
SPEC EF(klient_inst.SYN=tak & klient_inst.klient_polaczony=tak);
·ð Typ: bezpieczeÅ„stwo
·ð Wynik: false
·ð Opis: nie jest możliwe wysÅ‚anie żądania poÅ‚Ä…czenia przez klienta, jeÅ›li poÅ‚Ä…czenie
już trwa
SPEC AG(serwer_inst.rozlacz=tak -> AF klient_inst.klient_polaczony=nie);
·ð Typ: osiÄ…galność
·ð Wynik: true
·ð Opis: kiedy zostanie wysÅ‚any sygnaÅ‚ rozÅ‚Ä…czenia z serwera, klient zostanie
rozłączony
SPEC AG(serwer_inst.clock=(serwer_inst.maxtime +1)-> AX serwer_inst.serwer_polaczony=nie);
·ð Typ: osiÄ…galność
·ð Wynik: true
·ð Opis: kiedy zegar przekroczy czas maksymalny poÅ‚Ä…czenia, w nastÄ™pnym kroku zostanie
rozłączony serwer