wszystkie tranzycje które s ˛a aktywne w stanie reprezentowanym przez dany w˛ezeł. Funkcja multiSteps odpowiada za podział listy aktywnych tranzycji (z mo˙zliwymi konfliktami) na podlisty zwane wielokrokami. Wielokrok jest list ˛a tranzycji takich, ˙ze ˙zaden z wielokroków nie zawiera konfliktów oraz ka˙zdy wielokrok zawiera maksymaln ˛a liczb˛e mo˙zliwych tranzycji.
Nast˛epnie wyznaczane s ˛a stany mo˙zliwe do osi ˛agni˛ecia poprzez wykonanie tranzycji z poprzedniego kroku. Dla czasowych modeli istotne s ˛a równie˙z funkcje timeShift oraz timeFire. Pierwsza z nich zwraca przesuni˛ecie czasu dla pierwszego stanu i pierwszego wielokroku. Druga natomiast zwraca list˛e nowych stanów wygenerowanych dla danego stanu i wielokroku.
Funkcja update aktualizuje listy nieprzeprocesowanych oraz pomocniczych w˛ezłów. Porównuje ona nowe stany z list ˛a ju˙z wyznaczonych stanów, aby sprawdzi´c czy wyst˛epowały ju˙z w przeszło´sci. Je˙zeli tak to dodawana jest tylko nowa kraw˛ed´z, a je´sli nie to dodawany jest do listy zarówno w˛ezeł jak i kraw˛ed´z.
Ostatnim elementem wygenerowanej reprezentacji IHR jest funkcja main. Domy´slnie generuje ona graf LTS i zapisuje do formatu DOT [46].
3.6 Dodatkowe opcje generacji
Tablica 3.1: Wybrane opcje narz˛edzia Alvis Compiler Opcja Opis
-ald wykorzystuje kod do generacji wyj´scia w formacie Aldebaran
-csv wykorzystuje kod do generacji wyj´scia w formacie CSV
-dot wykorzystuje kod do generacji wyj´scia w formacie DOT
-nt generuje nieczasow ˛a wersj˛e podanego modelu
-m wykorzystuje zdefiniowany przez u˙zytkownika kod funkcji main
-p1 wykorzystuje pierwszy ze zdefiniowanych algorytmów priorytetyzacji (p1)
-p2 wykorzystuje drugi ze zdefiniowanych algorytmów priorytetyzacji (p2)
-p wykorzystuje zdefiniowany przez u˙zytkownika algorytm priorytetyzacji
Oprócz opcji przeł ˛aczania pomi˛edzy czasow ˛a i nieczasow ˛a wersj ˛a modelu, kompilator j˛ezyka Alvis oferuje równie˙z inne przydatne argumenty wiersza polece´n. Ich przegl ˛ad został przedstawiony w tabeli 3.1. Przede wszystkim u˙zytkownik ma mo˙zliwo´s´c wybrania preferowanego formatu wyj´sciowego który zosta-nie wygenerowany przez program. Kompilator wspiera generacj˛e wyj´scia w formatach DOT (Graphviz), Aldebaran (CADP) oraz CSV.
U˙zytkownik mo˙ze równie˙z zdefiniowa´c własne priorytety dla ka˙zdego agenta. Domy´slnie priorytety s ˛a pomijane. Kompilator umo˙zliwia trzy opcje zarz ˛adzania priorytetami. Opcja -p1 i -p2 pozwala na
3.6. Dodatkowe opcje generacji 31
wanie jednego z predefiniowanych algorytmów. Priorytety s ˛awykorzystywane do redukcji niedeterminizmu w zachowaniu modelu poprzez rozwi ˛azywanie konfliktów pomi˛edzy tranzycjami komunikacji rywalizuj ˛a-cymi o dost˛ep do tego samego agenta. W przypadku algorytmu p1, priorytet tranzycji komunikacji jest równy priorytetowi agenta, który wykonuje tranzycj˛e. W przypadku drugiego podej´scia (algorytm p2), je-˙zeli tranzycja komunikacji pobiera 2 porty jako argumenty (tranzycja dotyczy dwóch agentów), to priorytet tranzycji jest sum ˛a priorytetów obu komunikuj ˛acych si˛e agentów. Alvis Compiler dostarcza równie trzeciej opcji (-p), która umo˙zliwia wykorzysta´c kod w j˛ezyku Haskell, zawieraj ˛acy własn ˛a implementacj˛e algo-rytmu zarz ˛adzania priorytetami. Metoda wł ˛aczania własnego algoalgo-rytmu zarz ˛adzania priorytetami została opisana w [104].
Domy´slna implementacja funkcji main jest wykorzystywana do generacji grafu LTS i jego eksportu do wybranego formatu. Opcja -m (-main) mo˙ze zosta´c u˙zyta do podania zdefiniowanego przez u˙zytkownika pliku z własn ˛a implementacj ˛a napisan ˛a w j˛ezyku Haskell i zamieniaj ˛ac ˛a standardowe zachowanie. Umo˙z-liwia to łatwe wprowadzenie nowego formatu wyj´sciowego lub logiki weryfikacji, jak równie˙z wykonanie dodatkowych operacji na generowanym grafie. Opcja -m mo˙ze zosta´c poł ˛aczona z innymi opcjami wyj´scio-wymi. Je˙zeli zostanie pomini˛eta, to domy´slnie wykorzystywana jest opcja -dot.
Standardowa instalacja narz˛edzia Alvis Compiler zawiera folder o nazwie compiler_files zawieraj ˛acy pliki IHR wraz z implementacjami wymienionych wy˙zej opcji zwi ˛azanych z formatami wyj´sciowymi i priorytetami. Jest on równie˙z domy´sln ˛a ´scie˙zk ˛a dla opcji, które umo˙zliwiaj ˛a ustawianie własnych plików. U˙zytkownik ma mo˙zliwo´s´c modyfikacji tych plików w celu dostosowania ich do własnych potrzeb.
Rozdział 4
Weryfikacja modelowa
Potwierdzenie niezawodno´sci systemów jest jednym z najwa˙zniejszych problemów w in˙zynierii oprogra-mowania. W bran˙zy informatycznej obowi ˛azuj ˛acym standardem stało si˛e testowanie wytwarzanego opro-gramowania za pomoc ˛a testów manualnych i automatycznych. Podej´scie to polega na weryfikacji istniej ˛a-cego kodu. W realiach rynkowych testowanie oprogramowania jest swojego rodzaju kompromisem pomi˛e-dzy wysok ˛a jako´sci ˛a produktu (bezbł˛edno´sci ˛a), a nakładem pracy wymaganej do utrzymania tej jako´sci. W wi˛ekszo´sci przypadków takie podej´scie jest wystarczaj ˛ace. S ˛a jednak zastosowania, w szczególno´sci w systemach krytycznych ze wzgl˛edu na bezpiecze´nstwo, w których potencjalne bł˛edy systemu s ˛a zbyt kosztowne, by zastosowa´c podej´scie oparte wył ˛acznie na analizie implementacji. W takiej sytuacji, cz˛esto stosowanym podej´sciem jest wykorzystanie analizy formalnych modeli tworzonych systemów. Przykładowo formalna weryfikacja specyfikacji pozwala na wykrycie bł˛edów projektowych jeszcze przed rozpocz˛eciem implementacji.
4.1 Weryfikacja modelowa
4.1.1 Idea
Weryfikacja modelowa (ang. model checking) jest obecnie najwa˙zniejsz ˛a grup ˛a metod automatycznej ana-lizy oprogramowania opartych na metodach formalnych. Technika ta została wprowadzona na pocz ˛atku lat 80. przez niezale˙zne prace E. Clarke’a i E. A. Emersona [35] oraz J. P. Queille’a i J. Sifakisa [98]. Jej my´sl ˛a przewodni ˛a jest przedstawienie modelu jako etykietowanego systemu przej´s´c (systemu tranzycyjnego), for-malnej specyfikacji jego własno´sci za pomoc ˛alogik temporalnych, a nast˛epnie automatycznym sprawdzeniu prawdziwo´sci tych własno´sci w narz˛edziach typu model checker [33], [119].
4.1. Weryfikacja modelowa 33
4.1.2 Proces weryfikacji
Weryfikacja modelowa jest inaczej procesem obliczania odpowiedzi na pytanie, czy dany model spełnia zdefiniowane formuły. Kroki mo˙zna opisa´c nast˛epuj ˛aco [65]:
• Stworzenie modeluM systemu u˙zywaj ˛ac j˛ezyka modelowania wspieranego przez dany model chec-ker.
• Wyspecyfikowanie wybranej własno´sci systemu w postaci formuły φ wykorzystuj ˛ac j˛ezyk specyfika-cji wspierany przez model checker.
• Uruchomienie model checkera z argumentami wej´sciowymiM oraz φ.
Narz˛edzie zwraca odpowied´z twierdz ˛ac ˛a, je˙zeli model spełnia formuł˛e (M ⊧ φ). W przeciwnym wypadku wi˛ekszo´s´c narz˛edzi generuje kontrprzykład udowadniaj ˛acy, ˙ze formuła nie jest spełniona w danym syste-mie, co jest niezwykle pomocne przy projektowaniu i wykrywaniu problemów z systemem. Istnieje równie˙z trzecia mo˙zliwo´s´c, w której narz˛edzie nie poradzi sobie z liczb ˛a stanów modelu i nie zwróci ˙zadnego wy-niku w akceptowalnym czasie lub zwróci bł ˛ad ze wzgl˛edu na niewystarczaj ˛ac ˛a ilo´s´c dost˛epnych zasobów (wykorzystanie pami˛eci).
Bardzo istotne jest, aby nie miesza´c poj˛ecia modeluM z wła´sciwym fizycznym systemem. Modele s ˛a abstrakcjami, które celowo pomijaj ˛a wiele fizycznych atrybutów fizycznego systemu, które nie s ˛a istotne do weryfikacji danego zbioru własno´sci. Jest to mechanizm podobny do abstrakcji znanych z matematyki czy mechaniki. Abstrakcje s ˛a niezwykle przydatnym sposobem skupienia si˛e na istocie analizowanego pro-blemu [65]. Jest to równie˙z zwi ˛azane z problemem eksplozji stanów – odtworzenie wszystkich wła´sciwo´sci systemu w modelu skutkowałoby powstaniem ogromnej liczby stanów, których sprawdzenie nie byłoby mo˙zliwe w akceptowalnym czasie na dost˛epnej infrastrukturze. Cz˛e´sciowym rozwi ˛azaniem problemu eks-plozji stanów mo˙ze by´c przeniesienie modelu na wy˙zszy poziom abstrakcji.
4.1.3 Silne i słabe strony
Jak ka˙zda dost˛epna technika sprawdzania jako´sci systemów weryfikacja modelowa posiada silne i słabe strony, z których nale˙zy sobie zdawa´c spraw˛e, aby odpowiednio dobra´c podej´scie i narz˛edzia przy tworzeniu produktu. Do zalet tego podej´scia zaliczane s ˛a [6]:
• Uniwersalno´s´c – mo˙zliwo´s´c zastosowania do szerokiego spektrum systemów, takich jak systemy wbu-dowane, in˙zynieria oprogramowania czy projektowanie sprz˛etu
• Umo˙zliwienie cz˛e´sciowej weryfikacji systemu – własno´sci sprawdzane s ˛a niezale˙znie i nie jest ko-nieczne wyspecyfikowanie wszystkich własno´sci (mo˙zna skupi´c si˛e na tych najistotniejszych). • Sprawdzanie wszystkich mo˙zliwych stanów – w przeciwie´nstwie do testowania czy symulacji, które
sprawdzaj ˛a jedynie niewielki podzbiór stanów i najcz˛e´sciej nie s ˛a w stanie zagwarantowa´c, ˙ze testo-wany problem w systemie nie wyst˛epuje.