Automatikus kódgenerátor helyességének ellenőrzése

Beágyazott rendszerekben a fejlesztés egy hatékony módja a modell alapú kódgenerálás. Erre többféle technológia is rendelkezésre áll. A tanszéken elkészült egy JET (Java Emitter Templates) alapú kódgenerátor, ami automata modellek alapján képes C nyelvű forráskódot előállítani beágyazott mikrokontrolleres rendszerekhez.

Nyitott kérdés maradt ugyanakkor, hogy a kódgenerátor bizonyítottan helyes-e, azaz a generált kód pontosan ugyanúgy viselkedik-e, ahogyan azt a kódgenerálás alapjául szolgáló modell előírja.

A hallgató feladata egy olyan módszer kidolgozása, amelynek segítségével szisztematikusan bizonyítható a kódgenerálás helyessége. Ennek alapjául szolgálhat egy olyan keretrendszer megvalósítása, ami összeveti a modell szimulációjával kapott végrehajtási útvonalakat a kód végrehajtásakor kapott (futás közben naplózott) végrehajtási útvonalakkal.