7.2 Alvis Query Language
7.3.3 Porównanie z wynikami weryfikacji w nuXmv
Przedstawione wyniki pokazuj ˛a znacz ˛ac ˛a popraw˛e w wykorzystaniu kluczowego zasobu, jakim jest pami˛e´c operacyjna, w stosunku do weryfikacji w narz˛edziu nuXmv. Ró˙znice wida´c szczególnie przy du˙zych mo-delach. Przykładowo weryfikacja modelu centrali sygnalizacji po˙zarowej z ponad 116 tysi ˛acami stanów w nuXmv wymaga 415 GB RAM, podczas gdy w AQL wystarcza 0.53 GB. Dzi˛eki temu mo˙zliwe jest prze-prowadzenie weryfikacji dla modeli, których weryfikacja przy pomocy nuXmv była niemo˙zliwa ze wzgl˛edu na koszty instancji.
Na podstawie wyników pomiarów zebranych w tabeli 7.2 zauwa˙zono, ˙ze zale˙zno´s´c rezerwowanej przez GHCI pami˛eci operacyjnej do ilo´sci stanów modelu jest funkcj ˛a liniow ˛a, w przeciwie´nstwie do weryfikacji w nuXmv, gdzie zale˙zno´s´c ta została przybli˙zona funkcj ˛a kwadratow ˛a (patrz rysunek 6.5). Wykresy za-le˙zno´sci wymaganej ilo´sci pami˛eci RAM od liczby stanów w modelach weryfikowanych za pomoc ˛a AQL zostały przedstawione na rysunku 7.4.
W przypadku weryfikacji za pomoc ˛a AQL, do załadowania modeli zawieraj ˛acych 106stanów potrzebne jest w zale˙zno´sci od modelu od 1.5 do 3.5 GB pami˛eci operacyjnej. Zestawiaj ˛ac to z 25.5 TB wyliczonymi dla weryfikacji w nuXmv, wida´c wyra´zn ˛a przewag˛e proponowanego podej´scia opartego o posta´c po´sredni ˛a w j˛ezyku Haskell.
7.4. Podsumowanie 95
Tablica 7.3: Przykładowe wyniki eksperymentów z wydajno´sci ˛a funkcji AQL operuj ˛acych na ´scie˙zkach w grafie.
Model Stany Formuła Przyrost
RAM [MB] Czas [godz] Centrala sygnalizacji po˙zarowej (z czasem) 19 628 isReachable 0 19627 <1 <0.01 Centrala sygnalizacji po˙zarowej (z czasem) 19 628 minPathLen 0 19627 13 7.96 Centrala sygnalizacji po˙zarowej 43 624 isReachable 4 43623 <1 <0.01 Centrala sygnalizacji po˙zarowej 2 (z czasem) 116 697 isReachable 45 116696 <1 <0.01 Centrala sygnalizacji po˙zarowej 2 (z czasem) 116 697 maxPathLen 0 99001 <1 <0.01 Centrala sygnalizacji po˙zarowej 3 (z czasem) 639 604 isReachable 3532 624121 <1 <0.01 Producent-konsument 4 30 096 allPathsReach 0 30095 <1 <0.01 Producent-konsument 5 118 206 isReachable 32 118205 <1 <0.01 Je´sli chodzi o czas ładowania modelu, to warto zwróci´c uwag˛e, ˙ze kompilacja grafu LTS jest wyma-ganym etapem weryfikacji w nuXmv. Tak wi˛ec nie ma warto´sci porównywanie czasów ładowania modelu w nuXmv do czasów wyliczania LTS.
7.4 Podsumowanie
Rezultatem tego etapu bada´n było wprowadzenie nowego podej´scia do weryfikacji modeli w j˛ezyku Alvis, opartego na wykorzystaniu postaci po´sredniej w j˛ezyku Haskell. Przeprowadzone testy potwierdziły, ˙ze dzi˛eki wykorzystaniu zalet programowania funkcyjnego, weryfikacja modeli Alvis bezpo´srednio w j˛ezyku Haskell jest znacznie bardziej optymalna pod k ˛atem wykorzystania pami˛eci operacyjnej ni˙z weryfikacja w nuXmv. Jednocze´snie przygotowany interfejs w postaci j˛ezyka Alvis Query Language, dostarcza łatwe do zrozumienia i wykorzystania funkcje, które pozwalaj ˛a korzysta´c z narz˛edzia nawet osobom nie posiada-j ˛acym znaposiada-jomo´sci posiada-j˛ezyka Haskell. Za ich pomoc ˛a mo˙zliwa posiada-jest weryfikacposiada-ja modeli o liczbie stanów prze-kraczaj ˛acej 106.
7.4. Podsumowanie 96
Liczba stanów modelu
Wykorzystanie RAM [GB] 0 1 2 3 4 200 000 400 000 600 000 800 000 1 000 000
Producent-konsument 1,3E-06*x + 0,13 R² = 0,999 Centrala sygnalizacji pożarowej (z czasem) 3,56E-06*x + 0,123 R² = 1 Centrala sygnalizacji pożarowej 2,24E-06*x + 0,122 R² = 1 Predykcja
Rysunek 7.4: Wykresy zale˙zno´sci zajmowanej przez GHCI pami˛eci RAM od liczby stanów modelu wraz z predykcjami opartymi na regresji liniowej.
wszystkim w kolejnych fazach warto zintegrowa´c generacj˛e kodu odpowiedzialnego za weryfikacj˛e z kom-pilatorem Alvis Compiler. Ponadto warto rozwa˙zy´c rozszerzenie zestawu dost˛epnych funkcji. W szczegól-no´sci mo˙zna w przyszło´sci zaimplementowa´c pewien podzbiór operatorów jednej z logik temporalnych, np. RTCTL.
Rozdział 8
Podsumowanie
J˛ezyk Alvis powstał w wyniku poszukiwa´n formalnego j˛ezyka modelowania, który b˛edzie łatwy w u˙zyt-kowaniu dla in˙zynierów oprogramowania. W tym celu Alvis ł ˛aczy w sobie zalety j˛ezyków programowania wysokiego poziomu z graficznymi j˛ezykami modelowania zale˙zno´sci pomi˛edzy komponentami (agentami) w systemach współbie˙znych. Jednym z podstawowych zało˙ze´n j˛ezyka jest umo˙zliwienie formalnej analizy modeli w nim utworzonych.
Przed rozpocz˛eciem prac opisanych w niniejszej rozprawie, jedyn ˛a mo˙zliwo´sci ˛a formalnej analizy mo-deli Alvis było podej´scie bazuj ˛ace na generacji grafu LTS, stanowi ˛acego reprezentacj˛e przestrzeni stanów modelu i jego eksport do formatu Aldebaran. Plik ten mo˙zna nast˛epnie wczyta´c do narz˛edzia CADP Evalu-ator w celu przeprowadzenia weryfikacji. Ogromn ˛a wad ˛a tego podej´scia jest utrata przy eksporcie wszyst-kich informacji przechowywanych w stanach systemu, w tym w szczególno´sci warto´sci zmiennych.
Celem rozprawy było zaproponowanie i implementacja alternatywnego podej´scia do analizy, umo˙zli-wiaj ˛acego skuteczn ˛a formaln ˛a weryfikacj˛e modeli Alvis w oparciu o stany, wykorzystuj ˛ac posta´c po´sredni ˛a modelu w j˛ezyku Haskell. Postawiono równie˙z zało˙zenie, ˙ze proponowane podej´scie powinno umo˙zliwia´c analiz˛e modeli o liczbie stanów przekraczaj ˛acej 106, na sprz˛ecie dost˛epnym dla przeci˛etnego in˙zyniera w akceptowalnym przedziale czasu. Ponadto, aby ułatwi´c wykorzystanie rozwi ˛azania, w ramach pracy miał zosta´c stworzony j˛ezyk zapyta´n umo˙zliwiaj ˛acy intuicyjn ˛a weryfikacje wybranych własno´sci modeli, bez konieczno´sci znajomo´sci wewn˛etrznej reprezentacji modelu czy j˛ezyka Haskell. Dodatkowo, opracowane w ramach pracy narz˛edzia miały rozszerza´c opracowany ju˙z wcze´sniej proces, integruj ˛ac si˛e z istniej ˛acym pakietem narz˛edzi Alvis.
Zadania te zostały zrealizowane poprzez opracowanie i implementacj˛e j˛ezyka zapyta´n Alvis Query Lan-guage, umo˙zliwiaj ˛acego weryfikacj˛e modelu operuj ˛ac na postaci IHR. Dodatkowo zaproponowane zostało komplementarne podej´scia do weryfikacji modeli w narz˛edziu nuXmv oraz rozszerzenie mo˙zliwo´sci wery-fikacji obu podej´s´c, poprzez wykorzystanie chmur obliczeniowych.
98 Do najwa˙zniejszych wyników rozprawy nale˙zy zaliczy´c:
• Opracowanie koncepcji analizy modeli w j˛ezyku Alvis na podstawie ich postaci IHR i wł ˛aczenia jej w istniej ˛acy proces.
• Implementacj˛e j˛ezyka zapyta´n Alvis Query Language, umo˙zliwiaj ˛acego intuicyjn ˛a analiz˛e modeli systemów zawieraj ˛acych powy˙zej 106 stanów na standardowym sprz˛ecie komputerowym.
• Opracowanie i implementacj˛e algorytmu translacji do j˛ezyka SMV, pozwalaj ˛acego na weryfikacj˛e modeli Alvis przy wykorzystaniu narz˛edzia nuXmv.
• Opracowanie procesu weryfikacji modeli Alvis wykorzystuj ˛acego rozwi ˛azania chmurowe i demon-stracja jego warto´sci poprzez przeprowadzenie weryfikacji modeli na instancjach Google Cloud Com-pute.
• Opracowanie kilku modeli systemów współbie˙znych i czasu rzeczywistego, a nast˛epnie ich formaln ˛a weryfikacj˛e przy wykorzystaniu proponowanych podej´s´c.
• Przygotowanie analizy porównawczej wydajno´sci zaproponowanych podej´s´c na podstawie pomiarów zebranych podczas weryfikacji przygotowanych modeli.
Realizacja powy˙zszych zada´n spełnia wyszczególnione cele pracy, jak równie˙z weryfikuje pozytywnie postawion ˛a tez˛e rozprawy.
Niniejsza rozprawa z cał ˛a pewno´sci ˛a nie wyczerpuje jednak tematyki zwi ˛azanej z formaln ˛a weryfikacj ˛a modeli w j˛ezyku Alvis. W wyniku prac badawczych zauwa˙zono nast˛epuj ˛ace, potencjalne kierunki rozwoju j˛ezyka i narz˛edzi modelowania:
• Przedstawiony w rozprawie zestaw dost˛epnych funkcji AQL nie wyczerpuje mo˙zliwo´sci wykorzy-stania postaci po´sredniej w j˛ezyku Haskell. Warto rozwa˙zy´c rozszerzenie go o funkcje pozwalaj ˛ace na jeszcze dokładniejsz ˛a weryfikacj˛e modelu. W szczególno´sci przydatna dla u˙zytkownika byłaby implementacja wybranego podzbioru jednej z logik temporalnych (np. RTCTL).
• Przygotowana w ramach bada´n implementacja funkcji AQL nie została jeszcze zintegrowana z kompi-latorem Alvis Compiler. Du˙zym ułatwieniem dla u˙zytkownika byłaby implementacja generacji kodu Haskell odpowiedzialnego za weryfikacj˛e własno´sci AQL bezpo´srednio w kompilatorze.
• Podej´scie oparte o przetwarzanie w chmurze jest wartym rozwa˙zenia kierunkiem rozwoju całego zestawu narz˛edzi. Cały zaproponowany proces mógłby by´c oskryptowany do tego stopnia, ˙ze weryfi-kacja uruchomiana byłaby poprzez wywołanie jednej komendy na maszynie lokalnej. Mo˙zna jednak pój´s´c dalej i przenie´s´c wszystkie narz˛edzia na stałe do chmury obliczeniowej i udost˛epni´c narz˛edzia modelowania i weryfikacji Alvis jako usług˛e typu SaaS.
• Analiza mo˙zliwo´sci wykorzystania technik redukcji przestrzeni stanów w weryfikacji modeli Alvis. Obecnie w grafie LTS wiele stanów niewiele wnosi je´sli chodzi o sprawdzanie własno´sci modelu. Redukcja przestrzeni stanów pozwoliłaby weryfikowa´c znacznie wi˛eksze modele przy wykorzystaniu
99 tych samych zasobów.
• W ramach pracy testowano podej´scie oparte na translacji i weryfikacji modeli Alvis w nuXmv. Jest jednak wiele innych model checkerów, które potencjalnie mog ˛a sobie lepiej radzi´c z optymalizacj ˛a wykorzystania pami˛eci operacyjnej. Przeprowadzenie kompleksowej analizy wraz ze stworzeniem szybkich prototypów mogłoby wyłoni´c lepsze narz˛edzie do weryfikacji modeli Alvis.
Dodatek A
Listingi warstw kodu dla przykładów
testowanych modeli systemów
A.1 Centrala sygnalizacji po˙zarowej
Listing A.1: Warstwa kodu dla podstawowego modelu centrali sygnalizacji po˙zarowej z rysunku 5.7
1 agent SmokeDetector1, SmokeDetector2{
2 smokeDetected :: Bool = False;
3 loop {
4 smokeDetected = pick [True, False];
5 select{ 6 alt(smokeDetected){ 7 out alarmSignal; 8 exit; 9 } 10 } 11 } 12 } 13 ---14 agent DetectorsState { 15 numberOfActivatedDetectors :: Int = 0; 16 ---17 proc alarmSignal { 18 in (0) alarmSignal{ 19 success{ 20 numberOfActivatedDetectors = numberOfActivatedDetectors + 1; 21 exit; 100
A.1. Centrala sygnalizacji po˙zarowej 101 22 } 23 } 24 } 25 ---26 proc getState {
27 out getState numberOfActivatedDetectors;
28 exit; 29 } 30 } 31 ---32 -- EMP ACTION: 33 -- 0 - No action
34 -- 1 - Reset (not available in this version)
35 -- 2 - Confirm 36 -- 3 - Alarm1Off 37 -- 4 - Alarm2On 38 agent FacpController{ 39 alarmState :: Int = 0; 40 numberOfActivatedDetectors :: Int = 0; 41 empAction :: Int = 0;
42 timerUp :: Bool = False;
43 confirmed :: Bool = False;
44 45 loop{ 46 in (0) detectors numberOfActivatedDetectors; 47 in (0) panel empAction { 48 fail{ 49 empAction = 0; 50 } 51 } 52 ---53 select{
54 alt(numberOfActivatedDetectors > 1 || empAction == 4){
55 External alarm is turned on
--56 alarmState = 2;
57 out setAlarmState alarmState;
58 exit;
59 }
A.1. Centrala sygnalizacji po˙zarowej 102
61 Internal alarm is turned on by detectors
--62 alarmState = 1;
63 timerUp = False;
64 }
65 alt(alarmState == 1 && confirmed == False && empAction /= 2){
66 -- Internal alarm is still turned on but not
confirmed--67 in getTimerState timerUp;
68 select{
69 alt(timerUp == True){
70 alarmState = 2;
71 out setAlarmState alarmState;
72 exit;
73 }
74 }
75 }
76 alt(alarmState == 1 && confirmed == False && empAction == 2){
77 -- Internal alarm is
confirmed--78 confirmed = True;
79 }
80 alt(alarmState == 1 && confirmed == True){
81 Internal alarm is still turned on and waiting for threat evaluation
--82 in getTimerState timerUp;
83 select{
84 alt(timerUp == True){
85 alarmState = 2;
86 out setAlarmState alarmState;
87 exit; 88 } 89 } 90 } 91 } 92 } 93 } 94 ---95 agent Timer {
96 timeUp :: Bool = False;
97
98 proc getTimerState {
99 timeUp = pick [False, True];
A.1. Centrala sygnalizacji po˙zarowej 103
100 out getTimerState timeUp;
101 exit; 102 } 103 } 104 ---105 -- EMP ACTION: 106 -- 0 - No action
107 -- 1 - Reset (not available in this version)
108 -- 2 - Confirm 109 -- 3 - Alarm1Off 110 -- 4 - Alarm2On 111 agent EmployeesPanel{ 112 action :: Int = 0; 113 114 loop { 115 select{ 116 alt(action == 0){ 117 action = pick [0,2]; 118 select{ 119 alt(action > 0){ 120 out empAction; 121 } 122 } 123 } 124 alt(action == 2){ 125 action = pick [0,3,4]; 126 select{ 127 alt(action > 0){ 128 out empAction; 129 } 130 } 131 } 132 alt(action == 3){ 133 exit; 134 } 135 alt(action == 4){ 136 exit; 137 } 138 }
A.2. Zwrotnica tramwajowa 104 139 } 140 } 141 ---142 agent AlarmState { 143 alarmState :: Int = 0; 144 ---145 proc setState { 146 in setState alarmState; 147 exit; 148 } 149 ---150 proc getState {
151 out getState alarmState;
152 exit; 153 } 154 } 155 ---156 agent EmergencyCall { 157 alarmState :: Int = 0;
158 turnOn :: Bool = False;
159 loop { 160 in getState alarmState; 161 select{ 162 alt(alarmState == 2){ 163 turnOn = True; 164 exit; 165 } 166 } 167 } 168 }
A.2 Zwrotnica tramwajowa
Listing A.2: Warstwa kodu dla podstawowego modelu zwrotnicy tramwajowej z rysunku 5.5
1 agent Tram{
2 desiredDirection :: Int = 0;
3 bladesState :: Int = 0;
4 desiredDirection = pick [1,2];
A.2. Zwrotnica tramwajowa 105
5 --sending desired direction signal
6 out (0) iRTransmitter desiredDirection; --Tram has to send the signal when in the range of IRReceiver.
7 --tram in the switch zone
8 out tramIn;
9 --some time later:
10 in lights bladesState;
11 select{
12 alt(bladesState == desiredDirection){
13 --switch blades in right direction and switch is locked
14 out tramOut; --tram goes through the switch
15 }
16 -- in other case dir change was not received ...
17 -- ... and tram has to change it manually or will go the wrog way
18 } 19 } 20 ---21 agent IRReceiver{ 22 direction :: Int = 0; 23 in getDirection direction;
24 out setDirection direction;
25 }
26
---27 agent SwitchDriver{
28 direction :: Int = 0;
29 state :: Int = 0;
30 tram :: Int = 0; --tram state: 0 - before, 1- in, 2 - past switch zone
31 state = pick [-2,-1];
32 --initializing state:
33 out setLightsState state;
34 out setBladesState state;
35 start IRReceiver;
36 start Tram;
37
38 in (0) getDirection direction{ --checking if direction is to be changed
39 success{
40 state = direction;
41 }
42 fail{
A.3. Producent-konsument 106
44 }
45 }
46 in inductionLoop1; -- waiting for a tram to arrive in a switch zone
47 out setBladesState state;
48 out setLightsState state;
49 --waiting for tram to go through
50 in inductionLoop2;
51 state = -1 * state; --unblocking switch blades
52 out setBladesState state;
53 out setLightsState state;
54 }
55
---56 agent SwitchBlades{
57 bladesState :: Int = 0;
58 -- state: 1 - left locked, 2 - right locked
59 -- state: -1 - left not locked, -2 - right not locked
60 proc setBladesState{ 61 in setBladesState bladesState; 62 exit; 63 } 64 } 65 ---66 agent TrafficLights{ 67 lightsState :: Int = 0;
68 -- state: 1 - left locked, 2 - right locked
69 -- state: -1 - left not locked, -2 - right not locked
70 proc setLightsState{
71 in setLightsState lightsState;
72 exit;
73 }
74 proc getState{
75 out getState lightsState;
76 exit;
77 }
78 }
A.3 Producent-konsument
Listing A.3: Warstwa kodu dla podstawowego modelu Producent-Konsument z rysunku 5.8
A.3. Producent-konsument 107 1 agent P1 { 2 loop { 3 out put; 4 } 5 } 6 ---7 agent Buffer { 8 b :: Int = 0; 9 t1 :: Int = 0; 10 t2 :: Int = 0;
11 busy :: Bool = False;
12 13 proc (b < 5) put { 14 in put; 15 t1 = b + 1; 16 b = t1; 17 exit; 18 }
19 proc (b > 0 && busy == False) get {
20 busy = True; 21 out get; 22 t2 = b - 1; 23 b = t2; 24 busy = False; 25 exit; 26 } 27 } 28 ---29 agent C1,C2 { 30 loop { 31 in get; 32 } 33 }
Bibliografia
[1] F. Aarts, H. Kuppens, J. Tretmans, F. W. Vaandrager, and S. Verwer. Learning and testing the bounded retransmission protocol. In ICGI, 2012.
[2] L. Aceto, A. Ingófsdóttir, K.G. Larsen, and J. Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge, UK, 2007.
[3] R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Compu-tation, 104(1):2 – 34, 1993.
[4] R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 1994.
[5] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Verifying continuous time Markov chains. In R. Alur and T. Henzinger, editors, Proc. 8th International Conference on Computer Aided Verification (CAV’96), volume 1102 of LNCS, pages 269–276. Springer, 1996.
[6] C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, London, UK, 2008. [7] K. Balicki and M. Szpyrka. Formal definition of XCCS modelling language. Fundamenta
Informa-ticae, 93(1-3):1–15, 2009.
[8] C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 825–885. IOS Press, 2009.
[9] G. Behrmann, A. David, and K. G. Larsen. A Tutorial on Uppaal, pages 200–236. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004.
[10] J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL — a Tool Suite for Auto-matic Verification of Real–Time Systems. In Proc. of Workshop on Verification and Control of Hybrid Systems III, number 1066 in Lecture Notes in Computer Science, pages 232–243. Springer–Verlag, October 1995.
BIBLIOGRAFIA 109
[11] J. Bengtsson and W. Yi. Timed automata: Semantics, algorithms and tools. Lecture Notes on Con-currency and Petri Nets, 3098, 2004.
[12] J. A. Bergstra, A. Ponse, and S. A. Smolka, editors. Handbook of Process Algebra. Elsevier Science, Upper Saddle River, NJ, USA, 2001.
[13] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu. Bounded model checking. Advances in computers, 58(11):117–148, 2003.
[14] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without bdds. In Proce-edings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS ’99, pages 193–207, Berlin, Heidelberg, 1999. Springer-Verlag.
[15] J. Biernacki. Alvis models of safety critical systems state-base verification with nuXmv. In Pro-ceedings of the Federated Conference on Computer Science and Information Systems, pages 1701– 1708, 2016.
[16] J. Biernacki. Alvis2ModelChecker. http://alvis.kis.agh.edu.pl/wiki/software# alvis2modelchecker, 2019.
[17] J. Biernacki, A. Biernacka, and M. Szpyrka. Action-based verification of RTCP-nets with CADP. In International Conference of Computational Methods in Sciences and Engineering (ICCMSE 2015), volume 1702 of AIP Conference Proceedings, pages 100011–1–100011–4, Athens, Greece, March 20-23 2015. AIP Publishing.
[18] T. Bolognesi and E. Brinksma. Introduction to the iso specification language lotos. Comput. Netw. ISDN Syst., 14(1):25–59, March 1987.
[19] J. Bozic, L. Marsso, R. Mateescu, and F. Wotawa. A formal tls handshake model in lnt. CoRR, abs/1803.10319:1–40, 2018.
[20] J. Bradfield and I. Walukiewicz. The mu-calculus and Model Checking, pages 871–919. Springer International Publishing, Cham, 2018.
[21] R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., 35(8):677–691, August 1986.
[22] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020states and beyond. In LICS, pages 428–439. IEEE Computer Society, 1990.
[23] A. Burns and A. Wellings. Concurrent and real-time programming in Ada 2005. Cambridge Univer-sity Press, 2007.
BIBLIOGRAFIA 110
[24] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta. The nuxmv symbolic model checker. In Proceedings of the 16th International Conference on Computer Aided Verification - Volume 8559, pages 334–342, Berlin, Heidelberg, 2014. Springer-Verlag.
[25] D. Champelovier, X. Clerc, H. Garavel, Y. Guerte, C. McKinty, V. Powazny, F. Lang, W. Serwe, and G. Smeding. Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4). INRIA/VASY, 2011.
[26] T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. Automatic verification of competitive stochastic systems. In C. Flanagan and B. König, editors, Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), volume 7214 of LNCS, pages 315–330. Springer, 2012.
[27] A. Cimatti, E. Clarke, , F. Giunchiglia, and M. Roveri. NUSMV: a new Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, Proceedings Eleventh Conference on Computer-Aided Verifi-cation (CAV’99), number 1633 in Lecture Notes in Computer Science, pages 495–499, Trento, Italy, July 1999. Springer.
[28] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In Proc. International Conference on Computer-Aided Verification (CAV 2002), volume 2404 of LNCS, Co-penhagen, Denmark, July 2002. Springer.
[29] A Cimatti, A. Griggio, B. Schaafsma, and R. Sebastiani. The MathSAT5 SMT Solver. In Nir Piterman and Scott Smolka, editors, Proceedings of TACAS, volume 7795 of LNCS. Springer, 2013.
[30] J. Ciszewski and Marchlewski K. Wytyczne projektowania instalacji sygnalizacji po˙zarowej (SITP WP - 02:2010), 2011.
[31] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 8(2):244–263, April 1986.
[32] E. M. Clarke, O Grumberg, M Minea, and D. A. Peled. State space reduction using partial order techniques. International Journal on Software Tools for Technology Transfer, 2:279–287, 1999. [33] E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. MIT Press, London, Cambridge, 1999.
BIBLIOGRAFIA 111
[34] E. M. Clarke and F. Lerda. Model checking: Software and beyond. Journal of Universal Com-puter Science, 13(5):639–649, may 2007. http://www.jucs.org/jucs_13_5/model_ checking_software_and.
[35] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, Workshop, pages 52–71, Berlin, Heidelberg, 1982. Springer-Verlag.
[36] Google Cloud. Google Cloud Documentation, 2020.
[37] CONVECS. Research tools connected to the CADP toolset, 2019.
[38] O. Coudert and J.-C. Madre. A unified framework for the formal verification of sequential circuits. 1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers, pages 126–129, 1990.
[39] C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. J. ACM, 42(4):857–907, July 1995.
[40] F. Dannenberg, M. Kwiatkowska, C. Thachuk, and A. Turberfield. DNA walker circuits: computatio-nal potential, design, and verification. In D. Soloveichik and B. Yurke, editors, Proc. 19th Internatio-nal Conference on DNA Computing and Molecular Programming (DNA 19), volume 8141 of LNCS, pages 31–45. Springer, 2013.
[41] A. David and K. G. Larsen. A tutorial on uppaal 4.0. 01 2006.
[42] University of Oxford Department of Computer Science. PRISM model checker, 2020.
[43] M. Duflot, M. Kwiatkowska, G. Norman, and D. Parker. A formal analysis of Bluetooth device discovery. In Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA’04), 2004.
[44] E. A. Emerson. Model checking and the Mu-calculus. In N. Immerman and P. G. Kolaitis, editors, Descriptive Complexity and Finite Models, volume 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 185–214. American Mathematical Society, 1997.
[45] G. Fraser, F. Wotawa, and P. E. Ammann. Testing with model checkers: A survey. Softw. Test. Verif. Reliab., 19(3):215–261, September 2009.
BIBLIOGRAFIA 112
[47] H. Garavel. XTL: A metalanguage and tool for temporal logic modelchecking. In In Proceedings of the International Workshop on Software Tools for Technology Transfer STTT98 (Aalborg, Denmark), pages 33–42, 1998.
[48] H. Garavel, F. Lang, R. Mateescu, and W. Serwe. CADP 2006: A toolbox for the construction and analysis of distributed processes. In Computer Aided Verification (CAV’2007), volume 4590 of LNCS, pages 158–163, Berlin, Germany, 2007. Springer.
[49] H. Garavel, F. Lang, R. Mateescu, and W. Serwe. CADP 2011: a toolbox for the construction and analysis of distributed processes. International Journal on Software Tools for Technology Transfer (STTT), 15(2):89–107, 2013.
[50] H. Giese and S. Burmester. Real-time statechart semantics. Technical Report tr-ri-03-239, Universität Paderborn, Paderborn, Germany, June 2003.
[51] S. Gnesi and M. Tiziana. Formal Methods for Industrial Critical Systems: A Survey of Applications. 11 2012.
[52] GNU. Screen User’s Manual, 2018.
[53] M. Gorowski. Transport szynowy, 2014. http://www.transportszynowy.pl/zwrotnicetramsterowanie.php. [54] P. Głuchowski. Temporalna logika RTCTL w opisie i analizie w czasie rzeczywistym minimalnych
zbiorów przyczyn dla drzew niezdatno´sci z zale˙zno´sciami czasowymi. In Modele i zastosowania systemów czasu rzeczywistego, pages 23–32. WKŁ, 2008.
[55] H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535, 1994.
[56] D. Harel. Statecharts: A visual formalism for complex systems. Sci. Comput. Program., 8(3):231– 274, June 1987.
[57] D. Harel and M. Politi. Modeling Reactive Systems with Statecharts: The Statemate Approach. McGraw-Hill, Inc., New York, NY, USA, 1st edition, 1998.
[58] A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In H. Hermanns and J. Palsberg, editors, Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’06), volume 3920 of LNCS, pages 441–444. Springer, 2006.
[59] C. A. R. Hoare. Communicating sequential processes. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1985.
BIBLIOGRAFIA 113
[60] G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1991.
[61] G. J. Holzmann. The model checker spin. IEEE Trans. Softw. Eng., 23(5):279–295, May 1997. [62] G. J. Holzmann. Logic verification of ANSI-C code with SPIN. In SPIN Model Checking and
Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30 - September 1, 2000, Proceedings, pages 131–147, 2000.
[63] G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2003. [64] J. E. Hopcroft, R. Motwani, and J. D. Ullman. Introduction to Automata Theory, Languages, and
Computation (3rd Edition). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA,