Zastosowanie metod formalnych ...

Projekt badawczy nr 4 T11C 035 24

Zastosowanie metod formalnych do wspomagania wytwarzania poprawnego oprogramowania systemów czasu rzeczywistego

Projekt realizowany jest przez zespół z Laboratorium Informatyki, Katedry Automatyki AGH w Krakowie.

Zapraszamy do współpracy wszystkich chętnych, w szczególności studentów kierunków Informatyka oraz Automatyka i Robotyka, którzy chcieliby pisać prace magisterskie związane z inżynierią oprogramowania.

Nasz adres e-mail: adder@agh.edu.pl

Opis

Tematyka proponowanego projektu dotyczy wykorzystania kolorowanych sieci Petriego jako formalnej metody do tworzenia specyfikacji wymagań dla systemu czasu rzeczywistego i jako algebraiczno-graficznego języka do projektowania wykonywalnego modelu takiego systemu. Dodatkowo, w odniesieniu do analizy własności rozwijanego modelu, sieci Petriego będą wspierane przez logiki temporalne i algebry procesów. Zasadniczym celem naukowym jest opracowanie metod wykorzystania kolorowanych sieci Petriego (wraz z formalizmami wspomagającymi) do wytwarzania poprawnego oprogramowania systemów czasu rzeczywistego, począwszy od faz analizy i specyfikacji wymagań, a kończąc na etapie projektowania.

Rezultaty badań naukowych będą miały zarówno charakter teoretyczny jak również poparte będą praktycznymi zastosowaniami.
W dziedzinie osiągnięć teoretycznych należy spodziewać się następujących podstawowych rezultatów:

rozszerzenie możliwości wykorzystania D-sieci przez ich hierarchizację oraz opracowania nowych metod badań ich własności;
opracowanie metod i algorytmów formalnej analizy poprawności specyfikacji wymagań;
opracowanie metod dowodzenia zgodności modelu w formie kolorowanej sieci Petriego ze specyfikacją wymagań;
przeniesienie do obszaru sieci Petriego koncepcji bisymulacji i opracowanie odpowiednich algorytmów;
adaptacja zagadnienia poprawności względnej wykorzystująca funkcję obserwacji dla modelu i specyfikacji wymagań opisanych kolorowanymi sieciami Petriego;
opracowanie metod weryfikacji własności temporalnych dla modelu skończenie stanowego sieci Petriego.

Wymiernym efektem pracy programistycznej będzie narzędzie typu CASE (na licencji freeware) wspomagające projektowanie oprogramowania systemów czasu rzeczywistego, bazujące głównie na formalizmie sieci Petriego. Oprogramowanie to będzie stanowić implementację obecnych i uzyskanych w trakcie realizacji projektu wyników teoretycznych. Z założenia będzie oprogramowaniem uniwersalnym, mogącym współpracować z różnymi systemami do analizy sieci Petriego.