Végtelen állapotterű gráftranszformációs rendszerek helyességellenőrzése

Napjainkban a modellvezérelt tervezési módszertan egyre növekvő térhódítása figyelhető meg a rendszertervezés területén. A modellvezérelt tervezést egy precíz modellezési fázis vezet be, amely során számos nézőpontból vizsgáljuk meg a tervezés alatt álló rendszert, majd az integrált rendszertervet precíz matematikai analízisnek vetjük alá automatikus modelltranszformációk által. A garantált minőségű rendszertervből kiindulva az alkalmazás forráskódját és a telepítési információt automatikus kódgenerálás segítségével származtatjuk, amelyet tipikusan szintén egy speciális modelltranszformációnak tekinthetünk

Automatikus modelltranszformációk alkalmazásakor azonban problémát jelent, hogy vajon mennyire megbízhatóak maguk a modelltranszformációk. Amennyiben a transzformációk specifikációi koncepcionális hibákat tartalmaznak, ezek megjelennek a modelltranszformációk végrehajtásakor is, így gyakorta maguk a modelltranszformációk jelentik a minőségi szűk keresztmetszetet. Ezt elkerülendő, egyre inkább elengedhetetlenné válik a modelltranszformációk formális helyességellenőrzése.

A jelölt feladata, hogy áttekintse a gráf alapú modellek felett értelmezett shape analízis helyességellenőrzési módszerét, megvizsgálva a szakirodalomban kidolgozott analízis technikák átültethetőségét a VIATRA2 modelltranszformációs keretrendszer felett