University of Science and Technology in Kraków
Faculty of Electrical Engineering, Automatics, Computer Science and Biomedical Engineering
P
H
D D
ISSERTATION
A
PPLICATION OF FUNCTIONAL PARADIGM TO FORMAL
ANALYSIS OF SYSTEMS MODELLED WITH
A
LVIS LANGUAGE
AUTHOR:
Jerzy Biernacki SUPERVISOR:
Prof. Marcin Szpyrka, PhD, DSc ASSISTANT SUPERVISOR:
Piotr Matyasik, PhD
Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
Wydział Elektrotechniki, Automatyki, Informatyki i In˙zynierii BiomedycznejR
OZPRAWA
D
OKTORSKA
Z
ASTOSOWANIE PARADYGMATU FUNKCYJNEGO DO
FORMALNEJ ANALIZY SYSTEMÓW MODELOWANYCH W
J ˛
EZYKU
A
LVIS
AUTOR:
Jerzy Biernacki PROMOTOR:
Prof. dr hab. Marcin Szpyrka
PROMOTOR POMOCNICZY:
Dr in˙z. Piotr Matyasik
iv
Chciałbym szczególnie podzi˛ekowa´c swojej ˙Zonie, której nieoceniona pomoc pozwoliła mi znale´z´c czas na sko´nczenie bada´n i napisanie rozprawy.
Serdecznie dzi˛ekuj˛e równie˙z mojemu promotorowi prof. dr hab. Marcinowi Szpyrce, za motywacj˛e, cierpliwo´s´c i pomoc merytoryczn ˛a udzielon ˛a w trakcie pisania tej pracy.
v This doctoral dissertation deals with methods of formal verification of system models specified in Alvis modelling language. Formal methods are specifically useful in verification of systems which are required to give high guarantees of satisfying fundamental properties. This is specifically true for safety-critical systems which errors or failures can endanger human life or health, natural environment or cause severe economic losses. The problem that trouble most of the popular formalisms is their unapproachability for regular software engineers.
Alvis language was created in an attempt to find a formal modelling language that would be easy to use for software engineers. To meet this goal, Alvis combines the advantages of high-level programming languages with the graphical design of dependencies between the components (agents) in concurrent sys-tems. One of the core goals of this language is to enable formal verification of the specified models. Before the start of the research presented in this dissertation, the only way of formal analysis of Alvis models was verification using the CADP Evaluator tool. The crippling flaw of this approach is that all information on the state is lost in the process of export. In particular, the exported model does not carry any information on the values of variables.
The main goal of this dissertation was to propose and implement an alternative approach to the analy-sis, enabling to effectively and formally verify Alvis models incorporating information carried originally in states representation with the use of intermediate Haskell representation. An additional assumption was that the presented approach should be able to analyse models containing over 106states on a standard personal
computer in an acceptable amount of time. Moreover, to facilitate the usage of the approach, a dedicated qu-ery language should be defined, enabling intuitive verification of selected subset of model properties without advanced knowledge of internal representation of the model or Haskell programming skills. Additionally, all the presented tools are to extend the current verification process and integrate with the existing Alvis toolkit.
These goals were met through the definition and implementation of Alvis Query Language, enabling to verify models using their Haskell representation. Additionally, the dissertation presents a complementary approach to model verification using nuXmv tool and a process of enhancing both methods through the usage of cloud computing.
The dissertation also contains a few case studies of formal verification of concurrent and real-time systems with the proposed approaches. The measurements collected during the verification process are used to provide a comparative analysis of the presented methods.
vi Przedstawiona rozprawa doktorska dotyczy metod formalnej weryfikacji modeli systemów wyspecy-fikowanych w j˛ezyku Alvis. Metody formalne maj ˛a szczególne zastosowanie w odniesieniu do systemów w stosunku do których oczekiwane jest zapewnienie bardzo wysokich gwarancji spełnienia wskazanych własno´sci. Szczególnym przykładem s ˛a tutaj systemy krytyczne ze wzgl˛edu na bezpiecze´nstwo, których awarie lub bł˛edy mog ˛a mie´c wpływ na ˙zycie lub zdrowie ludzi, ´srodowisko naturalne czy te˙z spowodowa´c istotne straty ekonomiczne. Problemem wi˛ekszo´sci popularnych metod formalnych jest jednak ich nieprzy-st˛epno´s´c dla przeci˛etnych in˙zynierów oprogramowania.
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 modeli Alvis była weryfikacja w pakiecie CADP Evaluator. Ogromn ˛a wad ˛a tego podej´scia jest utrata przy eksporcie wszystkich 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 opracowany j˛ezyk zapyta´n umo˙zliwiaj ˛acy intuicyjn ˛a weryfikacj˛e 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.
Cele 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´scie do weryfikacji modeli w narz˛edziu nuXmv oraz rozszerzenie mo˙zliwo´sci wery-fikacji obu podej´s´c, poprzez wykorzystanie chmur obliczeniowych.
Rozprawa zawiera tak˙ze studium przypadków formalnej weryfikacji modeli systemów współbie˙znych i czasu rzeczywistego przy wykorzystaniu proponowanych podej´s´c. Na podstawie pomiarów zebranych podczas weryfikacji tych modeli przygotowana została analiza porównawcza opracowanych metod.
Spis tre´sci
1 Wst˛ep 1
1.1 Weryfikacja jako´sci i bezpiecze´nstwa systemów informatycznych . . . 1
1.1.1 Metody formalne . . . 2
1.1.2 Weryfikacja modelowa . . . 3
1.2 Przedstawienie problemu . . . 4
1.3 Cel bada´n i teza pracy . . . 5
1.3.1 Formalna teza rozprawy . . . 6
1.4 Zawarto´s´c rozprawy . . . 6
2 Podstawy j˛ezyka Alvis 9 2.1 Przeznaczenie j˛ezyka . . . 9
2.2 Podstawowe koncepcje . . . 9
2.3 Modelowanie systemów . . . 11
2.3.1 Model nieczasowy . . . 11
2.3.2 Model czasowy . . . 12
2.4 Reprezentacja przestrzeni stanów . . . 13
2.4.1 Stan modelu . . . 13 2.4.2 Tranzycje . . . 14 2.4.3 Grafy LTS . . . 16 2.5 ´Srodowisko Alvis . . . 19 2.5.1 Narz˛edzia modelowania . . . 19 2.5.2 Narz˛edzia weryfikacji . . . 19
2.6 Powi ˛azane formalizmy . . . 20
2.6.1 Sieci Petriego . . . 21
2.6.2 Algebry procesów . . . 21
2.6.3 Automaty czasowe . . . 22
2.6.4 Statechart . . . 22
SPIS TRE ´SCI viii
3 Intermediate Haskell Representation 24
3.1 Paradygmat funkcyjny . . . 24
3.2 J˛ezyk Haskell . . . 25
3.3 Posta´c po´srednia IHR . . . 25
3.4 Reprezentacja modelu w postaci IHR . . . 26
3.5 Wyliczanie grafu LTS . . . 29
3.6 Dodatkowe opcje generacji . . . 30
4 Weryfikacja modelowa 32 4.1 Weryfikacja modelowa . . . 32
4.1.1 Idea . . . 32
4.1.2 Proces weryfikacji . . . 33
4.1.3 Silne i słabe strony . . . 33
4.2 Systemy tranzycyjne . . . 34 4.3 Logiki temporalne . . . 36 4.3.1 LTL . . . 37 4.3.2 CTL . . . 38 4.3.3 RTCTL . . . 41 4.3.4 Rachunek µ . . . 43 4.4 Podstawowe techniki . . . 46 4.5 Narz˛edzia . . . 48 4.5.1 SPIN . . . 48 4.5.2 NuSMV / nuXmv . . . 49 4.5.3 CADP . . . 50 4.5.4 PRISM . . . 52 4.5.5 UPPAAL . . . 53
5 Translacja etykietowanego systemu przej´s´c do SMV 54 5.1 Model LTS w j˛ezyku SMV . . . 54
5.2 Algorytm translacji grafu LTS do SMV . . . 55
5.3 Testy rozwi ˛azania . . . 62
5.3.1 Opis systemu zwrotnicowego . . . 62
5.3.2 Model systemu w j˛ezyku Alvis . . . 64
5.3.3 Specyfikacja własno´sci systemu . . . 64
5.3.4 Testy podej´scia w narz˛edziu nuXmv . . . 66
SPIS TRE ´SCI ix
5.3.5 Podsumowanie wyników . . . 68
5.4 Podsumowanie . . . 69
6 Wykorzystanie rozwi ˛aza´n chmurowych do weryfikacji modeli Alvis 70 6.1 Chmury obliczeniowe . . . 70
6.1.1 Wirtualizacja zasobów . . . 71
6.1.2 Modele usług chmurowych . . . 71
6.1.3 Dostawcy rozwi ˛aza´n chmurowych . . . 71
6.1.4 Zalety rozwi ˛aza´n chmurowych . . . 72
6.2 Proces weryfikacji modelowej w chmurze . . . 73
6.2.1 Mo˙zliwo´sci . . . 73
6.2.2 Proces weryfikacji . . . 73
6.2.3 Automatyzacja . . . 75
6.3 Testy rozwi ˛azania . . . 77
6.3.1 Parametry instancji . . . 77
6.3.2 Modele testowe . . . 78
6.3.3 Podsumowanie wyników . . . 78
6.4 Podsumowanie . . . 79
7 Analiza przestrzeni stanów z poziomu postaci po´sredniej 81 7.1 Wykorzystanie postaci po´sredniej IHR . . . 81
7.1.1 Funkcje filtruj ˛ace . . . 81
7.1.2 Problemy funkcji filtruj ˛acych . . . 83
7.2 Alvis Query Language . . . 83
7.2.1 Umiejscowienie w procesie . . . 83
7.2.2 Dost˛epne funkcje . . . 85
7.2.3 Przykłady u˙zycia AQL . . . 86
7.2.4 Weryfikacja wykorzystuj ˛aca AQL na przykładowym modelu . . . 90
7.3 Testy rozwi ˛azania . . . 92
7.3.1 Parametry maszyn testowych . . . 93
7.3.2 Wyniki testów . . . 93
7.3.3 Porównanie z wynikami weryfikacji w nuXmv . . . 94
7.4 Podsumowanie . . . 95
SPIS TRE ´SCI x
A Listingi warstw kodu dla przykładów testowanych modeli systemów 100
A.1 Centrala sygnalizacji po˙zarowej . . . 100 A.2 Zwrotnica tramwajowa . . . 104 A.3 Producent-konsument . . . 106
Bibliografia 108
Rozdział 1
Wst˛ep
1.1 Weryfikacja jako´sci i bezpiecze´nstwa systemów informatycznych
Systemy informatyczne wykorzystywane s ˛a powszechnie w praktycznie ka˙zdej gał˛ezi przemysłu. Co-dzienne funkcjonowanie zarówno pojedynczych osób jak i całych gospodarek jest obecnie uzale˙znione ich prawidłowego funkcjonowania. W dobie transformacji cyfrowej równie˙z komercyjny sukces firm zale˙zy od funkcjonowania wykorzystywanych i udost˛epnianych przez nie systemów i aplikacji. Z tych powodów za-pewnienie wysokiej jako´sci i bezawaryjno´sci systemów informatycznych jest obecnie kluczowym aspektem wytwarzania oprogramowania.
Mo˙zna wskaza´c wiele przykładów, kiedy bł˛edy oprogramowania spowodowały ogromne straty. Do naj-popularniejszych nale˙z ˛a:
• wybuch rakiety Ariane 5 – Wybuch spowodowany był fałszywym zało˙zeniem, ˙ze oprogramowanie z rakiety Ariane 4 powinno działa´c równie dobrze na rakiecie Ariane 5. Pracuj ˛acy nad oprogramowa-niem in˙zynierowie nie przewidzieli jednak, ˙ze wi˛eksza moc silników w nowszym modelu spowoduje bł ˛ad konwersji 64-bitowej liczby zmiennoprzecinkowej na 16-bitow ˛a liczb˛e całkowit ˛a. Straty oszaco-wane zostały na około 500 mln dolarów.
• katastrofa lotu Lufthansa 2904 – system hamowania samolotu zadziałał za pó´zno, poniewa˙z lewe koło dotkn˛eło ziemi 9 sekund pó´zniej ni˙z prawe. Z powodu działania silnego wiatru oraz tafli wody na płycie lotniska koła nie uzyskały tej samej pr˛edko´sci k ˛atowej, wi˛ec system uznał, ˙ze nie dotkn˛eły podło˙za. W wyniku uderzenia i powstałego po˙zaru ´smier´c poniosły 2 osoby, a 56 zostało rannych. • awaria Therac-25 – kolejnym przykładem fatalnego w skutkach bł˛edu jest bł ˛ad który wyst˛epował
w kanadyjskiej maszynie do radioterapii nowotworów. Bł ˛ad oprogramowania powodował, ˙ze przy pewnej kombinacji klawiszy wykonanej w ci ˛agu 8 sekund uruchomiany zostawał wysokoenerge-tyczny tryb promieniowania bez przesłoni˛ecia głowicy filtrem dyspersyjnym. W efekcie pacjenci otrzymywali nawet 100 razy silniejsz ˛a, skupion ˛a wi ˛azk˛e promieniowania skierowan ˛a w jeden punkt
1.1. Weryfikacja jako´sci i bezpiecze´nstwa systemów informatycznych 2
na ciele. Nim bł ˛ad został wykryty i naprawiony ´smier´c poniosło 5 pacjentów.
• pomyłka rakietowego systemu ziemia-powietrze Patriot – Bł ˛ad w konwersji czasu generuje opó´znie-nie zegara systemowego, które przez 100 godzin działania systemu narasta do1/3sekundy. W efekcie
system radarowy, który wykrył nadlatuj ˛ac ˛a rakiet˛e przeskanował fragment nieba oddalony o ponad 600metrów od faktycznego i nie potwierdził zagro˙zenia. W skutek tego obronna rakieta Patriot nie wystartowała, a nadlatuj ˛acy pocisk trafił w baz˛e, zabijaj ˛ac 28 ˙zołnierzy.
Innym bardzo istotnym czynnikiem decyduj ˛acym o procesie wytwarzania oprogramowania jest aspekt finansowy. Badania pokazuj ˛a, ˙ze koszty usuwania bł˛edów wzrastaj ˛a bardzo szybko wraz z przechodzie-niem projektu do kojenych etapów w cyklu wytwarzania oprogramowania. Usuni˛ecie bł˛edu wykrytego po produkcyjnym wdro˙zeniu systemu mo˙ze by´c nawet 500 razy dro˙zsze ni˙z wykrycie na wczesnym etapie projektowania [6]. Przy wytwarzaniu zło˙zonych systemów, weryfikacja zajmuje w praktyce wi˛ecej czasu i pochłania wi˛ecej zasobów ni˙z sam implementacja.
Najcz˛e´sciej spotykanym podej´sciem do sprawdzania niezawodno´sci oprogramowania jest weryfikacja napisanego kodu. Jednak testowaniem nie mo˙zna wykaza´c braku bł˛edów danego systemu – mo˙zna jedynie wykaza´c ich obecno´s´c. Jest tak, poniewa˙z kompletna analiza istniej ˛acego kodu systemu nie jest mo˙zliwa. Jak dobitnie pokazuj ˛a wymienione wy˙zej przykłady katastrofalnych w skutkach bł˛edów, dla niektórych systemów testowanie kodu nie jest wystarczaj ˛acym zabezpieczeniem przed potencjalnymi awariami.
1.1.1 Metody formalne
Jednym z mo˙zliwych rozwi ˛aza´n jest zastosowanie metod formalnych. Metody formalne maj ˛a na celu usys-tematyzowanie procesu wytwarzania oprogramowania ju˙z od fazy specyfikacji. Formalne wyra˙zenie specy-fikacji systemu pozwala wyeliminowa´c z niej bł˛edy takie jak niekompletno´s´c czy dwuznaczno´s´c.
Zastosowanie metod formalnych w procesie wytwarzania oprogramowania mo˙ze znacz ˛aco ograniczy´c liczb˛e wykonywanych testów, a tak˙ze zagwarantowa´c produkt wy˙zszej jako´sci. Idea wspierania procesu wytwarzania oprogramowania przez metody formalne staje si˛e przez to w ostatnich latach coraz bardziej popularna. Metody formalne maj ˛a szczególne zastosowanie w odniesieniu do systemów (lub komponen-tów systemów), w stosunku do których oczekiwane jest zapewnienie bardzo wysokich gwarancji spełnienia wskazanych własno´sci, w tym twardych wymaga´n czasowych czy braku wyst˛epowania wyspecyfikowanych stanów niepo˙z ˛adanych. Szczególnym przykładem s ˛a tutaj systemy okre´slane jako krytyczne ze wzgl˛edu na bezpiecze´nstwo [51]. Terminem tym okre´slane s ˛a systemy, których awarie lub bł˛edy mog ˛a mie´c wpływ na ˙zycie lub zdrowie ludzi, ´srodowisko naturalne czy te˙z spowodowa´c istotne straty ekonomiczne. W przy-padku tych systemów proces wytwarzania oprogramowania jest szczególnie skomplikowany i musi by´c ´sci´sle regulowany. Bior ˛ac to pod uwag˛e wprowadzono szereg norm zalecaj ˛acych lub wr˛ecz wymagaj ˛acych stosowania w procesie metod formalnych. Przykładowo ITSEC (Information Technology Security
1.1. Weryfikacja jako´sci i bezpiecze´nstwa systemów informatycznych 3
ation Criteria) wprowadził konieczno´s´c ich stosowania w procesie ewaluacji oprogramowania dla czterech z siedmiu zdefiniowanych poziomów bezpiecze´nstwa. Dodatkowo norma Common Criteria (ISO 15408) rekomenduje zastosowanie metod formalnych powy˙zej pi ˛atego poziomu bezpiecze´nstwa.
Oprócz systemów krytycznych ze wzgl˛edu na bezpiecze´nstwo, metody formalne ciesz ˛a si˛e powszech-nym uznaniem przy weryfikacji systemów wbudowanych cechuj ˛acych si˛e współbie˙zno´sci ˛a działania oraz systemów czasu rzeczywistych. Specyficzne własno´sci takich systemów (np. przewidywalno´s´c, oczekiwa-nie terminowo´sci odpowiedzi, współbie˙zno´s´c działania poszczególnych komponentów itp.) powoduj ˛a, ˙ze bł˛edy w takich systemach s ˛a niezwykle trudne do wykrycia w oparciu o testy oprogramowania.
Metody formalne coraz cz˛e´sciej stosowane s ˛az powodzeniem tak˙ze w innych obszarach in˙zynierii opro-gramowania, w szczególno´sci w specyfikacji protokołów komunikacyjnych [1] i bezpiecze´nstwa [96][19], rozwi ˛aza´n IoT [94], pojazdów autonomicznych [79], jak równie˙z w robotyce [76] czy zarz ˛adzaniu ener-gi ˛a [101].
Intensywne badania spowodowały powstanie szeregu formalizmów i metod ich weryfikacji, jak rów-nie˙z narz˛edzi do ich praktycznego zastosowania. Ci ˛agły wzrost mo˙zliwo´sci obliczeniowych komputerów sprawił, ˙ze obecnie narz˛edzia te s ˛a w stanie weryfikowa´c nawet bardzo zło˙zone systemy. Do najbardziej po-pularnych metod formalnych zaliczane s ˛a Sieci Petriego [68][91][102], automaty czasowe [11][4] i algebry procesów [12][90][18].
1.1.2 Weryfikacja modelowa
Najwa˙zniejsz ˛a technik ˛a automatycznej analizy oprogramowania, nale˙z ˛ac ˛a do metod formalnych, jest obec-nie weryfikacja modelowa (ang. model checking). Metoda ta opiera si˛e na analizie zbioru wszystkich mo˙zli-wych stanów modelu systemu przygotowanego z u˙zyciem wybranej metody formalnej. Główna koncepcja weryfikacji modelowej poleaga na przedstawieniu modelu jako etykietowanego systemu przej´s´c (systemu tranzycyjnego), formalnej specyfikacji jego własno´sci za pomoc ˛a logik temporalnych, a nast˛epnie automa-tycznym sprawdzeniu prawdziwo´sci tych własno´sci w narz˛edziach typu model checker [33].
W tym podej´sciu zaprojektowany model jest weryfikowany jeszcze przed rozpocz˛eciem implementacji. Sprawdzenie wszystkich stanów danego systemu dostarcza za pomoc ˛amodel checkingu daje matematyczn ˛a gwarancj˛e zgodno´sci modelu z przygotowan ˛a specyfikacj ˛a.
Modele rzeczywistych systemów, nawet gdy s ˛a na wysokim poziomie abstrakcji, posiadaj ˛a miliony sta-nów i jeszcze wi˛ecej przej´s´c mi˛edzy nimi. Manualna analiza wszystkich mo˙zliwych ´scie˙zek jest praktycz-nie praktycz-niemo˙zliwa bez odpowiednich narz˛edzi - model checkerów. Wzrost zainteresowania wykorzystapraktycz-niem metod formalnych w procesie wytwarzania sprz˛etu i oprogramowania przyczynił si˛e do powstania wielu technik i narz˛edzi do model checkingu. Do najpopularniejszych mo˙zna zaliczy´c SPIN [61], NuSMV [28] / nuXmv [24], CADP [49], PRISM [58] oraz UPPAAL [41].
1.2. Przedstawienie problemu 4
1.2 Przedstawienie problemu
Problemem, który hamuje upowszechnienie metod formalnych jest to, ˙ze istniej ˛ace formalizmy s ˛a mało zrozumiałe dla przeci˛etnego in˙zyniera oprogramowania. Cz˛esto by stworzy´c model formalny nawet nie-skomplikowanego systemu potrzeba du˙zego do´swiadczenia oraz ilo´sci czasu, która cz˛esto jest zbyt du˙za do zaakceptowania. J˛ezyki specyfikacji modelu i jego własno´sci najcz˛e´sciej znacz ˛aco ró˙zni ˛a si˛e od j˛ezyków oprogramowania, które wykorzystywane s ˛a w in˙zynierii oprogramowania. Z tego te˙z powodu wi˛ekszo´s´c programistów, bardzo niech˛etnie podchodzi do wykorzystywania tych formalizmów. Cz˛esto dochodzi te˙z do sytuacji, w których mimo ˙ze system został poprawnie zamodelowany i zweryfikowany, to jest on pó´zniej bł˛ednie implementowany.
Tematyka rozprawy doktorskiej wpisuje si˛e w nurt prac badawczych dotycz ˛acych opracowywania for-malnych metod weryfikacji systemów. Opracowany w Katedrze Informatyki Stosowanej j˛ezyk Alvis [110] powstał jako wynik poszukiwania j˛ezyka modelowania, który z jednej strony byłby łatwy do opanowania przez in˙zyniera informatyka, a z drugiej pozwalał na formaln ˛a weryfikacj˛e wytworzonego modelu. J˛ezyk Alvis ł ˛aczy w sobie zalety graficznego j˛ezyka modelowania struktury systemu współbie˙znego z j˛ezykiem wysokiego poziomu stosowanym do opisu dynamiki poszczególnych komponentów zwanych agentami. W przypadku Alvisa ci˛e˙zkie podstawy matematyczne s ˛a ukrywane przed ko´ncowym u˙zytkownikiem bez ograniczania mo˙zliwo´sci i siły ekspresji formalizmu. Dzi˛eki swej przyst˛epno´sci i łatwo´sci zastosowania w procesie wytwarzania oprogramowania, j˛ezyk Alvis mo˙ze zosta´c bezpo´srednio wykorzystywany przez architektów systemów, bez ˙zadnych specjalnych umiej˛etno´sci i du˙zego do´swiadczenia w stosowaniu metod formalnych.
Alvis został stworzony szczególnie z my´sl ˛a o modelowaniu systemów współbie˙znych, czasu rzeczywi-stego, wbudowanych oraz rozproszonych [114]. Wspiera zarówno tworzenie modeli czasowych jak i nie-czasowych [115]. Wa˙zn ˛a cech ˛a j˛ezyka jest równie˙z mo˙zliwo´s´c tworzenia modeli hierarchicznych [108].
J˛ezyk Alvis został wyposa˙zony w zestaw narz˛edzi umo˙zliwiaj ˛acych modelowanie i analiz˛e systemów. Schemat standardowego procesu ich wykorzystania przedstawiono na rysunku 1.1.
Pierwszym jego etapem jest stworzenie modelu w programie Alvis Editor. Umo˙zliwia on definicj˛e za-równo warstwy kodu jak i diagramu komunikacji modelu. Model zapisywany jest w pliku XML, który kompilowany jest przez program Alvis Compiler. Wynikiem kompilacji jest powstanie postaci po´sredniej w j˛ezyku funkcyjnym Haskell [93]. Kod ten mo˙ze by´c bezpo´srednio skompilowany przy pomocy kom-pilatora GHC. Mo˙ze równie˙z zosta´c zmodyfikowany przez u˙zytkownika przy wykorzystaniu dowolnego edytora tekstu. Przykładami modyfikacji mo˙ze by´c implementacja własnych algorytmów weryfikacji czy zarz ˛adzania priorytetami. Ta mo˙zliwo´s´c ingerencji w kod warstwy po´sredniej jest szczególnie interesuj ˛ac ˛a własno´sci ˛a j˛ezyka Alvis z punktu widzenia rozprawy. Podstawowym rezultatem wykonania
1.3. Cel bada´n i teza pracy 5 Design of communication diagram Implementation of code layer Model design
|
{z
}
Alvis Editor|
{z
}
Alvis Compiler Alvis→Haskell Requirements / properties Implementation of filter functions Specification of re-quirements (µ calculus)|
{z
}
text editor Verification Verification with filter functions Model check-ing with CADP| {z }
LTS
|
{z
}
GHC, CADP Rysunek 1.1: Oryginalny proces projektowania i analizy modeli rozwijanych w j˛ezyku Alvis. nego kodu w j˛ezyku Haskell jest generacja etykietowanego systemu przej´s´c (Labelled Transition System, LTS), który stanowi reprezentacj˛e przestrzeni stanów modelu.
Oryginalne podej´scie do formalnej weryfikacji systemów modelowanych z zastosowaniem j˛ezyka Alvis bazowało wła´snie na generacji grafu LTS, wyeksportowaniu go do wybranego zewn˛etrznego formatu za-pisu, a nast˛epnie zastosowaniu zewn˛etrznych narz˛edzi do analizy własno´sci uzyskanego grafu. Jako przy-kład realizacji takiego podej´scia zaimplementowano mo˙zliwo´s´c eksportu grafu LTS do formatu Aldebaran, akceptowanego przez moduł Evaluator z pakietu CADP [49].
Narz˛edzie CADP Evaluator było dotychczas jedynym model checkerem, w którym mo˙zliwa była wery-fikacja modeli Alvis. Narz˛edzie to pozwalało co prawda na weryfikacj˛e własno´sci dla systemów o wysokiej zło˙zono´sci, jednak tylko pod k ˛atem przebiegu wykonywanych akcji, poniewa˙z proces translacji do formatu Aldebaran odrzuca wszystkie informacje o stanie modelu. W szczególno´sci wi˛ec przy wykorzystaniu tego podej´scia nie jest mo˙zliwe sprawdzenie konkretnych stanów i warto´sci zmiennych w tych stanach.
1.3 Cel bada´n i teza pracy
Celem niniejszej rozprawy doktorskiej jest opracowanie podej´s´c umo˙zliwiaj ˛acych skuteczn ˛aformaln ˛awery-fikacj˛e modeli w j˛ezyku Alvis, ze szczególnym nastawieniem na wykorzystanie postaci po´sredniej modelu w j˛ezyku Haskell. Opracowane w ramach prac podej´scia powinny pozwala´c na weryfikacj˛e opart ˛a o stan modelu, rozszerzaj ˛ac tym samym ograniczone mo˙zliwo´sci weryfikacji dost˛epne w narz˛edziu CADP Evalu-ator.
1.4. Zawarto´s´c rozprawy 6
Aby mo˙zliwe było powszechne zastosowanie j˛ezyka formalnego w in˙zynierii oprogramowania, pakiet Alvis musi umo˙zliwia´c kompleksow ˛a analiz˛e zło˙zonych systemów (liczba stanów przekraczaj ˛aca 106) na
standardowym sprz˛ecie komputerowym w akceptowalnym przedziale czasu. Brak takiej mo˙zliwo´sci sku-tecznie blokuje szersze wykorzystanie tego podej´scia w procesie wytwarzania oprogramowania.
Warto podkre´sli´c, ˙ze proponowane podej´scie powinno by´c zintegrowane z istniej ˛acymi narz˛edziami do modelowania systemów w j˛ezyku Alvis. Aby dodatkowo ułatwi´c wykorzystanie rozwi ˛azania, powinien zosta´c stworzony j˛ezyk zapyta´n umo˙zliwiaj ˛acy intuicyjn ˛a weryfikacj˛e własno´sci modelowanego systemu, takich jak brak zakleszcze´n czy brak stanów niepo˙z ˛adanych. Dzi˛eki temu u˙zytkownik nie b˛edzie musiał ingerowa´c bezpo´srednio w kod postaci po´sredniej ani te˙z pisa´c pełnego programu w j˛ezyku Haskell w celu wykorzystania opracowanych algorytmów analizy.
1.3.1 Formalna teza rozprawy
Formalna teza rozprawy zdefiniowana została nast˛epuj ˛aco:
Mo˙zliwe jest opracowanie skutecznych algorytmów formalnej weryfikacji własno´sci systemów współ-bie˙znych rozwijanych w j˛ezyku Alvis z wykorzystaniem paradygmatu funkcyjnego i po´sredniej reprezentacji modelu wyra˙zonej w j˛ezyku Haskell.
Teza została zweryfikowana w rozprawie poprzez:
• Opracowanie metod formalnej analizy modeli w j˛ezyku Alvis na podstawie ich postaci po´sredniej w j˛ezyku Haskell.
• Opracowanie algorytmów umo˙zliwiaj ˛acych analiz˛e modeli systemów zawieraj ˛acych przynajmniej 106stanów.
• Opracowanie j˛ezyka zapyta´n umo˙zliwiaj ˛acego intuicyjne wykorzystanie opracowanych algorytmów analizy do weryfikacji własno´sci zamodelowanych systemów.
• Implementacj˛e opracowanych algorytmów w j˛ezyku funkcyjnym Haskell i ich integracj˛e z istniej ˛a-cymi narz˛edziami modelowania w j˛ezyku Alvis.
• Demonstracj˛e wła´sciwo´sci proponowanego podej´scia w oparciu o przykłady systemów współbie˙z-nych i systemów czasu rzeczywistego.
W pracy zaproponowano równie˙z podej´scie bazuj ˛ace na wykorzystaniu czołowego narz˛edzia do weryfi-kacji modelowej, nuXmv [24]). W celu dodatkowego zwi˛ekszenia mo˙zliwo´sci obu podej´s´c zaproponowane zostało dodatkowo wykorzystanie rozwi ˛aza´n chmurowych w formalnym procesie analizy modeli Alvis.
1.4 Zawarto´s´c rozprawy
Niniejsz ˛a rozpraw˛e rozpoczyna wprowadzenie do modelowania w j˛ezyku Alvis przedstawiaj ˛ace podsta-wowe koncepcje j˛ezyka i dost˛epne narz˛edzia, równie˙z zestawiaj ˛ac Alvisa z popularnymi formalizmami
1.4. Zawarto´s´c rozprawy 7
zwalaj ˛acymi na weryfikacj˛e czasowych i nieczasowych, dyskretnych systemów współbie˙znych. Nast˛epnie opisana jest dokładnie posta´c po´srednia modelu w j˛ezyku Haskell, b˛ed ˛aca kluczowym elementem j˛ezyka z punktu widzenia rozprawy. Przed przyst ˛apieniem do wprowadzenia proponowanych w pracy podej´s´c do weryfikacji modeli Alvis, przedstawiona jest jeszcze ogólna koncepcja model checkingu, wraz z opisem dost˛epnych j˛ezyków specyfikacji własno´sci systemów oraz popularnych narz˛edzi do model checkingu.
Po tak przygotowanej podstawie, zaproponowane s ˛a trzy komplementarne podej´scia do weryfikacji mo-deli Alvis. Pierwsze z nich polega na translacji grafów LTS do formatu SMV i pó´zniejsz ˛a weryfikacj˛e modelu w narz˛edziu nuXmv. Drugie polega na wykorzystaniu chmur obliczeniowych do zwi˛ekszenia mak-symalnego rozmiaru modelu mo˙zliwego do formalnej weryfikacji za pomoc ˛astworzonych narz˛edzi. Trzecie to wprowadzenie j˛ezyka zapyta´n Alvis Query Language, operuj ˛acego bezpo´srednio na postaci po´sredniej w j˛ezyku Haskell. Do ka˙zdego z tych podej´s´c przedstawiono wyniki testów przy weryfikacji przygotowa-nych modeli systemów współbie˙zprzygotowa-nych, w tym systemu zwrotnicowego oraz centrali sygnalizacji po˙zarowej. Pod koniec rozprawy przedstawione zostało porównanie mo˙zliwo´sci i wydajno´sci wprowadzonych w niej podej´s´c do weryfikacji.
Zawarto´s´c poszczególnych rozdziałów rozprawy (pomijaj ˛ac wst˛ep) została ukształtowana nast˛epuj ˛aco: • Rozdział 2 przedstawia podstawowe koncepcje j˛ezyka Alvis oraz metody modelowania systemów
w tym formalizmie. Wprowadzono w nim równie˙z grafy LTS, stanowi ˛ace reprezentacj˛e przestrzeni stanów modelu. Grafy LTS s ˛a szczególnie istotne z punktu widzenia wprowadzonych w kolejnych rozdziałach weryfikacji modelowej. W rozdziale przedstawiono równie˙z porównanie j˛ezyka Alvis z innymi formalizmami o podobnym zastosowaniu, takimi jak sieci Petriego, algebry procesów, auto-maty czasowe, Statechart i PRISM.
• Rozdział 3 opisuje sposób reprezentacji modelu w postaci po´sredniej w j˛ezyku Haskell, ze szcze-gólnym uwzgl˛ednieniem sposobu reprezentacji stanów i dynamiki modelu. Na jego wst˛epie przed-stawiono ogóln ˛a koncepcj˛e paradygmatu funkcyjnego oraz opisano zalety j˛ezyka Haskell. Nast˛epnie opisano w jaki sposób wyliczana jest przestrze´n stanów i w jaki sposób generowane s ˛a grafy LTS. • Rozdział 4 przybli˙za ide˛e weryfikacji modelowej. Opisane zostały równie˙z popularne j˛ezyki opisu
własno´sci systemów: LTL, CTL, RTCTL i rachunek µ. Dokonana została równie˙z analiza najnow-szych narz˛edzi do weryfikacji modelowej pod k ˛atem mo˙zliwo´sci integracji z istniej ˛acym pakietem narz˛edziowym Alvisa.
• Rozdział 5 prezentuje pierwsze podej´scie do umo˙zliwienia kompleksowej weryfikacji modeli w j˛e-zyku Alvis. Bazuje ono na translacji wyliczonej przestrzeni stanów systemu w postaci grafu LTS do j˛ezyka modelowania SMV, a nast˛epnie weryfikacji modelu w pakiecie nuXmv. Na pocz ˛atku rozdziału opisano sposób reprezentacji przestrzeni stanów w j˛ezyku SMV. Nast˛epnie wprowadzono autorski al-gorytm translacji pomi˛edzy Alvisow ˛a reprezentacj ˛a przestrzeni stanów a reprezentacji akceptowanej
1.4. Zawarto´s´c rozprawy 8
przez narz˛edzie nuXmv. Przedstawiono równie˙z narz˛edzie Alvis2ModelChecker, b˛ed ˛ace implemen-tacj ˛a wyprowadzonego algorytmu. Program ten pozwala na automatyczn ˛a generacj˛e plików modeli w formacie SMV z formatu dot eksportowanego przez skompilowany program Haskellowy. W roz-dziale pokazano równie˙z studium przypadków weryfikacji modeli rzeczywistych systemów współ-bie˙znych, w tym zwrotnicy tramwajowej oraz centrali sygnalizacji po˙zarowej. Pod koniec rozdziału przedstawione zostało podsumowanie wyników testów wydajno´sciowych zaproponowanego podej-´scia i uzasadniono, dlaczego podej´scie to nie pozwala obecnie na pełn ˛aanaliz˛e modeli o ilo´sci stanów przekraczaj ˛acej 105 na standardowym sprz˛ecie komputerowym.
• Rozdział 6 przedstawia wykorzystanie chmur obliczeniowych do weryfikacji modeli w nuXmv, umo˙zliwiaj ˛ac skuteczn ˛a weryfikacj˛e systemów zawieraj ˛acych nawet 106 stanów. Na pocz ˛atku
roz-działu wprowadzono koncepcj˛e chmur obliczeniowych oraz jakie prezentuj ˛a zalety mo˙zliwe do wy-korzystania w procesie weryfikacji oprogramowania. Nast˛epnie opisano proces weryfikacji modeli Alvis na instancjach zewn˛etrznych i sposoby jego automatyzacji z wykorzystaniem j˛ezyków skryp-towych. W rozdziale przedstawiono równie˙z wyniki testów proponowanego podej´scia na instancji Google Cloud Compute, w oparciu o wprowadzone w poprzednim rozdziale modele oraz ich bardziej rozbudowane wersje. Analizuj ˛ac wyniki wydajno´sciowe, pokazano, ˙ze zastosowanie tego podej´scia pozwala weryfikowa´c systemy posiadaj ˛ace ponad 105 stanów, jak równie˙z potencjalnie nawet 106
je˙zeli wykorzystane zostan ˛a odpowiednio mocne instancje.
• Rozdział 7 wprowadza nowatorskie podej´scie do problemu weryfikacji modeli Alvis poprzez opra-cowanie algorytmów formalnej weryfikacji własno´sci systemów współbie˙znych z wykorzystaniem po´sredniej reprezentacji modelu wyra˙zonej w j˛ezyku funkcyjnym Haskell. Pocz ˛atek po´swi˛econy jest koncepcji funkcji filtruj ˛acych, b˛ed ˛acych podstawowym sposobem wykorzystania warstwy po´sredniej do weryfikacji modelu. Nast˛epnie wprowadzono proces weryfikacji modeli Alvis za pomoc ˛a orygi-nalnego j˛ezyka zapyta´n Alvis Query Language (AQL). Rozdział zawiera opis zaimplementowanych funkcji, wraz z ich deklaracjami i przykładami u˙zycia. Nast˛epnie pokazano na przykładowym mo-delu Alvis, w jaki sposób za pomoc ˛a AQL mo˙zna opisywa´c własno´sci systemu i analizowa´c wyniki weryfikacji. Przeprowadzono równie˙z testy wydajno´sciowe rozwi ˛azania na przykładach modeli wpro-wadzonych w poprzednich rozdziałach. Na koniec dokonano porównania z poprzednimi podej´sciami i pokazano, jak zalety paradygmatu funkcyjnego umo˙zliwiaj ˛a weryfikacj˛e modeli o rozmiarze znacz-nie przekraczaj ˛acym 106.
• Rozdział 8 jest podsumowaniem pracy. Zawiera wnioski ko´ncowe oraz sugerowane kierunki dalszych bada´n i rozwoju j˛ezyka oraz narz˛edzi modelowania Alvis.
Rozdział 2
Podstawy j˛ezyka Alvis
2.1 Przeznaczenie j˛ezyka
Alvis [110][111][109] jest formalnym j˛ezykiem modelowania opracowanym i rozwijanym na Katedrze In-formatyki Stosowanej AGH w Krakowie. Główn ˛a motywacj ˛a do jego stworzenia było dostarczenie prze-ci˛etnemu in˙zynierowi lub programi´scie formalnego j˛ezyka, który mógłby by´c przez niego z łatwo´sci ˛a zro-zumiany, a jednocze´snie pozwalał na zamodelowanie i weryfikacj˛e zło˙zonych systemów współbie˙znych. W tym celu Alvis ł ˛aczy w sobie zalety wysokopoziomowych j˛ezyków programowania z wizualnym j˛ezy-kiem modelowania słu˙z ˛acym do modelowania kanałów komunikacji pomi˛edzy podsystemami.
Jego najwi˛eksz ˛a przewag ˛a na klasycznymi metodami formalnymi, takimi jak Sieci Pe-triego [68][91][102] automaty czasowe [11][4] i algebry procesów [12][90][18], jest bardzo przyjazna in˙zynierowi składnia. Teoretyczne podstawy matematyczne zostały ukryte pod łatwo przyswajalnymi dla programisty instrukcjami j˛ezyka programowania i przejrzystym modelem komunikacji, bez straty dla potencjału i ekspresywno´sci formalizmu. B˛ed ˛ac j˛ezykiem formalnym, Alvis ma niezaprzeczaln ˛a przewag˛e nad popularnymi j˛ezykami programowania – modele zaprojektowane w j˛ezyku Alvis mog ˛a by´c formalnie zweryfikowane przy wykorzystaniu technik weryfikacji modelowej [6].
U˙zywaj ˛ac j˛ezyka Alvis, przeci˛etny in˙zynier oprogramowania jest w stanie zamodelowa´c i zweryfikowa´c nawet zło˙zone systemy, które pó´zniej mog ˛a zosta´c z łatwo´sci ˛a zaimplementowane. Potwierdzenie popraw-no´sci modelu jest szczególnie wa˙zne w systemach współbie˙znych i rozproszonych, gdzie tradycyjne metody testowania oprogramowania nie zawsze mog ˛a zosta´c zastosowane.
2.2 Podstawowe koncepcje
Model w j˛ezyku Alvis mo˙zna opisa´c jako kolekcj˛e podsystemów nazwanych agentami, które działaj ˛a rów-nolegle, komunikuj ˛a si˛e ze sob ˛a, rywalizuj ˛a o współdzielone zasoby itd. Koncepcja agenta została
zaczerp-2.2. Podstawowe koncepcje 10
ni˛eta z algebry procesów CCS [90], [107] i rozszerzona wzgl˛edem koncepcji zastosowanych w formali´zmie [7]. W j˛ezyku Alvis u˙zywane s ˛a dwa typy agentów: aktywne i pasywne, których koncepcja przypomina za-dania i obiekty chronione znane z j˛ezyka Ada [23]. Agenty aktywne wykonuj ˛a pewne operacje i mog ˛a by´c traktowane jako w ˛atki w systemie współbie˙znym. Agenty pasywne zapewniaj ˛amechanizm wzajemnego wy-kluczania i synchronizacji danych. Powi ˛azania pomi˛edzy agentami s ˛a definiowane na diagramie komunika-cji – wizualnej cz˛e´sci j˛ezyka Alvis. Diagram ten jest grafem skierowanym, w którym agenty przedstawiane s ˛a jako w˛ezły, a kanały komunikacji mi˛edzy nimi przedstawiane s ˛a jako łuki [108].
Do zamodelowania zachowania agentów wykorzystywana jest warstwa kodu, która oferuje zaledwie kilkana´scie starannie wyselekcjonowanych instrukcji (patrz Rys. 2.1). Kod ´zródłowy modelu Alvisa jest w składni podobny do j˛ezyków wysokiego poziomu. Wyra˙zenia j˛ezyka Alvis mog ˛a równie˙z zawiera´c ele-menty j˛ezyka funkcyjnego Haskell [93], [110], co pozwala m.in. łatwo implementowa´c potrzebne w modelu typy danych i operacje realizowane na tych typach.
Modele bardziej zło˙zonych systemów mog ˛a zosta´c zaprojektowane z wykorzystaniem hierarchicznych diagramów komunikacji [109]. Diagramy hierarchiczne wprowadzaj ˛a koncepcj˛e w˛ezła hierarchicznego, który reprezentuje podsystem zdefiniowany na ni˙zszym poziomie. Takie rozwi ˛azanie umo˙zliwia opisanie systemu na kilku poziomach abstrakcji. W˛ezły hierarchiczne s ˛a podobne do podstawianych tranzycji stoso-wanych w hierarchicznych kolorostoso-wanych sieciach Petriego [68],[102].
Przegl ˛ad elementów graficznych j˛ezyka Alvis i instrukcji stosowanych w warstwie kodu zaprezento-wano na Rys. 2.1 [105]. agent aktywny agent pasywny agent hierarchiczny porty połaczenie jednokierunkowe połaczenie dwukierunkowe
wywołanie procedury wej´sciowej wywołanie procedury wyj´sciowej
• delay t; • exec x = expression; • exit; • in p x; • in (t) p x; • in (t) p x { success {...} fail {...} } • jump label; • loop (g) {...} • loop (every t) {...} • loop {...} • null; • out p x; • out (t) p x; • out (t) p x { success {...} fail {...} } • proc (g) p {...} • select { alt (g1) {...} alt (g2) {...} ... } • start A;
Agenty Kanały komunikacji Wyra˙zenia warstwy kodu
Rysunek 2.1: Elementy składni j˛ezyka Alvis.
2.3. Modelowanie systemów 11
2.3 Modelowanie systemów
2.3.1 Model nieczasowy
Podstawy modelowania w j˛ezyku Alvis przedstawimy na prostym przykładzie. Na rysunku 2.2 przedsta-wiony został model składaj ˛acy si˛e z dwóch agentów aktywnych A i C oraz agenta pasywnego B.
Rysunek 2.2: Prosty przykład modelu Alvis.
Zdefiniowane kanały komunikacji wskazuj ˛a, ˙ze agent A mo˙ze wysyła´c sygnały do agenta B za pomoc ˛a portu a1 oraz odbiera´c sygnały z agenta C za pomoc ˛aportu a2. Analogicznie agent C mo˙ze wysyła´c sygnały do agenta A za pomoc ˛aportu c2 i odbiera´c sygnały od agenta B za pomoc ˛aportu c1. Opis dynamiki agentów zawarty jest w warstwie kodu, przedstawionej na listingu 2.1.
Listing 2.1: Warstwa kodu dla modelu z Rys. 2.2
1 2 agent A{ 3 out a1; --1 4 in a2; --2 5 } 6 7 agent B{ 8 proc b1{ 9 in b1; --1 10 exit; --2 11 } 12 proc b2{ 13 out b2; --3 14 exit; --4
2.3. Modelowanie systemów 12 15 } 16 } 17 18 agent C{ 19 in c1; --1 20 out c2; --2 21 }
Agent A rozpoczyna swoje działanie od zapocz ˛atkowania komunikacji z agentem B poprzez instrukcj˛e out na porcie a1. Jest to przykład komunikacji agenta aktywnego z pasywnym, któr ˛a to mo˙ze zapocz ˛at-kowa´c wył ˛acznie agent aktywny. Je˙zeli agent B jest bezczynny i procedura (port) b1 jest dost˛epna, to jest ona wykonywana. Agent B w procedurze wej´sciowej b1 odbiera sygnał przez port b1 i ko´nczy działanie instrukcj ˛a exit. Nast˛epnie agent A wykonuje instrukcj˛e in a2, co oznacza prób˛e odebrania sygnału od agenta C. Tym razem jest to komunikacja dwóch agentów aktywnych. Zakładaj ˛ac, ˙ze to agent A zapocz ˛at-kował t˛e komunikacj˛e, to wykonuj ˛ac instrukcj˛e in przechodzi on w stan oczekiwania (tryb waiting), dopóki agent C nie sfinalizuje komunikacji wykonuj ˛ac instrukcj˛e out.
Agent C zachowuje si˛e podobnie do agenta A, z t ˛aró˙znic ˛a, ˙ze rozpoczyna działanie od próby wywołania procedury wyj´sciowej agenta B, a nast˛epnie komunikuje si˛e z agentem A wysyłaj ˛ac sygnał przez port c2. Po wykonaniu ostatniej instrukcji, zarówno agent A jak i C ko´ncz ˛a swoje działanie.
2.3.2 Model czasowy
Ten sam model mo˙ze zosta´c przedstawiony równie˙z w wersji czasowej. Nie wymaga to ˙zadnej bezpo´sred-niej zmiany w modelu. To czy model zostanie potraktowany jako czasowy czy nie, zale˙zy od u˙zytych opcji kompilatora. W modelach czasowych u˙zytkownik mo˙ze zdefiniowa´c czas trwania ka˙zdej z instrukcji mo-delu. Domy´slnie długo´s´c ka˙zdej instrukcji wynosi jedn ˛ajednostk˛e czasu. Warto´sci domy´slne mo˙zna zmieni´c edytuj ˛ac wygenerowan ˛a dla modelu funkcj˛e duration. Na listingu 2.2 zaprezentowana została funkcja du-ration dla czasowej wersji modelu 2.2, gdzie czas trwania instrukcji out, in oraz exit został ustawiony odpowiednio na 3, 2 i 1 jednostk˛e czasu.
Listing 2.2: Funkcja Duration dla czasowej wersji modelu z Rys. 2.2
1
2 -- | Returns the duration for the given agent and statement number.
3 duration :: Agent -> Int -> Int
4 duration A 1 = 3
5 duration A 2 = 2
6 duration B 1 = 2
7 duration B 2 = 1
2.4. Reprezentacja przestrzeni stanów 13 8 duration B 3 = 3 9 duration B 4 = 1 10 duration C 1 = 2 11 duration C 2 = 3 12 duration _ _ = 1
2.4 Reprezentacja przestrzeni stanów
2.4.1 Stan modelu
Stan modelu Alvis jest reprezentowany przez list˛e stanów wszystkich jego agentów aktywnych i pasywnych. Ka˙zdy stan pojedynczego agenta mo˙ze by´c jednoznacznie opisany przez informacje zawarte w nast˛epuj ˛acej czwórce:
Definicja 2.4.1. Stan agenta X jest krotk ˛a:
S(X) = (am(X), pc(X), ci(X), pv(X)), (2.1)
gdzie am(X) jest trybem agenta (agent mode), pc(X) jest licznikiem rozkazów (program counter), za´s ci(X) jest list ˛a kontekstow ˛a (context information), pv(X) jest krotk ˛a parametrów (parameters values).
Do ka˙zdego z symboli am, pc, ci i pv mo˙ze by´c dodany w indeksie numer stanu, np. pvSi, aby wskaza´c którego stanu dana warto´s´c dotyczy.
Tryb agenta mo˙ze przyjmowa´c nast˛epuj ˛ace warto´sci: Finished (F), Init (I), Running (X) and Taken (T). Tryb Finished oznacza, ˙ze agent zako´nczył swoje działanie. Warto´sc Init jest domy´slnym trybem w ja-kim znajduj ˛a si˛e agenty, które nie s ˛a uruchamiane w stanie pocz ˛atkowym. Tryb Running oznacza, ˙ze agent wykonuje jedn ˛a ze swoich instrukcji. Tryb Taken oznacza, ˙ze jedna z procedur agenta pasywnego została wywołana i agent wykonuje instrukcje w niej zamieszczone. Tryb Waiting, dla agentów pasywnych oznacza, ˙ze agent nie wykonuje ˙zadnej instrukcji i oczekuje na to, by inny agent wywołał jedn ˛a z dost˛epnych pro-cedur. Dla agentów aktywnych tryb ten oznacza, ˙ze agent albo oczekuje na komunikacj˛e z innym agentem aktywnym, albo oczekuje na obecnie niedost˛epn ˛a procedur˛e agenta pasywnego.
Licznik rozkazów wskazuje na aktualny numer instrukcji agenta. Mo˙ze to by´c kolejna instrukcja do wykonania, albo instrukcja która została ju˙z rozpocz˛eta, ale agent oczekuje na działanie innego agenta, aby móc j ˛a zako´nczy´c (np. przy komunikacji mi˛edzy agentami).
Lista kontekstowa zawiera dodatkowe informacje o obecnym stanie agenta. Przykładowo, gdy agent jest w trybie waiting, lista kontekstowa zawiera informacje o zdarzeniach, na które agent czeka.
2.4. Reprezentacja przestrzeni stanów 14
Definicja 2.4.2. Stan modelu A, zawieraj ˛acego agentyA = {X1, ..., Xn} jest krotk ˛a
S= (S(X1), ..., S(Xn)). (2.2)
Koncepcja stanu modelu w j˛ezyku Alvis została zobrazowana na rysunku 2.3.
Agenty modelu z }| { ((am1, pc1, ci1, pv1), . . . , agent aktywny z }| { (ami, pci, cii, pvi), . . . , agent pasywny z }| { (amj, pcj, cij, pvj), . . . , (amn, pcn, cin, pvn)) I – init F– finished W– waiting X – running tryb agenta numer obecnej instrukcji licznik rozkazów dodatkowe informacje o stanie, np. wywołane procedury lista kontekstowa aktualne warto´sci parametrów agenta krotka parametrów W– waiting T– taken tryb agenta
Rysunek 2.3: Reprezentacja stanu modelu w j˛ezyku Alvis.
2.4.2 Tranzycje
Z teoretycznego punktu widzenia instrukcje wyst˛epuj ˛ace w warstwie kodu modelu s ˛a reprezentowane po-przez tzw. tranzycje. Ka˙zda z instrukcji pokazanych na Rys. 2.1 z wyj ˛atkiem proc jest reprezentowana przez co najmniej jedn ˛a tranzycj˛e. W przypadku instrukcji komunikacji (in,out) stosowanych jest kilka tranzycji, aby odró˙zni´c od siebie ró˙zne warianty komunikacji np. czy jest to rozpocz˛ecie, czy zako´nczenie komunikacji i czy jest to komunikacja z agentem aktywnym lub pasywnym.
Przyjmijmy, ˙ze X i Y s ˛a agentami zawieraj ˛acymi porty odpowiednio X.p i Y.q. W rozwa˙zanych w ni-niejszej rozprawie modelach mog ˛a wyst ˛api´c nast˛epuj ˛ace tranzycje:
• TDelay X– wykonanie instrukcjidelayprzez agenta X;
• TExec X– wykonanie instrukcji execprzez agenta X, tj. ewaluacja wyra˙zenia i przypisanie jego wyniku do parametru;
• TExit X– wykonanie instrukcjiexitprzez agenta X, tj. zako´nczenie pracy agenta aktywnego lub
zako´nczenie procedury agenta pasywnego;
• TIn X.p– wykonanie instrukcjiinprzez aktywnego agenta X (port X.p), rozumianej jako
inicjali-zowanie komunikacji z innym agentem;
• TInF X.p Y.p– wykonanie instrukcjiinprzez aktywnego agenta X (port X.p), rozumianej jako
finalizacja komunikacji z agentem Y (port Y.q);
• TInAP X.p Y.q– wykonanie instrukcjiinprzez aktywnego agenta X (port X.p), rozumianej jako
wywołanie dost˛epnej procedury wyj´sciowej Y.q;
2.4. Reprezentacja przestrzeni stanów 15
• TInPP X.p Y.q– wykonanie instrukcjiinprzez pasywnego agenta X (port X.p, rozumianej jako wywołanie dost˛epnej procedury wyj´sciowej Y.q;
• TJump X– wykonanie instrukcjijumpprzez agenta X;
• TLoop X– wykonanie instrukcjiloop(z lub bez warunku logicznego) przez agenta X, tj. ewaluacja warunku p˛etli (je´sli wyst˛epuje) i ewentualne przej´scie do jej wn˛etrza;
• TLoopEvery X– wykonanie instrukcjiloop everyprzez agenta X, tj. wej´scie do wn˛etrza p˛etli okresowej;
• TNull X– wykonanie instrukcjinullprzez agenta X;
• TOut X.p– wykonanie instrukcjioutprzez aktywnego agenta X (port X.p), rozumianej jako ini-cjalizowanie komunikacji z innym agentem;
• TOutF X.p Y.p– wykonanie instrukcjioutprzez aktywnego agenta X (port X.p), rozumianej jako finalizacja komunikacji z agentem Y (port Y.q);
• TOutAP X.p Y.q– wykonanie instrukcjiout przez aktywnego agenta X (port X.p), rozumianej jako wywołanie dost˛epnej procedury wej´sciowej Y.q;
• TOutPP X.p Y.q– wykonanie instrukcjiout przez aktywnego agenta X (port X.p), rozumianej jako wywołanie dost˛epnej procedury wej´sciowej Y.q;
• TSelect X– wykonanie instrukcjiselectprzez agenta X, tj. ewaluacja warunków poszczególnych
alternatyw i ewentualne wybranie jednej z nich;
• TStart X– wykonanie instrukcjistartprzez agenta X.
Słowo kluczoweprocu˙zyte jest jedynie w celu organizacji kodu agent pasywnego i jest pomijane przy numerowaniu instrukcji kodu, dlatego te˙z nie przewiduje si˛e ˙zadnej tranzycji w tym przypadku.
Do pełnego opisu zmian stanów modelu wymagane jest uwzgl˛ednienie tzw. tranzycji systemowych, które reprezentuj ˛a zmiany w stanie modelu wprowadzane przez „´srodowisko uruchomieniowe”:
• STInAP X.p Y.q,STInPP X.p Y.q,STOutAP X.p Y.q,STOutPP X.p Y.q– reprezentuj ˛asy-tuacje, gdy po upływie oczekiwania na niedost˛epne procedury agent X, który zainicjalizował ko-munikacj˛e, jest budzony przez ´srodowisko systemu wtedy, gdy procedura, na któr ˛a czekał, staje si˛e dost˛epna;
• STDelayEnd X– reprezentuje wybudzenie agenta X, zaraz po tym jak upłyn ˛ał okres zawieszenia agenta, b˛ed ˛acy wynikiem wykonania instrukcjidelay.
• STLoopEnd X – reprezentuje wybudzenie agenta X, zwi ˛azane z zako´nczeniem bie˙z ˛acego okresu instrukcjiloop every.
• STInEnd X, STOutEnd X – reprezentuj ˛a wybudzenie agenta X, zaraz po tym jak upłyn ˛ał okres oczekiwania na finalizacj˛e komunikacji, która nie nast ˛apiła;
wy-2.4. Reprezentacja przestrzeni stanów 16
ł ˛acznie z upływu czasu.
2.4.3 Grafy LTS
Wykonanie dowolnego kroku jest wyra˙zone jako przej´scie pomi˛edzy formalnie zdefiniowanymi stanami mo-delu Alvis. Stany momo-delu i przej´scia mi˛edzy nimi s ˛a reprezentowane przy u˙zyciu etykietowanych systemów przej´s´c (grafów LTS). (0) A: (X,1,[],()) B: (W,0,[in(b1),out(b2)],()) C: (X,1,[],()) (1) A: (X,1,[proc(B.b1)],()) B: (T,1,[],()) C: (X,1,[],()) TOutAP(A.a1, B.b1) (2) A: (X,1,[],()) B: (T,3,[],()) C: (X,1,[proc(B.b2)],()) TInAP(C.c1, B.b2) (3) A: (X,1,[proc(B.b1)],()) B: (T,2,[],()) C: (X,1,[],()) TIn(B.b1) (4) A: (X,1,[proc(B.b1)],()) B: (T,1,[],()) C: (W,1,[in(c1)],()) TIn(C.c1) (5) A: (W,1,[out(a1)],()) B: (T,3,[],()) C: (X,1,[proc(B.b2)],()) TOut(A.a1) (6) A: (X,1,[],()) B: (T,4,[],()) C: (X,1,[proc(B.b2)],()) TOut(B.b2) (7) A: (X,2,[],()) B: (W,0,[in(b1),out(b2)],()) C: (X,1,[],()) TExit(B) (8) A: (X,1,[proc(B.b1)],()) B: (T,2,[],()) C: (W,1,[in(c1)],()) TIn(C.c1) TIn(B.b1) (9) A: (W,1,[out(a1)],()) B: (T,4,[],()) C: (X,1,[proc(B.b2)],()) TOut(B.b2) TOut(A.a1) (10) A: (X,1,[],()) B: (W,0,[in(b1),out(b2)],()) C: (X,2,[],()) TExit(B) (11) A: (W,2,[in(a2)],()) B: (W,0,[in(b1),out(b2)],()) C: (X,1,[],()) TIn(A.a2) (12) A: (X,2,[],()) B: (T,3,[],()) C: (X,1,[proc(B.b2)],()) TInAP(C.c1, B.b2) (13) A: (X,2,[],()) B: (W,0,[in(b1),out(b2)],()) C: (W,1,[in(c1)],()) TExit(B) (14) A: (W,1,[out(a1)],()) B: (W,0,[in(b1),out(b2)],()) C: (X,2,[],()) TExit(B) (15) A: (X,1,[proc(B.b1)],()) B: (T,1,[],()) C: (X,2,[],()) TOutAP(A.a1, B.b1) (16) A: (X,1,[],()) B: (W,0,[in(b1),out(b2)],()) C: (W,2,[out(c2)],()) TOut(C.c2) (17) A: (W,2,[in(a2)],()) B: (T,3,[],()) C: (X,1,[proc(B.b2)],()) TInAP(C.c1, B.b2) TIn(A.a2) (18) A: (X,2,[],()) B: (T,4,[],()) C: (X,1,[proc(B.b2)],()) TOut(B.b2) STInAP(C.c1, B.b2) (19) A: (W,2,[in(a2)],()) B: (W,0,[in(b1),out(b2)],()) C: (W,1,[in(c1)],()) TIn(A.a2) STOutAP(A.a1, B.b1) (20) A: (W,1,[out(a1)],()) B: (W,0,[in(b1),out(b2)],()) C: (W,2,[out(c2)],()) TOut(C.c2) (21) A: (X,1,[proc(B.b1)],()) B: (T,2,[],()) C: (X,2,[],()) TIn(B.b1) (22) A: (X,1,[proc(B.b1)],()) B: (T,1,[],()) C: (W,2,[out(c2)],()) TOut(C.c2) TOutAP(A.a1, B.b1) (23) A: (W,2,[in(a2)],()) B: (T,4,[],()) C: (X,1,[proc(B.b2)],()) TOut(B.b2) TIn(A.a2) (24) A: (X,2,[],()) B: (W,0,[in(b1),out(b2)],()) C: (X,2,[],()) TExit(B) STInAP(C.c1, B.b2) STOutAP(A.a1, B.b1) TExit(B) (25) A: (X,1,[proc(B.b1)],()) B: (T,2,[],()) C: (W,2,[out(c2)],()) TOut(C.c2) TIn(B.b1) (26) A: (W,2,[in(a2)],()) B: (W,0,[in(b1),out(b2)],()) C: (X,2,[],()) TExit(B) TIn(A.a2) (27) A: (X,2,[],()) B: (W,0,[in(b1),out(b2)],()) C: (W,2,[out(c2)],()) TOut(C.c2) TExit(B) (28) A: (F,0,[],()) B: (W,0,[in(b1),out(b2)],()) C: (F,0,[],())
TOutF(C.c2, A.a2) TInF(A.a2, C.c2)
Rysunek 2.4: Graf LTS dla nieczasowej wersji modelu z Rys. 2.2.
Definicja 2.4.3. Etykietowany system przej´s´c (LTS) jest krotk ˛a:
LTS = (S, A, →, S0), (2.3)
2.4. Reprezentacja przestrzeni stanów 17
gdzie S jest zbiorem stanów, A jest zbiorem akcji, →⊆ S × A × S jest relacj ˛a przej´s´c i S0 jest stanem
pocz ˛atkowym.
Dla modelu Alvis, graf LTS jest czwórk ˛a:
LTS = (R(S0), T , →, S0), (2.4)
gdzieR(S0) jest zbiorem stanów osi ˛agalnych ze stanu pocz ˛atkowego, T jest zbiorem mo˙zliwych tranzycji
dla danego modelu,→= {(S, t, S′)∶ S −t → S′∧S, S′∈ R(S
0)}, gdzie t ∈ T , i S0jest stanem pocz ˛atkowym.
W nieczasowych modelach Alvis łuki s ˛a etykietowane nazwami poszczególnych tranzycji wykonywanych przez agenta. Graf LTS dla nieczasowego modelu 2.2 został przedstawiony na rysunku 2.4.
W modelach czasowych wiele tranzycji mo˙ze by´c wykonywanych równolegle. Z tego powodu, łuki grafów LTS s ˛a etykietowane parami. Pierwszym elementem takiej pary jest lista tranzycji wykonywanych równolegle, a drugim elementem jest upływ czasu powi ˛azany z przej´sciem pomi˛edzy dwoma nast˛epuj ˛acymi po sobie stanami.
Na rysunku 2.5 został przedstawiony graf LTS dla czasowej wersji rozwa˙zanego modelu. Domy´slnie czasy wykonania ka˙zdej instrukcji ustawione s ˛a na jedn ˛a jednostk˛e czasu. W przypadku rozwa˙zanego mo-delu czasy wykonania zostały ustawione jak przedstawiono w tabeli 2.1.
Tablica 2.1: Zdefiniowane warto´sci czasu dla modelu z rysunku 2.2 Agent Instrukcja Jednostki czasu
A out 3 A in 2 B out 3 B in 2 B exit 1 C out 3 C in 2
Warto zwróci´c uwag˛e na to, co dzieje si˛e mi˛edzy stanem S0, a S1. Wykonywane s ˛a równocze´snie
tran-zycjeTIn C.c1oraz TOutAP A.a1 B.b1. TranzycjaTIn C.c1zostanie zako´nczona po 2 jednostkach czasu, ale tranzycja TOutAP A.a1 B.b1 b˛edzie jeszcze realizowana przez kolejn ˛a 1 jednostk˛e czasu. Gdyby agent C nie czekał na finalizacj˛e komunikacji, to mógłby w tym czasie zacz ˛a´c wykonywa´c ko-lejn ˛a instrukcj˛e. Tak wi˛ec, poniewa˙z czasy realizacji dla tych instrukcji s ˛a ró˙zne, to nie mo˙zna poda´c stanu modelu po ich zako´nczeniu w sposób analogiczny do stanów w modelu nieczasowym. Aby rozwi ˛aza´c ten problem został wprowadzony mechanizm tzw. migawek (ang. snapshots [106]). Migawki s ˛a stanami sys-temu w których cz˛e´s´c kroków jest wci ˛a˙z w trakcie wykonania. Przyj˛ete zostało, ˙ze s ˛a one tworzone z tak ˛a
2.4. Reprezentacja przestrzeni stanów 18 (0) A: (X,1,[],()) B: (W,0,[in(b1),out(b2)],()) C: (X,1,[],()) (1) A: (X,1,[sft(1)],()) B: (W,0,[in(b1),out(b2),lock(A)],()) C: (W,1,[in(c1)],()) {TIn(C.c1),TOutAP(A.a1, B.b1)}/2 (2) A: (X,1,[sft(1)],()) B: (T,3,[],()) C: (X,1,[proc(B.b2)],()) {TOut(A.a1),TInAP(C.c1, B.b2)}/2 (3) A: (X,1,[proc(B.b1)],()) B: (T,1,[],()) C: (W,1,[in(c1)],()) {TOutAP(A.a1, B.b1)}/1 (4) A: (W,1,[out(a1)],()) B: (T,3,[sft(2)],()) C: (X,1,[proc(B.b2)],()) {TOut(A.a1),TOut(B.b2)}/1 (5) A: (X,1,[proc(B.b1)],()) B: (T,2,[],()) C: (W,1,[in(c1)],()) {TIn(B.b1)}/2 (6) A: (W,1,[out(a1)],()) B: (T,4,[],()) C: (X,1,[proc(B.b2)],()) {TOut(B.b2)}/2 (7) A: (X,2,[],()) B: (W,0,[in(b1),out(b2)],()) C: (W,1,[in(c1)],()) {TExit(B)}/1 (8) A: (W,1,[out(a1)],()) B: (W,0,[in(b1),out(b2)],()) C: (X,2,[],()) {TExit(B)}/1 (9) A: (X,2,[sft(2)],()) B: (T,3,[],()) C: (X,1,[proc(B.b2)],()) {TIn(A.a2),STInAP(C.c1, B.b2)}/0 (10) A: (X,1,[proc(B.b1)],()) B: (T,1,[],()) C: (X,2,[sft(3)],()) {STOutAP(A.a1, B.b1),TOut(C.c2)}/0 (11) A: (W,2,[in(a2)],()) B: (T,3,[sft(1)],()) C: (X,1,[proc(B.b2)],()) {TIn(A.a2),TOut(B.b2)}/2 (12) A: (X,1,[proc(B.b1)],()) B: (T,2,[],()) C: (X,2,[sft(1)],()) {TIn(B.b1),TOut(C.c2)}/2 (13) A: (W,2,[in(a2)],()) B: (T,4,[],()) C: (X,1,[proc(B.b2)],()) {TOut(B.b2)}/1 (14) A: (X,2,[],()) B: (W,0,[in(b1),out(b2)],()) C: (W,2,[out(c2)],()) {TExit(B),TOut(C.c2)}/1 (15) A: (W,2,[in(a2)],()) B: (W,0,[in(b1),out(b2)],()) C: (X,2,[],()) {TExit(B)}/1 (16) A: (F,0,[],()) B: (W,0,[in(b1),out(b2)],()) C: (F,0,[],()) {TInF(A.a2, C.c2)}/2 {TOutF(C.c2, A.a2)}/3
Rysunek 2.5: Graf LTS dla czasowej wersji modelu z Rys. 2.2.
cz˛estotliwo´sci ˛a, aby w˛ezły w grafie LTS reprezentowały wszystkie zmiany stanu zachodz ˛ace w modelu. Na listach kontekstowych agentów mog ˛a wyst˛epowa´c wpisy sft(n) (ang. step finish time) oznaczaj ˛ace liczb˛e jednostek czasu do zako´nczenia bie˙z ˛acej tranzycji. Wpis taki mo˙zna wi˛ec zobaczy´c w stanie S1 w którym
tranzycjaTOutAP A.a1 B.b1potrzebuje jeszcze 1 jednostki czasu do zako´nczenia realizacji (co nast˛epuje w stanie S3).
2.5. ´Srodowisko Alvis 19
2.5 ´Srodowisko Alvis
2.5.1 Narz˛edzia modelowania
Modele w j˛ezyku Alvis s ˛a projektowane przy wykorzystaniu oprogramowania Alvis toolkit, w którego skład wchodz ˛a Alvis Editor i Alvis Compiler. Alvis Editor jest wizualnym ´srodowiskiem modelowania systemów w j˛ezyku Alvis. Edytor wyposa˙zono w narz˛edzie do graficznego projektowania diagramów komunikacji oraz edytor kodu ´zródłowego z pod´swietlaniem składni. Alvis Compiler [120] dokonuje translacji zapro-jektowanego modelu na program w j˛ezyku Haskell. W zale˙zno´sci od u˙zytych opcji kompilatora uzyskany program pozwala na generacj˛e grafu LTS i jego eksport do wybranego formatu lub na symulacj˛e kompilo-wanego modelu.
Proces modelowania i weryfikacji przy wykorzystaniu j˛ezyka Alvis został przedstawiony na Rys. 2.6. Proces rozpoczyna si˛e od stworzenia modelu w programie Alvis Editor. Kompletny model jest zapisywany do jednego pliku w formacie XML. W kolejnym etapie stosowany jest kompilator Alvis Compiler, który przetwarza model w Alvisie na plik wykonywalny w j˛ezyku Haskell. Proces kompilacji stanowi punkt wyj-´scia do weryfikacji zaprojektowanego modelu.
2.5.2 Narz˛edzia weryfikacji
Wygenerowany kod w j˛ezyku Haskell mo˙zna wyedytowa´c w celu dodania własnych algorytmów weryfi-kacji, algorytmów zarz ˛adzania priorytetami czy te˙z własnej funkcji duration, odpowiadaj ˛acej za okre´slenie czasu trwania ka˙zdej instrukcji modelu. W zale˙zno´sci od wybranych parametrów kompilatora i wprowa-dzonych modyfikacji, wykonanie kodu wynikowego powoduje wygenerowanie grafu LTS [112]), logów symulacji lub wyników zdefiniowanych przez u˙zytkownika procedur. Wyniki zapisywane s ˛a w odpowied-nich formatach danych – obecnie s ˛a to formaty DOT, Aldebaran i CSV. Pierwszy z odpowied-nich pozwala m.in. na wygenerowanie graficznej reprezentacji grafu LTS np. z wykorzystaniem programu xdot. Pozwala on w wy-godny sposób „w˛edrowa´c” po grafie i „manualnie” analizowa´c wybrane fragmenty grafu. Format Aldebaran pozwala na bezpo´srednie wczytanie grafu LTS do pakietu CADP. Format CSV stosowany jest do weryfi-kacji modelu z u˙zyciem metod statystycznych lub metod eksploracji danych. Mog ˛a by´c tutaj wykorzystane np. ´srodowiska bazuj ˛ace na j˛ezyku R lub Python.
Wracaj ˛ac to kwestii wykorzystania technik weryfikacji modelowej, mo˙zliwa jest automatyczna ana-liza grafu LTS pod k ˛atem spełnialno´sci formuł zapisanych w logice temporalnej. Proces weryfikacji przed rozpocz˛eciem opisywanych w tej rozprawie prac pozwalał jedynie na weryfikacj˛e opart ˛ana akcjach (nie sta-nach) przy wykorzystaniu rachunku µ (ang. µ-calculus) [44] w narz˛edziu CADP toolbox [48], [49]. Jednym z etapów prac było przygotowanie translacji grafu LTS do j˛ezyka SMV, pozwalaj ˛acego na wykorzystanie narz˛edzia nuXmv do weryfikacji formuł wyra˙zonych w logikach LTL i CTL. Szerszy opis tego podej´scia
2.6. Powi ˛azane formalizmy 20
Alvis Editor
diagram komunikacji + warstwa kodu
Alvis Compiler
Alvis → Posta´c po´srednia w Haskell
Dowolny edytor tekstu doł ˛aczenie własnego kodu Haskell
Kompilator GHC plik XML plik Haskell plik Haskell plik Haskell (0) A: (X,1,[],()) B: (X,1,[],()) (1) A: (X,2,[],()) B: (X,1,[],()) loop(A) (2) A: (X,1,[],()) B: (X,2,[],()) loop(B) (3) A: (W,2,[out(a)],()) B: (X,1,[],()) out(A.a) (4) A: (X,2,[],()) B: (X,2,[],()) loop(B) loop(A) (5) A: (X,1,[],()) B: (W,2,[in(b)],()) in(B.b) (6) A: (W,2,[out(a)],()) B: (X,2,[],()) loop(B) out(A.a) (7) A: (X,2,[],()) B: (W,2,[in(b)],()) in(B.b) loop(A) in(B.b) out(A.a) plik DOT 0 1 loop(A) 2 loop(B) 3 out(A.a) 4 loop(B) loop(A) 5 in(B.b) 6 loop(B)out(A.a) 7 in(B.b) loop(A) in(B.b) out(A.a) plik Aldebaran 0; A; X; 1; []; (); B; X; 1; ... 1; A; X; 2; []; (); B; X; 1; ... 2; A; X; 1; []; (); B; X; 2; ... 3; A; W; 2; [out(a)]; (); B; ... 4; A; X; 2; []; (); B; X; 2; ... 5; A; X; 1; []; (); B; W; 2; ... 6; A; W; 2; [out(a)]; (); B; ... 7; A; X; 2; []; (); B; W; 2; ... plik TXT
?
własny nuXmv CADP R, Pythonwykonanie pliku binarnego (mo˙zliwe wyniki)
Rysunek 2.6: Proces modelowania i weryfikacji przy wykorzystaniu j˛ezyka Alvis. znajduje si˛e w rozdziale 5.
Wi˛ecej informacji na temat narz˛edzi wspieraj ˛acych wykorzystanie j˛ezyka Alvis jest dost˛epnych w in-strukcji znajduj ˛acej si˛e na stronie projektu [113].
2.6 Powi ˛azane formalizmy
W niniejszym podrozdziale zawarto opis wybranych popularnych formalnych j˛ezyków modelowania, które mog ˛aby´c u˙zywane podobnie jak Alvis do modelowania i weryfikacji dyskretnych systemów współbie˙znych czasowych i/lub nieczasowych.
2.6. Powi ˛azane formalizmy 21
2.6.1 Sieci Petriego
Sieci Petriego s ˛a niew ˛atpliwie najbardziej popularn ˛a grup ˛a formalnych j˛ezyków modelowania. Słu˙z ˛a do formalnego, graficznego opisu i analizy systemów współbie˙znych. Od ich wprowadzenia w latach 60. przez Carla A. Petriego [95] zostało zaproponowanych przynajmniej kilkadziesi ˛at wariantów (klas) sieci b˛ed ˛acych rozwini˛eciem oryginalnej koncepcji, dzi˛eki czemu u˙zytkownik ma mo˙zliwo´s´c dobrania odpowiedniej klasy do modelowanego problemu. Podstawow ˛aró˙znic ˛apomi˛edzy sieciami Petriego, a j˛ezykiem Alvis jest wysoki próg wej´scia w ten formalizm. Stworzenie nawet prostego modelu wymaga od u˙zytkownika długotrwałego treningu. Dodatkowo, dla skomplikowanych systemów sieci Petriego s ˛a bardzo szybko si˛e rozrastaj ˛a, sta-j ˛ac si˛e ci˛e˙zkimi do zrozumienia nawet dla do´swiadczonych in˙zynierów. Nasta-jprawdopodobniesta-j nasta-jbli˙zsz ˛a Alvisowi klas ˛a s ˛a kolorowane czasowe sieci Petriego (Timed coloured Petri nets [68]). Pozwalaj ˛a one na modelowanie zdarze´n dyskretnych ł ˛acz ˛ac mo˙zliwo´sci sieci Petriego z wysokopoziomowym j˛ezykiem pro-gramowania (SML), który umo˙zliwia mi˛edzy innymi definiowanie typów danych, zmiennych, czy wyra˙ze´n do manipulacji danymi [91]. Model czasowy w tej klasie sieci Petriego opiera si˛e na znacznikach czasu, które mog ˛a zosta´c przypisane do tokenów (znaczników), czyli warto´sci przechowywanych w miejscach sieci, podczas odpalania przej´s´c. Poniewa˙z warto´sci znaczników czasowych mog ˛a rosn ˛a´c w niesko´nczo-no´s´c, grafy osi ˛agalno´sci dla tych sieci s ˛a zwykle niesko´nczone. Z tego powodu mo˙zliwo´sci wykorzystania technik weryfikacji modelowej dla modeli stworzonych w kolorowanych czasowych sieciach Petriego s ˛a ograniczone lub wymagaj ˛a generowania alternatywnych sko´nczonych reprezentacji grafów osi ˛agalno´sci np. przez zastosowanie klas równowa˙zno´sci dla stanów i tranzycji. W j˛ezyku Alvis ka˙zde przej´scie mo˙ze mie´c indywidualnie przypisany czas trwania. Poniewa˙z warto´sci nie s ˛a zwi ˛azane z globalnym zegarem, grafy LTS s ˛a zwykle sko´nczone. Kolejn ˛a istotn ˛a ró˙znic ˛a jest to, ˙ze w przypadku sieci kolorowanych reprezentacja graficzna modelu rzadko odzwierciedla struktur˛e modelowanego systemu, utrudniaj ˛ac zarówno proces two-rzenia jak i interpretacji. Diagramy komunikacji w Alvisie znacznie lepiej odzwierciedlaj ˛a rzeczywisto´s´c, poniewa˙z ka˙zdy agent reprezentuje konkretny komponent systemu. Ostatni ˛a wart ˛a wspomnienia ró˙znic ˛a s ˛a mo˙zliwo´sci definiowania własnych typów danych i funkcji manipulacji danymi – Alvis umo˙zliwia to dzi˛eki wykorzystaniu systemu typów Haskella. W przypadku sieci kolorowanych i j˛ezyka SML, dost˛epny jest jedynie ograniczony zbiór typów podstawowych i powi ˛azanych operatorów.
2.6.2 Algebry procesów
Algebry procesów s ˛a drug ˛a popularn ˛a grup ˛a metod formalnych. W ich przypadku opis zachowania systemu wzorowany jest na rachunku algebraicznym – przedstawiaj ˛a zewn˛etrzne zachowania systemu jako ci ˛ag wy-ra˙ze´n algebraicznych. Najbardziej znanymi algebrami procesów s ˛a CCS (Calculus of Communicating Sys-tems, [90], [2]), CSP (Communicating Sequential Processes, [59], [12]) oraz LOTOS [67]. W przypadku algebr procesów proces modelowania opiera si˛e na tworzeniu skryptów opisuj ˛acych dany system. Skrypty
2.6. Powi ˛azane formalizmy 22
mog ˛a mie´c posta´c ci ˛agu równa´n algebraicznych (CCS, CSP) lub kodu (LOTOS). W przypadku CCS i CSP rozwa˙zana jest synchroniczna komunikacja mi˛edzy procesami – procesy wykonuj ˛ace te same akcje s ˛a trak-towane jako komunikuj ˛ace si˛e ze sob ˛a. Podej´scie to, chocia˙z relatywnie proste, niesie ze sob ˛a spore ryzyko niezamierzonego skomunikowania ze sob ˛a ró˙znych cz˛e´sci systemu. Stanowi to bardzo powa˙zny problem, szczególnie w zło˙zonych modelach. W j˛ezyku LOTOS procesy komunikuj ˛a si˛e ze sob ˛a wył ˛acznie synchro-nicznie poprzez tzw. bramy. Stany obiektów definiowane s ˛anatomiast przez abstrakcyjne typy danych. Cho-cia˙z zastosowana notacja przypomina j˛ezyki wysokiego poziomu to bazuje na koncepcjach zapo˙zyczonych z algebr CCS i CSP. Pomimo prób dodania do tego j˛ezyka kompozycji asynchronicznej [82], proces mo-delowania jest ci˛e˙zki do zrozumienia, co skutecznie zniech˛eca in˙zynierów i wstrzymuje jego popularyzacj˛e w in˙zynierii oprogramowania.
Warto wspomnie´c, ˙ze geneza j˛ezyka Alvis jest powi ˛azana z algebrami procesów. J˛ezyk XCCS [7], b˛e-d ˛acy rozszerzeniem algebry CCS o graficzny mob˛e-del poł ˛acze´n mi˛eb˛e-dzy agentami, jest niejako poprzeb˛e-dnikiem Alvisa. Sam Alvis posiada kilka zapo˙zycze´n z algebr procesów, jak cho´cby terminy takie ja agent, port czy kanał komunikacyjny. W przypadku Alvisa jednak wykorzystanie równa´n algebraicznych zostało całkowicie porzucone na rzecz warstwy kodu w j˛ezyku wysokiego poziomu.
2.6.3 Automaty czasowe
Automaty czasowe [11], [4] s ˛a rozszerzeniem automatów sko´nczonych [64] o zmienne zegarowe pozwala-j ˛ace wyrazi´c zale˙zno´sci czasowe w modelu. Zmienne te reprezentupozwala-j ˛a zegary w modelowanym systemie. Ze-gary te s ˛a zerowane podczas startu systemu, a nast˛epnie ich warto´sci synchronicznie wzrastaj ˛a. Dodatkowo, mo˙zna dokona´c niezale˙znego zerowania zegarów i mierzy´c czas jaki upłyn ˛ał od ostatniego wyzerowania. Zegary u˙zywane s ˛ado definiowania warunków czasowych, w których dany system mo˙ze operowa´c, w szcze-gólno´sci do definicji dost˛epnych przej´s´c oraz długo´sci pobytu modelu w danym stanie. W przeciwie´nstwie do j˛ezyka Alvis, nie jest mo˙zliwe zdefiniowanie czasu trwania pojedynczego przej´scia.
Automaty czasowe wykorzystuj ˛a graficzn ˛a reprezentacj˛e systemu oraz umo˙zliwiaj ˛a modularyzacj˛e delu poprzez wprowadzenie hierarchii, jednak opis modelu jest bardzo sformalizowany, a weryfikacja mo-delu wymaga zaawansowanych umiej˛etno´sci matematycznych.
2.6.4 Statechart
Wizualny j˛ezyk modelowania Statechart [56] jest pod wieloma wzgl˛edami podobny do Alvisa. Rozszerza on koncepcj˛e maszyny stanów o trzy kluczowe aspekty: hierarchi˛e, równoległo´s´c i komunikacj˛e. Specyfikacja systemu mo˙ze dzi˛eki temu zosta´c zmodularyzowana. Chocia˙z oryginalna koncepcja nie posiadała modelu czasu, z biegiem lat powstały formalizmy wprowadzaj ˛ace czasowo´s´c. Nale˙z ˛a do nich mi˛edzy innymi Timed Statecharts [69], Real-time Statecharts [50] oraz dwie koncepcje opisane przez twórc˛e j˛ezyka Statechart
2.6. Powi ˛azane formalizmy 23
w jego pó´zniejszej pracy [57].
Najwi˛eksz ˛a przewag ˛a Alvisa nad grup ˛a formalizmów bazuj ˛acych na Statechart jest oddzielenie kodu od warstwy wizualnej, znacznie bardziej zwi˛ezła reprezentacja graficzna oraz mo˙zliwo´s´c dodania dowolnego kodu (dozwolonego w j˛ezyku Haskell) do modelu. Chocia˙z Statechart umo˙zliwia chowanie stanów systemu w kolejnych warstwach, to ostatecznie wszystkie stany systemu musz ˛a znale´z´c swoj ˛a reprezentacj˛e w mo-delu. Warstwa wizualna w j˛ezyku Alvis modeluje jedynie komunikacj˛e, dzi˛eki czemu jest znacznie mniejsza i łatwiejsza do zrozumienia w przypadku modeli rzeczywistych systemów, zawieraj ˛acych miliony stanów. Oddzielenie warstwy kodu pozwala z kolei na reu˙zywalno´s´c (ten sam kod dla wielu agentów) oraz ułatwia zrozumienie modelu przeci˛etnemu programi´scie.
2.6.5 PRISM
PRISM [74] jest probabilistycznym narz˛edziem do formalnego modelowania i analizy modeli stycznych, w tym czasowych ła´ncuchów Markova, procesów decyzyjnych Markova, automatów probabili-stycznych oraz czasowych automatów probabiliprobabili-stycznych [92]. PRISM rozszerza koncepcj˛e maszyny sta-nów o przej´scia probabilistyczne, zmienne zegarowe oraz modularyzacj˛e. Posiada on własny j˛ezyk opisu modelu. Niew ˛atpliw ˛a przewag ˛a PRISM nad Alvisem jest to, ˙ze j˛ezyk ten nie ma problemu z opisywaniem niepewno´sci. W Alvisie istnieje jedynie kilka instrukcji umo˙zliwiaj ˛acych wprowadzenie losowo´sci (instruk-cja pick i komunika(instruk-cja nieblokuj ˛aca). Jednak w przeciwie´nstwie do Alvisa, opis modelu PRISM umo˙zliwia definiowanie zmiennych jedynie kilku typów (boolean i integer z ograniczonym zakresem) oraz wykorzysta-nie wykorzysta-niewielkiej liczby wbudowanych operacji. Innym znanym problemem PRISM jest spore ryzyko popeł-nienia ci˛e˙zkich do znalezienia bł˛edów. Ryzyko to jest zwi ˛azane z tym, ˙ze komunikacja pomi˛edzy modułami mo˙ze by´c zaciemniona przez jawne wywołania zmiennych z innych modułów. Modelowanie w PRISM wy-maga my´slenia na ni˙zszym poziomie abstrakcji – w kategoriach stanów i upływu czasu. U˙zytkownik Alvisa mo˙ze operowa´c na wy˙zszym poziomie, bli˙zszym rzeczywistej implementacji systemu, a przestrze´n stanów jest generowana automatycznie (graf LTS).
Rozdział 3
Intermediate Haskell Representation
Jak zostało przedstawione w rozdziale 2, głównym zadaniem narz˛edzia Alvis Compiler jest translacja mo-delu Alvis do postaci po´sredniej w j˛ezyku funkcyjnym Haskell. Ta po´srednia reprezentacja modeli nazwana została IHR (ang. Intermediate Haskell Representation) [112]. Rozdział ten został po´swi˛econy szerszemu przedstawieniu koncepcji stoj ˛acych za powstaniem postaci po´sredniej oraz opisaniu sposobu reprezentacji stanów i dynamiki modelu w j˛ezyku Haskell.
3.1 Paradygmat funkcyjny
Paradygmatem programowania nazywany jest styl okre´slaj ˛acy podstawowe mechanizmy tworzenia progra-mów w danym j˛ezyku. Najpopularniejsze obecnie j˛ezyki programowania, takiej jak Python, Java, Swift czy C++ s ˛a j˛ezykami przede wszystkim imperatywnymi (ang. imperative) oraz dodatkowo obiektowymi. J˛ezyki imperatywne składaj ˛a si˛e z sekwencji instrukcji do wykonania, gdzie programista jawnie definiuje krok po kroku sposób realizacji zadania. Wykorzystuje przy tym zmienne, charakteryzuj ˛ace si˛e tym, ˙ze posiadaj ˛a swój stan, który ulega zmianie w czasie działania programu.
Najpopularniejsz ˛a alternatyw ˛a dla paradygmatu imperatywnego jest paradygmat funkcyjny (ang. func-tional). Jego istot ˛ajest to, ˙ze wykonanie programu traktowane jest jako ewaluacje wyra˙ze´n matematycznych, a nie sekwencji instrukcji jak w przypadku stylu imperatywnego. W j˛ezykach funkcyjnych program two-rzony jest poprzez implementacj˛e coraz bardziej skomplikowanych funkcji matematycznych oraz stałych, a˙z do osi ˛agni˛ecia celu. Odpowiednikiem operacji jest obliczanie wyra˙ze´n, zamiast przypisa´n s ˛a definicje funkcji, a rekurencja zast˛epuje p˛etle.
Z paradygmatem funkcyjnym zwi ˛azane jest poj˛ecie czysto´sci funkcji. Funkcje czyste (ang. pure) cha-rakteryzuj ˛a si˛e tym, ˙ze nie posiadaj ˛a tzw. efektów ubocznych. Efekty uboczne to wszystkie operacje wy-konywane podczas działania funkcji, które nie maj ˛a zwi ˛azku z warto´sci ˛a zwracan ˛a przez funkcj˛e (np. mo-dyfikacja zmiennych, operacje wej´scia/wyj´scia). Istnieje zbiór j˛ezyków funkcyjnych, w tym j˛ezyk Haskell,
