Modell-alapú kényszerkielégítési problémák megoldása SMT környezetben

Automatizált modellgenerálási és modellmódosítási feladatok után előálló modellek esetében gyakran megsérülnek, vagy eleve nem teljesülnek a modellekkel szemben támasztott kiegészítő követelmények. Ezen követelmények érvényre juttatásához a modellekben szereplő, de hiányosan kitöltött attribútumok, relációk kitöltése, létrehozása szükséges, ezáltal kielégítve egy komplex követelményrendszert. Ezen modell-alapú kényszerkielégítési probléma napjaink aktív kutatási területe.

A hallgató feladata, hogy ezen probléma egy adott technológiai megvalósítását megtervezze és elkészítse. A modellek az Eclipse Modeling Framework (EMF) keretrendszer modellezési formátumában állnak rendelkezésre, melyhez kiegészítő OCL nyelvű kényszerek fogalmazhatóak meg. A hallgató feladat a bemeneti metamodell, modell és kényszerek által kialakított kényszerkielégítési probléma leképezése SMT nyelvre és a hatékony megoldás
elősegítése.

A hallgató feladata továbbá az elkészített módszertan bemutatása gyakorlati alkalmazásként a tanszéken folyó R3Cop kutatási projekt keretében. A projekt célja autonóm robotok tesztelésének támogatása automatikus tesztkörnyezet generálás segítségével. A tesztkörnyezet egy absztrakt metamodellével és hozzá kapcsolódó OCL megkötésekkel adott, amiből több lépésen keresztül konkrét, majd akár robot-szimulátor specifikus környezeti modellek állíthatóak elő. Az előállítás folyamán szükséges lépés a metamodellhez kapcsolódó OCL megkötések értelmezése, azok automatizált feldolgozása, kényszerkielégítési problémák előállítása és megoldása.