Tanszéki konzulens: 

Zavada Ármin Zsolt doktorandusz Szoba: IL405 Tel.: +36 1 463- Email: zavada (*) mit * bme * hu

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.