Grupa laboratoryjna: ŚR 13:15

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

Wrocław, 18 maja 2016 r.

Data oddania:

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

Wykonanie w programie UPPAAL automatu generatora cyfr losowych z zakresu [0, 9] wraz z auto-

matem cyfrowego zamka otwierającego się po wprowadzeniu dowolnego ciągu cyfr kończącego się sekwencją 1783.

Rozwiązanie:

W wykonanym systemie synchronizacja pomiędzy dwoma automatami, generatorem (rys. 1.) i zamkiem (rys.

2.), zrealizowana jest poprzez globalny kanał pilny wprowadzono. Dzięki temu reakcja automatu odbiorcy (zamka)
jest natychmiastowa. Generator posiada 10 przejść zmieniających wartość zmiennej globalnej cyfra na liczby z
zakresu [0, 9]. Po wyborze cyfry automat przechodzi w stan committed, który jest natychmiast opuszczany powodując
odpowiednie przejście po stronie automatu zamek.

Rysunek 1: Model automatu generator.

Rysunek 2: Model automatu zamek.

W szczególnym przypadku, kiedy automat zamek znajdzie się w stanie otwarty (został wprowadzony prawidłowy

kod zamka) oraz generator wylosuje kolejną cyfrę, nastąpi stan blokady, ponieważ nie będzie możliwe odpalenie
żadnego przejścia zsynchronizowanego kanałem wprowadzono.

Listing 1: Deklaracje zmiennych globalnych.

int [0 ,9] cyfra;
urgent chan wprowadzono ;

Listing 2: Deklaracje instancji automatów.

P1 = generator ();

P2 = zamek ();

// System skladajacy sie z generatora oraz zamka

system P1 , P2;

Sprawdzenie w weryfikatorze:

• możliwości otworzenia zamka: E<> P2.otwarty (własność jest prawdziwa);
• możliwości wystąpienia stanu blokady w systemie: E<> deadlock (własność jest prawdziwa).

.

2