Dizertační práce
Proveditelné specifikace
Jeden z nedostatků klasických metod pro specifikaci softwarových požadavků je obtížnost ověření konzistence a adekvátnosti specifikací. Softwarové inženýrství reagovalo na tuto skutečnost různými metodami (např. model based software engineering, agile software development, executable algebraic specification), které umožňují vidět praktické chování specifikací ve vývojovém procesu co nejdříve. Tyto metody ale dělají kompromisy ohledně jiných aspektů, týkajících se např. expresivity anebo preciznosti. V rámci tohoto tématu student navrhne formální jazyk, který splní dva na první pohled protichůdné cíle:
• Jazyk má expresivitu tak vysokou, aby mohl sloužit k pohodlnému psaní specifikací
• Specifikace v tomto jazyku se dají provést podobně jako programy v obvyklém programovacím jazyku
Klíčem pro současné splnění obou cílů budou anotace, kterými uživatel jazyku poskytuje informaci o vykonávání specifikace tak, aby zvýšená snaha o psaní anotací měla za důsledek zvýšenou účinnost vykonávání. Prvním krokem bude vývoj nástroje pro výuku, který dovoluje studentům, kteří píšou specifikace jako úkol ve cvičení, jejich řešení hned i spustit a otestovat.
Řešení omezujících podmínek
Vyvíjíme software, teorii a algoritmy, které umí řešit matematické formule obsahující nelineární rovnice a nerovnice, konjunkce, disjunkce, a logické kvantifikátory. Aplikujeme výslednou technologii v několika oblastech (např. verifikace složitých systémů, výpočet Lyapunových funkcí). Nabízíme velké množství témat v této oblasti.
Více informací:
Verifikace složitých systémů
Vlak Pendolino z Prahy do Ostravy měl na začátku vážné problémy: občas zastavoval během jízdy kvůli chybě v softwaru. Podobné chyby způsobovaly vážná neštěstí, například havárii raketoplánu Ariane 5 v roce 1996. Náš výzkum je zaměřen na pomoc s tím, aby se v budoucnosti bylo možné takovým problémům vyhýbat. Nabízíme velké množství témat v této oblasti.
Více informací: