Rysunek 5.3: Interfejs programu Alvis2ModelChecker.
Na rysunku 5.4 przedstawiona została propozycja procesu weryfikacji modeli Alvis w narz˛edziu nuXmv, b˛ed ˛aca zmodyfikowan ˛a wersj ˛a procesu z rysunku 2.6.
5.3 Testy rozwi ˛azania
Przedstawione wy˙zej podej´scie zostało przetestowane zarówno na kilku prostych modelach Alvis, przykła-dach akademickich typu producent–konsument jak i na modelach rzeczywistych systemów krytycznych ze wzgl˛edu na bezpiecze´nstwo. W´sród tych ostatnich wyró˙zni´c nale˙zy model sterownika zwrotnicy tramwa-jowej wytworzonej przez grup˛e ZUE S.A. [122] i wykorzystywanej w transporcie publicznym w Krako-wie, Szczecinie i Wrocławiu [53] oraz model centrali sygnalizacji po˙zarowej, wytworzonego na podstawie projektu opublikowanego przez Stowarzyszenia In˙zynierów i Techników Po˙zarnictwa (SITP) [30]. Wi˛ecej informacji o tym drugim modelu mo˙zna znale´z´c w publikacji [17]. Natomiast w tej sekcji podej´scie zostanie głównie przedstawione wła´snie na przykładzie modelu zwrotnicy.
5.3.1 Opis systemu zwrotnicowego
Schemat modelowanego systemu został przedstawiony na rysunku 5.5.
W ka˙zdym tramwaju znajduje si˛e nadajnik podczerwieni (inaczej IR od ang. infrared) NP03, który jest wykorzystywany do wysyłania sygnałów z nadje˙zd˙zaj ˛acego pojazdu do systemu sterowania zwrotnic ˛a. Odbiornik OP03, umieszczony zazwyczaj na przewodzie jezdnym sieci trakcyjnej lub na osobnych słupkach
5.3. Testy rozwi ˛azania 63
1. Alvis Editor
diagram komunikacji + warstwa kodu
2. Alvis Compiler
Alvis → Posta´c po´srednia w Haskell
3. Kompilator GHC 4. Wykonanie programu Generacja grafu LTS 5. Alvis2ModelChecker graf LTS → plik SMV 6. nuXmv weryfikacja modelowa plik XML plik Haskell plik wykonywalny plik dot plik SMV
Rysunek 5.4: Proces weryfikacji modeli Alvis w narz˛edziu nuXmv.
przed rozjazdem, jest odpowiedzialny za odbieranie sygnału od tramwaju. Sygnalizacja ´swietlna dostarcza motorniczemu dwa rodzaje informacji – aktualn ˛a pozycj˛e iglic zwrotnicy oraz status blokady ich nap˛edu.
Odpowiedzialno´sci ˛a motorniczego jest upewnienie si˛e zanim wjedzie na rozjazd, ˙ze iglice zwrotnicy s ˛a ustawione w po˙z ˛adanym kierunku i zablokowane. Za pomoc ˛apanelu sterowania umieszczonego w tramwaju mo˙ze on zmieni´c kierunek ustawienia iglic zwrotnicy wysyłaj ˛ac sygnał przez nadajnik NP03. Gdy odbiornik otrzyma ˙z ˛adanie zmiany kierunku, wysyła odpowiedni sygnał do sterownika zwrotnicy, który po sprawdze-niu, ˙ze operacja jest bezpieczna wysyła sygnał do nap˛edu zwrotnicy, aby zmieni´c kierunek iglic. ˙Z ˛adanie zmiany kierunku jest mo˙zliwe wył ˛acznie w zasi˛egu działania odbiornika. Motorniczy ma wi˛ec jedynie ogra-niczony czas na podj˛ecie wła´sciwej decyzji, zale˙zny od pr˛edko´sci tramwaju. Je˙zeli kieruj ˛acy pojazdem nie zmieni kierunku w czasie gdy tramwaj jest w zasi˛egu operacyjnym odbiornika, to jest zmuszony zatrzyma´c pojazd i r˛ecznie zmieni´c kierunek iglic r˛ecznie, wykorzystuj ˛ac do tego specjaln ˛a d´zwigni˛e.
5.3. Testy rozwi ˛azania 64 Odbiornik IR Zwrotnica Nadajnik IR Pętla indukcyjna 1 Pętla indukcyjna 2 Sygnalizator
Rysunek 5.5: Schemat zamodelowanej zwrotnicy tramwajowej.
iglicami zwrotnicy. P˛etle te s ˛a odpowiedzialne za wykrycie przyjazdu i odjazdu tramwaju ze strefy. Kiedy pojazd jest wykryty, elektryczna blokada zwrotnicowa zatrzymuje iglice w ustawionej pozycji, uniemo˙zli-wiaj ˛ac zmian˛e ustawienia a˙z do odjazdu tramwaju. Mechanizm ten słu˙zy upewnieniu si˛e, ˙ze tramwaj bez-piecznie przejedzie przez zwrotnic˛e, niweluj ˛ac ryzyko wykolejenia si˛e na skutek złego ustawienia szyn.
5.3.2 Model systemu w j˛ezyku Alvis
Diagram komunikacji dla modelu tego systemu w j˛ezyku Alvis został przedstawiony na rysunku 5.6. War-stwa kodu dla modelu została przedstawiona w dodatku A.2. Tramwaj został zamodelowany jako agent Tram, Odbiornik podczerwieni jako agent IRReceiver, sterownik zwrotnicy jako SwitchDriver, a iglice zwrotnicy jako SwitchBlades.
Wykorzystuj ˛ac implementacj˛e algorytmu zaprezentowanego na listingu 1 model przedstawionego sys-temu został automatycznie przetłumaczony do pliku wej´sciowego narz˛edzia nuXmv. Reprezentacja w j˛e-zyku SMV zachowuje wszystkie informacje o zachowaniu systemu zawarte w wej´sciowym pliku LTS o ile nie zostan ˛a wykorzystane opcjonalne uproszczenia wył ˛aczaj ˛ace etykiety tranzycji lub zmienne inne ni˙z warto´sci z krotki parametrów.
5.3.3 Specyfikacja własno´sci systemu
Kolejnym krokiem jest weryfikacja własno´sci systemu. W prezentowanym w tym rozdziale podej´sciu s ˛a one opisane w formie formuł logiki LTL i CTL akceptowanych przez nuXmv. Trzy przykładowe formuły zostały przedstawione w Listingu 5.1.
5.3. Testy rozwi ˛azania 65 SwitchDriver getDirection inductionLoop1 setBladesState setLightsState inductionLoop2 Tram iRTransmitter lights tramIn tramOut IRReceiver setDirection getDirection SwitchBlades setBladesState TrafficLights setLightsState getState
Rysunek 5.6: Diagram komunikacji zamodelowanego sterownika zwrotnicy tramwajowej.
Listing 5.1: Przykłady formuł LTL i CTL dla modelu zwrotnicy tramwajowej.
1 --1) TramPassed = false U BladesLocked = true
2 LTLSPEC (SwitchDriver#pv3 < 2) U (SwitchBlades#pv1 < 0)
3 4 --2) EF TramPassed = true 5 CTLSPEC EF (SwitchDriver#pv3 = 2) 6 7 --3) F TramPassed = true 8 LTLSPEC F (SwitchDriver#pv3 = 2)
SwitchDriver#pv3oznacza zmienn ˛a tram (z ang. tramwaj) agenta SwitchDriver. Mo˙ze one przyjmowa´c trzy warto´sci: 0 gdy tramwaj jest przed pierwsz ˛a p˛etl ˛a indukcyjn ˛a, 1 gdy tramwaj przeje-chał przez pierwsz ˛a p˛etl˛e,oraz 2 gdy tramwaj przejeprzeje-chał przez rozjazd (min ˛ał drug ˛a p˛etl˛e indukcyjn ˛a). SwitchBlades#pv1 jest zmienn ˛a bladesState (z ang. stan iglic) agenta SwitchDriver. Gdy jej warto´s´c jest dodatnia, iglice s ˛a odblokowane, a gdy jest ujemna to iglice s ˛a zablokowane.
5.3. Testy rozwi ˛azania 66
tramwaj przejedzie przez przejazd. Własno´s´c ta jest kluczowa dla potwierdzenia bezpiecze´nstwa systemu zwrotnicowego. Narz˛edzie nuXmv potwierdziło spełnienie tej formuły w modelu. Druga formuła sprawdza, czy istnieje jakakolwiek ´scie˙zka w której tramwaj przeje˙zd˙za przez przejazd. Własno´s´c ta sprawdza czy przejazd jest w ogóle funkcjonalny, gdy˙z gdy tramwaj nigdy przez przejazd nie przeje˙zd˙za, to wszystkie formuły sprawdzaj ˛ace jego bezpiecze´nstwo byłyby spełnione, ale system jest bezu˙zyteczny. nuXmv po-twierdza jednak prawdziwo´s´c tej formuły. Ostatnie formuła jest podobna do poprzedniej, jednak sprawdza czy tramwaj zawsze ostatecznie przeje˙zd˙za przez rozjazd. Ta jednak nie jest spełniona dla modelu. Du˙z ˛a zalet ˛a narz˛edzia nuXmv jest mo˙zliwo´s´c analizy podanego przez nie kontrprzykłady dla formuł, które nie s ˛a spełnione. Tak i w tym przypadku, przegl ˛adaj ˛ac ´scie˙zk˛e w której tramwaj nie przeje˙zd˙za przez rozjazd okazuje si˛e, ˙ze dzieje si˛e to w sytuacji, gdy motorniczy nie zd ˛a˙zył wysła´c sygnału zmiany kierunku, gdy tramwaj znajdował si˛e w strefie działania odbiornika podczerwieni. W takiej sytuacji, kieruj ˛acy pojazdem zatrzymuje pojazd, wysiada i r˛ecznie zmienia kierunek iglic za pomoc ˛a d´zwigni. Jako, ˙ze takie zachowanie nie jest ju˙z elementem modelu, tramwaj został słusznie zatrzymany przed przejazdem. Zachowanie to jest uznane wi˛ec za wła´sciwe dla modelu.
5.3.4 Testy podej´scia w narz˛edziu nuXmv
Na potrzeby testów przygotowane zostały trzy wersje modelu tego samego systemu, ró˙zni ˛ace si˛e poziomem skomplikowania, ka˙zdy opisuj ˛acy system na innym poziomie abstrakcji. Dla ka˙zdego z tych modeli przy-gotowano zestaw tych samych własno´sci do sprawdzenia. Zostały one podzielone na trzy grupy: formuły osi ˛agalno´sci, bezpiecze´nstwa i ˙zywotno´sci. Zmierzono czasy weryfikacji dla formuł z ka˙zdej z tych grup. Okazało si˛e, ˙ze nie rosn ˛a one znacz ˛aco wraz ze wzrostem modelu – nawet dla najwi˛ekszych modeli jest to kilka sekund. Czas ten si˛e zwi˛eksza gdy nuXmv musi przedstawi´c wyj ˛atkowo długi ´slad dla kontrprzykładu. Jednak tym co zmienia si˛e zdecydowanie bardziej drastycznie jest czas wczytywania modelu oraz wyma-gana ilos´c pami˛eci operacyjnej. Po zaimplementowaniu algorytmu translacji parametry te zostały zmierzone i przedstawione w tabeli 5.1. Testy zostały przeprowadzone na komputerze klasy PC z systemem Linux Mint wyposa˙zonym w procesor AMD Phenom II X6 o taktowaniu 3.2 GHz oraz 16 GB pami˛eci RAM DDR3 o taktowaniu 1600 MHz. Zarówno czasy wczytywania jak i wykorzystanie RAM rosn ˛a bardzo szybko wraz ze zwi˛ekszeniem skomplikowania modelu, lecz nawet dla najbardziej zło˙zonego modelu, wci ˛a˙z s ˛a na ak-ceptowalnym poziomie.
Dla porównania jednak, zrobiono równie˙z testy na bardziej skomplikowanym modelu centrali sygnali-zacji po˙zarowej. Diagram komunikacji dla tego systemu został przedstawiony na Rys. 5.7. Warstwa kodu dla modelu została przedstawiona w dodatku A.1. Ze wzgl˛edu na zło˙zono´s´c, liczba stanów w diagramie LTS dla tego modelu jest odpowiednio wi˛eksza. Pomimo, ˙ze sam proces translacji przebiegł szybko, to na-rz˛edzie nuXmv nie mogło sobie poradzi´c z załadowaniem modelu. Ilo´s´c wymaganej pami˛eci operacyjnej
5.3. Testy rozwi ˛azania 67
Tablica 5.1: Wyniki testów wydajno´sci weryfikacji modeli Alvis w narz˛edziu nuXmv.
Model Stany RAM [GB] Czas ładowania modelu [s]
Podstawowy model zwrotnicy 1 221 0.16 8.27
Szczegółowy model zwrotnicy 3 005 0.79 63
Zaawansowany model zwrotnicy 6 835 3.53 312
Centrala sygnalizacji po˙zarowej 43 624 >16
-przekroczyła dost˛epne zasoby (RAM), a proces nuXmv został ubity przez system operacyjny (Linux). Z tego powodu czas wczytania modelu nie został podany.
SmokeDetector1 alarmSignal SmokeDetector2 alarmSignal FacpController detectors panel setAlarmState getTimerState EmployeesPanel empAction EmergencyCall getState DetectorsState alarmSignal getState AlarmState getState setState Timer getTimerState
Rysunek 5.7: Diagram komunikacji dla modelu centrali sygnalizacji po˙zarowej.
Pierwsze wyniki były wi˛ec obiecuj ˛ace, ale wci ˛a˙z nie wystarczaj ˛ace do weryfikacji systemów posiada-j ˛acych 106 stanów. Przeprowadzono wi˛ec kilka usprawnie´n algorytmu translacji, a w konsekwencji zopty-malizowano równie˙z wynikowy model nuXmv. Nast˛epnie przeprowadzone zostały ponowne testy na tych samych modelach co poprzednio. Do zestawienia dodano równie˙z kilka innych modeli – czasow ˛a wer-sj˛e dla modelu centrali sygnalizacji po˙zarowej oraz rozbudowanego modelu znanego problemu producent-konsument. Ten ostatni został dodany do zestawienia ze wzgl˛edu na łatwe skalowanie tego modelu w celu generowanie wielu mo˙zliwych stanów. Diagram komunikacji dla podstawowego modelu z jednym
produ-5.3. Testy rozwi ˛azania 68
Tablica 5.2: Wyniki testów wydajno´sci weryfikacji modeli Alvis w narz˛edziu nuXmv po optymalizacji al-gorytmu.
Model Stany RAM [GB] Czas ładowania modelu [s]
Podstawowy model zwrotnicy 1 221 0.075 1.4
Szczegółowy model zwrotnicy 3 005 0.31 10.5
Zaawansowany model zwrotnicy 6 835 1.4 64
Centrala sygnalizacji po˙zarowej (model z czasem) 19 628 12.4 716
Centrala sygnalizacji po˙zarowej 43 624 >16
-Producent-konsument 1 1 404 0.082 1.55
Producent-konsument 2 3 606 0.41 11.2
Producent-konsument 3 13 626 5.21 158.7
Producent-konsument 4 30 096 >16
-centem i dwoma konsumentami został przedstawiony na rysunku 5.8. Warstwa kodu dla modelu została przedstawiona w dodatku A.3. Wyniki testów zostały przedstawione w tabeli 5.2.
Buffer put get P1 put C2 get C1 get
Rysunek 5.8: Diagram komunikacji dla modelu Producent-konsument.
Jak pokazuj ˛a przedstawione wyniki, optymalizacje pozwoliły uzyska´c ok 2.5 razy mniejsze zu˙zycie pami˛eci operacyjnej oraz 5-6 razy szybsze wczytywanie modelu. Dzi˛eki temu, udało si˛e dokona´c weryfi-kacji systemu posiadaj ˛acego ponad 19.6 tysi˛ecy stanów. Wci ˛a˙z jednak wyniki te dalekie s ˛a od zało˙zonych 106 stanów. Problemem jest w tym wypadku bardzo zachłanne pod k ˛atem pami˛eci operacyjnej podej´scie stosowane przez nuXmv. Problem najlepiej wida´c na wykresie 5.9, gdzie przedstawiona jest zale˙zno´s´c wy-maganej pami˛eci RAM w zale˙zno´sci od liczby stanów, utworzona na podstawie uzyskanych wyników.
5.3.5 Podsumowanie wyników
Wyniki testów potwierdziły, ˙ze prezentowane podej´scie sprawdza si˛e dla modeli o niskiej i ´sredniej zło˙zo-no´sci. Jednak dla bardziej zło˙zonych modeli wymaga ono bardzo du˙zej ilo´sci zasobów. Szczególnie proble-matyczna jest wymagana ilo´s´c pami˛eci RAM, której ilo´s´c dost˛epna na standardowym sprz˛ecie PC pozwala na weryfikacj˛e modeli o liczbie stanów rz˛edu 104.