Transzformált formális modellek automatikus analízisének lépései

Egy ipari rendszer automatikus analízise megoldható pl. úgy, hogy a mérnöki tervező rendszerben elkészített "félformális" modellt automatikusan formális modellé transzformáljuk, majd ezt a modellt ellenőrizzük formális módszerekkel. A modelltranszformáció azonban csak egy eleme ennek a folyamatnak. Ezen felül a formális modell "nyelvén" ki kell fejezni az ellenőrzendő kritériumokat, majd az analízis végeztével az ellenőrzés során felfedett esetleges problémákat, ellenpéldákat "vissza kell vetítetni" a kiinduló mérnöki modellbe.

A hallgató feladata ezen átalakítások valamely kiválasztott aspektusának megvalósítása elméleti, esetleg gyakorlati szempontból.