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.










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.

MODULE

generator

VAR

wprowadzona_liczba:

0

..

9

;

INIT

wprowadzona_liczba

in

0

..

9

;

Rysunek 1: Moduł generator

Model zdefiniowany pośrednio na podstawie schematu:

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 znaleźć 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ą:

Rysunek 2: Schemat modułu zamek

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

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).

MODULE

main

VAR

gen : generator;

zam: zamek(gen.wprowadzona_liczba);

DEFINE

succed := zam.blokada = otwarty;

ASSIGN

Rysunek 4: Moduł main

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.

W pierwszym kroku zmieniają się miesiące od wartości 1 (styczeń) do wartości 12 (grudzień):











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:











Zmienna licznik_r powiększa się o 1 raz do roku. Zwiększanie następuje już w miesiącu nr 11
(listopadzie), gdyż opóź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.

MODULE

main

VAR

rok : {zwykly,przestepny};

miesiac :

1

..

12

;

licznik_r :

1

..

4

;

Rysunek 5: Deklaracja zmiennych

ASSIGN

init

(miesiac) :=

1

;

next

(miesiac) :=

case

miesiac<

12

: miesiac+

1

;

miesiac=

12

:

1

;

esac

;

Rysunek 6: Zmiana miesięcy

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

W chwili, gdy licznik_r osiągnie wartość 4, opis roku zmienia się ze zwykłego na przestępny:










Osiągalna ścieżka stanów:

init

(rok) := zwykly;

next

(rok) :=

case

licznik_r<

4

: zwykly;

licznik_r=

4

: przestepny;

esac

;

Rysunek 8: Zmiana stanu roku

-- Loop starts here
-> State: 1.1 <-
rok = zwykly
miesiac = 1
licznik_m = 1
licznik_r = 1
-> State: 1.2 <-
miesiac = 2
licznik_m = 2
-> State: 1.3 <-
miesiac = 3
licznik_m = 3
-> State: 1.4 <-
miesiac = 4
licznik_m = 4
-> State: 1.5 <-
miesiac = 5
licznik_m = 5
-> State: 1.6 <-
miesiac = 6
licznik_m = 6
-> State: 1.7 <-
miesiac = 7
licznik_m = 7
-> State: 1.8 <-
miesiac = 8
licznik_m = 8
-> State: 1.9 <-
miesiac = 9
licznik_m = 9
-> State: 1.10 <-
miesiac = 10
licznik_m = 10
-> State: 1.11 <-
miesiac = 11
licznik_m = 11
-> State: 1.12 <-
miesiac = 12
licznik_m = 12
licznik_r = 2
-> State: 1.13 <-
miesiac = 1
licznik_m = 1
-> State: 1.14 <-
miesiac = 2
licznik_m = 2
-> State: 1.15 <-
miesiac = 3
licznik_m = 3
-> State: 1.16 <-
miesiac = 4
licznik_m = 4
-> State: 1.17 <-
miesiac = 5
licznik_m = 5
-> State: 1.18 <-
miesiac = 6
licznik_m = 6
-> State: 1.19 <-
miesiac = 7
licznik_m = 7

-> State: 1.20 <-
miesiac = 8
licznik_m = 8
-> State: 1.21 <-
miesiac = 9
licznik_m = 9
-> State: 1.22 <-
miesiac = 10
licznik_m = 10
-> State: 1.23 <-
miesiac = 11
licznik_m = 11
-> State: 1.24 <-
miesiac = 12
licznik_m = 12
licznik_r = 3
-> State: 1.25 <-
miesiac = 1
licznik_m = 1
-> State: 1.26 <-
miesiac = 2
licznik_m = 2
-> State: 1.27 <-
miesiac = 3
licznik_m = 3
-> State: 1.28 <-
miesiac = 4
licznik_m = 4
-> State: 1.29 <-
miesiac = 5
licznik_m = 5
-> State: 1.30 <-
miesiac = 6
licznik_m = 6
-> State: 1.31 <-
miesiac = 7
licznik_m = 7
-> State: 1.32 <-
miesiac = 8
licznik_m = 8
-> State: 1.33 <-
miesiac = 9
licznik_m = 9
-> State: 1.34 <-
miesiac = 10
licznik_m = 10
-> State: 1.35 <-
miesiac = 11
licznik_m = 11
-> State: 1.36 <-
miesiac = 12
licznik_m = 12
licznik_r = 4
-> State: 1.37 <-
rok = przestepny
miesiac = 1
licznik_m = 1
-> State: 1.38 <-
miesiac = 2
licznik_m = 2

-> State: 1.39 <-
miesiac = 3
licznik_m = 3
-> State: 1.40 <-
miesiac = 4
licznik_m = 4
-> State: 1.41 <-
miesiac = 5
licznik_m = 5
-> State: 1.42 <-
miesiac = 6
licznik_m = 6
-> State: 1.43 <-
miesiac = 7
licznik_m = 7
-> State: 1.44 <-
miesiac = 8
licznik_m = 8
-> State: 1.45 <-
miesiac = 9
licznik_m = 9
-> State: 1.46 <-
miesiac = 10
licznik_m = 10
-> State: 1.47 <-
miesiac = 11
licznik_m = 11
-> State: 1.48 <-
miesiac = 12
licznik_m = 12
licznik_r = 1
-> State: 1.49 <-
rok = zwykly
miesiac = 1
licznik_m = 1

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”.

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).

Łączenie się za pomocą handshakingu wygląda następująco po stronach obu modułów:

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 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.

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

;

Po pozytywnym przejściu handshakingu (ACK po stronie serwera na TRUE) zostaje uruchomione
połączenie, również po stronie 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:













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

(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

init

(klient_polaczony):=

FALSE

;

next

(klient_polaczony):=

case

rozlacz=

TRUE

:

FALSE

;

serwer_polaczony=

TRUE

:

TRUE

;

TRUE

:

FALSE

;

esac

;

Rysunek 14: Połączenie klienta

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:













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:

Symulacje przedstawionego wyżej modelu:

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

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

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

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