I. Tematy raczej praktyczne
Weryfikacja programów binarnych
| Kontunuacja pracy magisterskiej z zeszłego roku. Celem pracy jest opracowanie metody weryfikacji programów w sytuacji, gdy dysponujemy tylko kodem binarnym, a kod źródłowy jest niedostępny. Użyjemy (i zaadaptujemy) narzędzie CBMC, służące do weryfikacji programów w C. Praca polegać będzie na zastąpieniu języka wejściowego CBMC przez język maszynowy, lub jego rozsądny podzbiór, wybranego procesora. |
Usprawnienie weryfikacji programów wskaźnikowych
| Kontunuacja pracy magisterskiej z zeszłego roku. W jej wyniku powstało rozszerzenie narzędzia CBMC, usprawniające weryfikację programów operujących na wskaźnikach. Usprawnienie to zachowuje poprawność weryfikacji przy założeniu deterministycznych wskaźników, czyli wtedy, gdy adres odwołania do pamięci jest zawsze jednoznaczny (deterministyczny). (W CBMC, jednym ze źródeł niedeterminizmu są dane wejściowe weryfikowanego programu.) Celem pracy jest eksperymentalne porównanie orginalnego CBMC i jego usprawnionej wersji. Prawdopodobnie będzie też konieczne poprawnienia analizy wskaźników wykonywanej w CBMC, w celu wykorzystania w pełni możliwości oferowanych przez determinizm wskaźników. |
Sprawdzanie równoważności programów
| Celem pracy jest adaptacja ograniczonej weryfikacji modelowej, np. w wydaniu zaimplementowanym w narzędziu CBMC, do znajdowania nierównoważności programów w C. Wynikiem będą wykonania dwóch programów, dające różne wyniki dla tych samych danych wejściowych (o ile takie odróżniające wykonania istnieją, i o ile są one wystarczająco krótkie). Zakładamy, że programy są nieskomplikowane, np. nie wywołują funkcji, nie alokują dynamicznie, itp. |
Analiza wrażliwości ścieżek sygnałowych
| Biologia systemów to dziedzina bioinformatyki, w której analizuje się modele matematyczne systemów biologicznych (biochemicznych), takich jak komórka lub jej składowe. Ostatnio coraz szersze zainteresowanie w tej dziedzinie znajdują formalne metody weryfikacji, np. weryfikacja modelowa (ang. model-checking), głownie probabilistyczna. Celem pracy będzie analiza wrażliwości probabilistycznego modelu szlaku sygnałowego. Użyjemy albo narzędzia PRISM, albo któregoś z narzędzi implementujących tzw. Monte Carlo Model Checking. Eksperymenty przeprowadzone zostaną w środowisku Taverna. |
Modelowanie systemu sygnalizacji świetlnej
| Celem pracy jest stworzenie matematycznego modelu systemu sygalizacji świetlnej, przy użyciu automatów czasowych. Efektywność (przepustowość) modelu zależeć będzie od wielu parametrów, takich jak długość oczekiwania na zielone światło, przesunięcie czasowe pomiędzy zsynchronizowanymi skrzyżowaniami, itp. Wyznaczenie wartości optymalnych dla tych parametrów będzie jednym z celów pracy. Praca ma w dużym stopniu charakter eksperymentalny, eksperymenty będą przeprowadzone w narzędziu UPPAAL. |
II. Tematy raczej teoretyczne
Symulacja pomiędzy automatem skończonym a siecią Petriego
| Temat dotyczy zagadnienia symulacji pomiędzy systemem skończom a systemem nieskończonym opisanym przez sieć Petriego. Wiadomo, że symulacja w obydwu kierunkach jest rozstrzygalna, ale niewiele wiadomo nt. złożoności. Wstępne wyniki dają EPXSPACE-trudność, ale pewnie można je łatwo poprawić. Ponadto jest ciekawe pytanie: czy istnieje skończona (ograniczona) symulacja? Problem ten jest motywowany modelami tzw. web serwisów, a jego rozstrzygalność jest wciąż otwarta. |
Problemy decyzyjne dla jezykow przemiennych
| Chodzi o problem przynaleznosci (czy dane slowo nalezy do jezyka) i rownosci (czy dwa jezyki sa rownowazne) dla bezkontekstowych jezykow przemiennych. Przemiennosc oznacza, ze zamiast slow mamy do czynienia ze skonczonymi multizbiorami. Dla problemu przynaleznosci, w szczegolnym przypadku jezykow regularnych, nie jest wciaz jasne, czy jest on wielomianowy (na pewno jest w NP). Dla problemu rownosci wciaz nie jest znana dokladna zlozonosc (jest w NEXPTIME). Problem przynaleznosci dla jezykow przemiennych to to samo, co osiagalnosc (reachability) w sieciach Petriego bez komunikacji. A problem rownosci to ,,reachability equivalence'' w takich sieciach. |
Problemy decyzyjne dla modeli obliczeń z błędami
| Maszyny licznikowe albo maszyny (automaty) z FIFO są równoważne maszynom Turinga co do siły wyrazu. Wyobrażmy sobie, że dopuszczamy pewien rodzaj usterek (błędów) podczas obliczeń: wartości liczników (zawartość FIFO) mogą w sposób niekontrolowany zmniejszać się (w innym wariancie mogą się zwiększać). Model z błędami jest słabszy i np. ma rozstrzygalny problem stopu. Praca powinna zawierać przegląd ostatnich wyników. Możemy też spróbować rozwiązać jakiś problem wciąż otwarty. Np. nie wiadomo, czy ograniczoność maszyn ze ,,zwiększającymi się'' licznikami jest rozstrzygalna. Nie wiadamo też, jakie języki są rozpoznawane przez automaty z FIFO. |
S. Lasota (2010.04.14)