Dyplom

Praca dyplomowa dotyczy weryfikacji systemów obiektowych (Object Oriented Programming) technikami skończeniestanowymi (Model Checking) w środowisku COSMA. W uproszczeniu zamierzamy sprawdzić model systemu w oparciu o wymagania bez uruchamiania tego systemu. Wymagania (zapisane w sposób formalny) są sprawdzane grafie stanów osiągalnych (Reachability Graph). GSO zawiera wszystkie możliwe stany systemu - złe stany i złe ścieżki mogą być skutecznie wychwytywane. Jeśli nie ma takowych, to możemy stwierdzić, że system spełnia stawiane mu wymagania.

Oczywiście metoda ta ma swoje ograniczenia - musimy korzystać ze specjalnego formalizmu (CSM), GSO znacznie rośnie wraz ze wzrostem złożoności badanych systemów. Jednym z zadań realizowanych przeze mnie jest redukcja wielkości GSO.

  • Praca dyplomowa (html)
  • Praca dyplomowa na jednej stronie (html)
  • Program model_danych (ZIP, źródła C++ i wersja skompilowana dla Windows)

Rysunek pokazuje graficzną reprezentację automatów na którymi pracuję. Prostokąty o zaokrąglonych rogach to stany, strzałki reprezentują przejścia pomiędzy stanami, etykiety przy strzałkach to logiczne warunki przejść. Kiedy warunek jest spełniony automat może zmienić stan. Wewnątrz prostokątów jest nazwa stanu (na górze) i lista generowanych w tym stanie sygnałów (na dole). Proste, nieprawdaż ?

Chciałbym podziękować mojemu promotorowi Jerzemu Mieścickiemu za to, że przez dwa lata pracował ze mną nad tym tematem - jego cenne uwagi pozwoliły doprowadzić pracę do aktualnego stanu. Zapraszam do zapoznania się z tematem.

(...) Nie ma bowiem łatwych odpowiedzi. Nie istnieje nic takiego jak najlepsze rozwiązanie - zarówno jeśli chodzi o narzędzia, jak i języki czy systemy operacyjne. Są jedynie systemy, które mogą być bardziej odpowiednie w konkretnych okolicznościach.

I tu właśnie do gry wchodzi pragmatyzm. Nie należy przywiązywać się do żadnej określonej metody, ale mieć na tyle rozległą wiedzę i doświadczenie, by w danej sytuacji wybrać dobre rozwiązanie. (...)

Andrew Hunt, David Thomas "Pragmatyczny Programista"