Monitor generálás temporális logikai követelményekből

Biztonságkritikus beágyazott számítógépes rendszerekben (pl. robotok, járművek irányító rendszereiben) a működés közbeni hibák detektálásának egyik módszere a futásidőbeli verifikáció. Ennek lényege, hogy precízen felvett követelmények alapján olyan monitor komponenseket valósítanak meg, amelyek folyamatosan követik a rendszer működését, és a specifikált követelményektől eltérő működés esetén megindítják a beavatkozást (pl. a biztonságos leállást).

A monitor komponensek megvalósításának egyik hatékony módszere a formalizált követelmények alapján történő automatikus forráskód generálás. A biztonsági követelmények egy része a rendszer által generált események (üzenetek, állapotváltások) sorrendjére vonatkozik, ezek a követelmények jól formalizálhatók lineáris temporális logikák (LTL) segítségével. A feladat célja egy olyan kódgenerátor alkalmazás fejlesztése, ami LTL követelmények alapján képes az eseményszekvenciákat kiértékelő monitor forráskódjának előállítására. Ennek első lépése az LTL követelményből a monitor alapját képező véges automata (FSM) előállítása.