CADP

CADP (ang. Construction and Analysis of Distributed Processes) [49] jest obszernym pakietem oprogra-mowania rozwijanym obecnie przez zespół projektowy CONVECS, którego członkowie nale˙z ˛a do insty-tutu Inria Grenoble - Rhône-Alpes oraz laboratorium LIG. Oferuje on zestaw narz˛edzi do projektowania asynchronicznych systemów współbie˙znych, takich jak protokoły komunikacyjne, systemy rozproszone, ar-chitektury wieloprocesorowe czy usługi webowe. Swoje pocz ˛atki ma w drugiej połowie lat 80-tych, kiedy to stworzone zostały 2 pierwsze narz˛edzia CAESAR i ALDEBARAN. Pierwsze z nich jest kompilatorem i generatorem przestrzeni stanów dla j˛ezyka LOTOS, natomiast drugie pozwalało na minimalizacj˛e oraz porównywanie etykietowanych systemów przej´s´c (LTS) wzgl˛edem relacji równowa˙zno´sci. Od tamtej pory pakiet był jednak stale ulepszany i rozszerzany o kolejne narz˛edzia. Obecnie pakiet składa si˛e z 42 narz˛edzi, 17 mo˙zliwych do wykorzystania komponentów oraz posiada ponad 100 uznanych integracji z zewn˛etrznymi

4.5. Narz˛edzia 51

narz˛edziami badawczymi [37][103]. Oferowane funkcjonalno´sci pokrywaj ˛a pełen cykl projektowania sys-temów asynchronicznych – specyfikacj˛e, symulacj˛e, prototypowanie, weryfikacj˛e, testowanie i sprawdzanie wydajno´sci. Aby poradzi´c sobie z rozbudowanymi systemami, CADP oferuje implementacj˛e wielu tech-nik weryfikacji, w tym analiz˛e osi ˛agalno´sci, weryfikacj˛e w locie, weryfikacj˛e kompozycyjn ˛a, weryfikacj˛e rozproszon ˛a i analiz˛e statyczn ˛a. Dodatkowo wspera wiele j˛ezyków specyfikacji.

