Monitor generálás scenario alapú 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 komponensei közötti kommunikáció forgatókönyveire vonatkozik. Ezek a követelmények jól formalizálhatók Property Sequence Chart (PSC) segítségével. A feladat célja PSC leírásra alkalmas szöveges reprezentáció definiálása, majd ennek leképzése a monitor generáláshoz szükséges Büchi automata formátumba.