plik

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:

;

INIT

wprowadzona_liczba

;

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=

: pierwsze;

wprowadzona_liczba!=

& blokada=zamkniety : zamkniety;

wprowadzona_liczba=

& blokada=pierwsze : drugie;

wprowadzona_liczba!=

& wprowadzona_liczba!=

& blokada=pierwsze : zamkniety;

wprowadzona_liczba!=

& wprowadzona_liczba!=

& blokada=drugie : zamkniety;

wprowadzona_liczba=

& blokada = drugie : trzecie;

wprowadzona_liczba!=

& wprowadzona_liczba!=

& blokada= trzecie : zamkniety;

wprowadzona_liczba=

& blokada = trzecie : otwarty;

wprowadzona_liczba!=

& 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 :

;

licznik_r :

;

Rysunek 5: Deklaracja zmiennych

ASSIGN

init

(miesiac) :=

;

next

(miesiac) :=

case

miesiac<

: miesiac+

;

miesiac=

;

esac

;

Rysunek 6: Zmiana miesięcy

init

(licznik_r) :=

;

next

(licznik_r) :=

case

miesiac!=

: licznik_r;

licznik_r=

;

miesiac=

: licznik_r+

;

esac

;

Rysunek 7:Zliczanie lat

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

, miesiac=

];



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

(miesiac=

miesiac=

)



Typ: osiągalność



Wynik: true



Opis: Styczeń zawsze w końcu przejdzie do grudnia

(licznik_r=

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

((

licznik_r=

miesiac=

) ->

(

rok=zwykly &

miesiac=

));



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 :

;

maxtime :

;

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

;

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

;

SYNACK_serwer=

FALSE

;

esac

;

init

(ACK):=

FALSE

;

next

(ACK):=

case

SYNACK=

TRUE

;

SYNACK=

FALSE

;

esac

;

Rysunek 11: Hanshaking po stronie klienta

init

(SYN):=

FALSE

;

next

(SYN):=

case

SYN_klient=

TRUE

: {

TRUE

FALSE

};

SYN_klient=

FALSE

;

esac

;

init

(SYNACK):=

FALSE

;

next

(SYNACK):=

case

SYN=

TRUE

;

SYN=

FALSE

;

esac

;

init

(ACK):=

FALSE

;

next

(ACK):=

case

ACK_klient=

TRUE

;

ACK_klient=

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

;

rozlacz=

TRUE

FALSE

;

rozlacz=

FALSE

& klient_polaczony=

TRUE

;

next

(SYN_klient)=

TRUE

FALSE

;

SYN_klient=

TRUE

| SYNACK=

TRUE

| SYNACK_klient=

TRUE

| ACK_klient=

TRUE

| SYN=

TRUE

FALSE

;

TRUE

;

esac

;

Rysunek 13: Połączenie serwera

init

(klient_polaczony):=

FALSE

;

next

(klient_polaczony):=

case

rozlacz=

TRUE

FALSE

;

serwer_polaczony=

TRUE

;

TRUE

FALSE

;

esac

;

Rysunek 14: Połączenie klienta

init

(maxtime):=

;

next

(maxtime):= maxtime;

init

(clock):=

;

next

(clock):=

case

clock>maxtime :

;

klient_polaczony=

TRUE

:clock+

;

klient_polaczony=

FALSE

;

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=

FALSE

;

klient_polaczony=

TRUE

& clock=maxtime :

TRUE

;

klient_polaczony=

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

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

(klient_inst.SYN=tak ->

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

(serwer_inst.SYN=tak ->

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

(serwer_inst.serwer_polaczony=tak ->

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

(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

(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

(serwer_inst.rozlacz=tak ->

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

(serwer_inst.clock=(serwer_inst.maxtime +

)->

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