Biztonságkritikus rendszereket általában magasszintű modellekkel írunk le, mert az precizebb leírást ad, mint a tradicionális dokumentum-központű megközelítés. A magasszintű mérnöki modellek azonban csak akkor hasznosak, hogyha megbízhatunk azok struktúrájában és az általuk leírt viselkedés helyességében. Mivel ezt kézzel költséges vizsgálni és garantálni, manapság automatizált V&V eszközökkel tehermentesítjük a rendszermérnököket. Habár vannak ilyen eszközök, a fejlesztésük és elkészítésük rendkívül költséges, mert gyakran újabb nyelvek támogatásához rendszerint mindent újra kell implementálnunk, mert a nyelvek apróbb sajátosságai ellehetetlenítik az újrahasználhatóságot. Ennek kiküszöbölésére újszerű megközelítés a szemantikus modellek alkalmazása, amely az eszköz forráskódja helyett egy külső, könnyedén cserélhető és módosítható modellben tárolja a nyelv strukturális és viselkedési sajátosságait, úgymond "scriptelési" lehetőséget adva a V&V eszköz felett. A megközelítés előnye, hogy újabb nyelvek támogatása valamint meglévő eszközök módosítása már megtörténhet a konkrét V&V eszköz forráskódjának módosítása és újrafordítása nélkül, ami drasztikusan csökkenti a szükséges erőforrást. A Semantifyr keretrendszer egy szemantikus modellezési nyelv, hozzá tartozó fordítóprogramok és egyéb szolgáltatások összessége, amely lehetővé teszi magasszintű mérnöki nyelvekhez szemantikus modellek készítését, valamint V&V eszközök fejlesztését. A feladat meglévő vagy új magasszintű nyelvekhez (például SysML, SysMLv2, AADL, ...) szemantikus modell és V&V eszköz fejlesztése a Semantifyr keretrendszer segítségével. A téma kihívása a megközelítés újszerűsége, így rengeteg kihívás és izgalom várja a lelkes hallgatókat: - Hogyan garantálhatjuk - vagy legalább vizsgálhatjuk - a szemantikus modell helyességét? - Hogyan garantálhatjuk a fordító (Semantifyr) helyességét? - Hogyan könnyíthejük meg a szemantikus modellek fejlesztési folyamatát? VS Code, IntelliJ és egyéb fejlesztői környezetekkel való integrálás? Debugging, szimulálás, generatív AI integrálás? Újabb nyelvi elemek támogatása? - Hogyan optimalizálhatjuk az előállított (a fordító kimenete) analízis modellt? Hogy tudunk megküzdeni a formális verifikáció algoritmikus nehézségével? - Hogyan lesz ez az egész V&V folyamat láthatatlan, és legfőképpen, hasznos a mérnök számára? A témára akár több hallgató is jelentkezhet, a pontos részfeladatok és kiírás meghatározására a konzulenssel egyeztetve kerül sor, különös tekintettel a hallgató érdeklődési körére és preferenciáira.