Grupa laboratoryjna: ŚR 13:15 Wrocław, 18 maja 2016 r.
inż. Michał Polański, nr albumu: 200852
Data oddania:
inż. Elżbieta Tchorowska, nr albumu: 171067
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