Badania naukowe


Moja praca naukowa dotyczy specyfikacji i weryfikacji systemów wieloagentowych (ang. multi-agent systems) oraz systemów czasu rzeczywistego (ang. real-time system).

Agent to jednostka, która działa w pewnym ustalonym środowisku, jest zdolna do komunikowania się, monitorowania swego otoczenia i podejmowania autonomicznych decyzji. System wieloagentowy to sieć komunikujących się i współpracujących między sobą agentów, realizujących zarówno wspólne jak i prywatne cele. Systemy wieloagentowe mają już swoją ugruntowaną pozycję w wielu dziedzinach związanych z technologią informacji, takich jak na przykład inżynieria oprogramowania, e-handel, sieci telekomunikacyjne, automatyczne wnioskowanie i argumentacja, wspomaganie zarządzaniem w przedsiębiorstwie, itd. System czasu rzeczywistego to (zgodnie z definicją IEEE) system, którego poprawność działania zależy nie tylko od poprawności logicznych rezultatów, lecz również od czasu, w jakim te rezultaty są osiągane. Systemy czasu rzeczywistego znajdują zastosowanie między innymi w przemyśle do nadzorowania procesów technologicznych, przy implementacji protokołów komunikacyjnych, w planowaniu i kontroli ruchu lotniczego, itd.

Weryfikacja modelowa jest jedną z najbardziej rozpowszechnionych metod automatycznej weryfikacji poprawności systemów informatycznych wszelkiego typu, a w szczególności systemów czasu rzeczywistego oraz systemów wieloagentowych. Głównym wynikiem dotychczasowych moich i dr Andrzeja Zbrzeznego badań w tej dziedzinie jest opracowanie oryginalnego podejścia do weryfikacji systemów zależnych od czasu, specyfikowanych poprzez standardowe automaty czasowe oraz automaty czasowe rozszerzone o zmienne całkowite oraz implementacja tego podejścia w postaci modułu do systemu weryfikacyjnego VerICS. Wszystkie wykonane prace zostały podporządkowane nadrzędnemu celowi, którym było zaimplementowanie i opublikowanie systemu weryfikacyjnego, który będzie mógł konkurować z systemami obecnymi na rynku, takimi jak UppAll, KRONOS, RED, Rabbit i inne.

Obecnie jednym z naszych (moich i dr Zbrzeznego) celów badawczych jest kontynuowanie badań nad nowymi metodami weryfikacji systemów wieloagentowych i tych zależnych od czasu, specyfikowanych przez automaty czasowe rozszerzone o warunki na zmienne całkowite, a w szczególoności takich, które mogą wykorzystywać nie tylko efektywne algorytmy testowania spełnialności formuł Boolowskich, ale również te oparte na BDD.

Drugim celem naszym badań jest weryfikacja programów współbieżnych napisanych w Javie - obecnie najpopularniejszym języku programowania wysokiego poziomu. Tutaj można zobaczyć dotychczasowe nasze osiągnięcia w tej dziedzinie.