Tanszéki konzulens: 

Cziborová Dóra doktorandusz Szoba: IL 405 Tel.: +36 1 463- Email: cziborova (*) mit * bme * hu

Kritikus valós idejű rendszerek fejlesztésében kulcsfontosságú kihívás a szoftverrendszerek helyes működésének verifikációja. Az automatizált modellellenőrzésben a rendszernek egy formális (matematikai) leírásán kerülnek ellenőrzésre a kívánt biztonsági követelmények, egy automatizált eszköz által. Ezen automatizált eszközök különböző matematikai bizonyító és gráf algoritmusokat használnak működés közben.
A modellellenőrzés problémája már közepes méretű rendszereken végezve is algoritmikusan nehéz feladat, ugyanis a bejárandó állapotok száma gyakran a modell méretében exponenciálisan nő. Ezen kívül az időzítések megszámlálhatatlanul végtelen állapotteret okoznak. Annak érdekében, hogy ezen rendszerek is vizsgálhatók legyenek, hatékony algoritmusokra van szükségünk. Az önálló munka során a hallgató beletanul az egyetemen fejlesztett Theta nyílt forráskódú modellellenőrző keretrendszerbe (https://github.com/ftsrg/theta) és azt új algoritmusokkal egészíti ki.