CADP w odró˙znieniu od innych explicit model checkerów (np. SPIN) polega na weryfikacji opartej na akcjach (ang. action-based verification), a nie na stanach (ang. state-based verification. Weryfikacja ta polega na modelu semantycznym przyj˛etym z teorii współbie˙zno´sci, gdzie mo˙zna odwoływa´c si˛e jedynie do obserwowalnych akcji komunikacji zachodz ˛acych w systemie, a nie do zawarto´sci stanów. Takie podej´scie znacz ˛aco zwi˛eksza mo˙zliwo´sci rozmiary mo˙zliwych do weryfikacji systemów – pomimo wykorzystania jawnej przestrzeni stanów jest w stanie dokonywa´c weryfikacji systemów posiadaj ˛acych nawet 1010stanów. Jednak uniemo˙zliwiaj ˛acałkowicie wykorzystanie informacje zawartych w stanach, znacz ˛aco utrudnione jest zadanie specyfikacji własno´sci systemu, a same formuły s ˛a cz˛esto du˙zo mniej intuicyjne.

Pakiet CADP wspiera obecnie kilka j˛ezyków specyfikacji modeli, w tym w szczególno´sci:

• LOTOS (ang. Language Of Temporal Ordering Specification) [67] – formalny j˛ezyk specyfikacji ustandaryzowany przez ISO do specyfikacji protokołów komunikacyjnych. Składa si˛e w zasadzie z dwóch j˛ezyków. Pierwszy z nich słu˙zy do specyfikacji danych i jest oparty na algebraicznych, abstrakcyjnych typach danych. Drugi dotyczy sterowania i jest algebr ˛a procesów czerpi ˛aca z algebr CCS [90], CSP [59] czy CIRCAL [89].

• FSP (ang. Finite State Process) [81] – zwi˛ezła notacja algebraiczna dla procesów współbie˙znych, wspierana przez narz˛edzie LTSA.

• EXP [78] – j˛ezyk opisu sieci komunikuj ˛acych si˛e grafów LTS, reprezentowany przez zestaw plików BCG (ang. Binary Coded Graphs.

• LOTOS NT [25]. – jest j˛ezykiem próbuj ˛acym poł ˛aczy´c najistotniejsze cechy algebr procesów (m.in. współbie˙zno´s´c czy abstrakcj˛e) z popularnymi j˛ezykami programowania imperatywnego i funkcyj-nego. W odró˙znieniu od LOTOS, który ł ˛aczy w sobie 2 j˛ezyki, LOTOS NT jest jednolity, a cz˛e´s´c dotycz ˛aca danych mo˙ze by´c postrzegana jako podzbiór cz˛e´sci dotycz ˛acej sterowania. Dzi˛eki temu, j˛ezyk ten jest prostszy do nauki i wykorzystania.

W pakiecie istniej ˛a obecnie dwa typy narz˛edzi do model checkingu:

• XTL (ang. eXecutable Temporal Language) [47] – j˛ezyk funkcyjny słu˙z ˛acy do eksploracji i odpyty-wania jawnych etykietowanych systemów przej´s´c zakodowanych w formacie BCG. Operatory logiki temporalnej mog ˛a by´c w nim wymieszane z niestandardowymi własno´sciami, np. zliczaniem stanów czy tranzycji, a w wi˛ekszej ogólno´sci z dowolnymi obliczeniami opisanymi przez rekursywne funkcje eksploruj ˛ace LTS.

4.5. Narz˛edzia 52

• Evaluator – rodzina model checkerów umo˙zliwiaj ˛acych weryfikacj˛e w locie formuł w regularnym wolnym od przepływów rachunku µ dla etykietowanych systemów przej´s´c. Obecnie w u˙zyciu s ˛a trzy wersje model checkera: Evaluator3 [85][48], Evaluator4 [49] dodaj ˛acy mo˙zliwo´s´c wykorzysta-nia w formułach etykiet przej´s´c w których zakodowane s ˛a informacje o nazwach bram czy zmiewykorzysta-nia- zmienia-j ˛acych si˛e warto´sciach zmiennych oraz operatory sprawiedliwo´sci) i Evaluator5 [84] dodazmienia-j ˛acy proba-bilistyczny operator okre´slaj ˛acy prawdopodobie´nstwo sekwencji przej´s´c interpretowany na probabi-listycznych systemach przej´s´c (ang. Probabilistic Transition System – PTS) [73].

4.5.4 PRISM

PRISM [58], jak przedstawiono wst˛epnie w sekcji 2.6.5, jest probabilistycznym model checkerem, słu˙z ˛acym do formalnego modelowania i analizy systemów wykazuj ˛acych zachowania losowe lub probabilistyczne. Twórcami narz˛edzia s ˛a Dava Parker (University of Birmingham) , Gethin Norman (University of Glasgow) i Marta Kwiatkowska (University of Oxford). Pierwsza wersja narz˛edzia opublikowana została w 2001 roku i regularnie wydawane s ˛a jego nowe wersje [42]. Oprogramowanie zyskało spor ˛a popularno´s´c, zarówno w ´srodowisku naukowym, jak i komercyjnym, i jest wykorzystywane w wielu dziedzinach, w tym mi˛edzy innymi protokołach komunikacji [43], biologii [40] czy teorii gier [26].

PRISM akceptuje modele probabilistyczne opisane w dedykowanym, wysokopoziomowym j˛ezyku mo-delowania opartym na stanach [72]. Bezpo´srednio wspiera on trzy typy modeli: Ła´ncuchy Markowa z cza-sem dyskretnym (ang. discrete-time Markov chains – DTMC), procesy decyzyjne Markowa (ang. Markov decision processes – MDP) oraz ła´ncuchy Markowa z czasem ci ˛agłym (ang. continuous-time Markov cha-ins – CTMCs). Dodatkowo wspierane s ˛a równie˙z automaty probabilistyczne (ang. probabilistic automata – PA) i czasowe automaty probabilistyczne (ang. probabilistic timed automata – PTA). Własno´sci mog ˛a by´c specyfikowane za pomoc ˛a probabilistycznych logik temporalnych PCTL (dla DTMC i MDP) i CSL (dla CTMC) [74].

Implementacja PRISM wykorzystuje struktury danych oparte o binarne diagramy decyzyjne. Narz˛edzie najpierw tworzy wewn˛etrzn ˛a reprezentacj˛e modelu probabilistycznego, obliczaj ˛ac przestrze´n osi ˛agalnych stanów. Nast˛epnie sprawdzane s ˛awyspecyfikowane własno´sci przy u˙zyciu odpowiednich algorytmów wery-fikacji modelowej. Wynik werywery-fikacji mo˙ze by´c jako´sciowy (sprawdzenie spełnienia formuły) lub ilo´sciowy (prawdopodobie´nstwo zaj´scia danego zdarzenia). PRISM umo˙zliwia równie˙z tworzenie tzw. eksperymen-tów, w których wyniki s ˛a funkcjami modelu i parametrów własno´sci. Takie tabelaryczne wyniki mo˙zna wyeksportowa´c do arkusza kalkulacyjnego lub przegl ˛ada´c na wykresach [73].

4.5. Narz˛edzia 53