Állapot-alapú mérnöki modellek formális verifikációja

Állapottérképeket és egyéb, állapot-alapú mérnöki modellezési nyelveket gyakran használnak a modell-alapú szoftver- és rendszerfejlesztés során. Ezek a modellek alkalmasak, hogy a rendszer viselkedését precízen leírják, továbbá implementáció is generálható (különböző kódgenerátorok segítségével) az elkészített modellekből.

A Gamma keretrendszer célja az állapot alapú mérnöki modellezés és az implementáció automatikus előállításának támogatása. A Gamma keretrendszer többek között a Yakindu állapotgépek alapján történő tervezést is támogatja, de más, nyílt forráskódú és akár kereskedelmi eszközökkel is használható együtt a mérnöki tervezés támogatására.

A mérnöki tervezés során fontos megbizonyosodni a terveink helyességéről, amely célra a validáció és a tesztelés mellett a formális verifikáció alkalmas. Formális ellenőrzés során matemaikai bizonyító algoritmusokat alkalmazunk, amelyek bejárják a modell állapotterét (gráf-bejáró algoritmusok segítségével), és a jellemzően valamilyen matemaikai logika nyelvén leírt követelmények teljesülését ellenőrzik.

A hallgató feladata megismerkedni egyrészt a mérnöki modellező eszközökkel, másrészt a formális verifikációs algoritmusokkal, és egy olyan megoldást implementálni, amely támogatja a mérnöki modellek formális ellenőrzését.