Monitor szintézis üzenet szekvencia specifikáció alapján

OData támogatás
Konzulens:
Dr. Majzik István
Méréstechnika és Információs Rendszerek Tanszék

A szoftverfejlesztésben fontos szempont a követelmények precíz megfogalmazása mind az implementálás, mind pedig az azt követő ellenőrzés és tesztelés hatékony végrehajtása érdekében. Különösen fontos a követelmények pontos megfogalmazása biztonságkritikus alkalmazások esetén, ahol a hibák és hiányosságok könnyen balesethez is vezethetnek.

A számítógépes rendszerek működése közben bekövetkező hibák detektálásának egyik módszere a futásidőbeli verifikáció. Ennek lényege, hogy a precízen felvett követelmények alapján, forráskód generálással olyan monitor komponenseket valósítunk meg, amelyek folyamatosan követik az ellenőrzött rendszer viselkedését, és a specifikált követelményektől eltérő működés esetén jelzik a hibát.

A követelmények specifikálásának pontos, mégis intuitív módon történő megadása üzenet szekvencia diagramok segítségével valósítható meg. Az üzenet szekvencia diagramokkal rögzített követelmények monitorozásához megfigyelő automata definiálható, amely működés közben detektálja a megadott diagramtól eltérő viselkedést. A megfigyelő automata már közvetlenül felhasználható a monitor forráskódjának generálására, ami aztán a tényleges hibadetektálást elvégzi és így a kívánt verifikáció elvégezhető.

Feladatom a kiválasztott üzenet szekvencia specifikációs nyelv alapján az automata konstrukciót megvalósító eszköz megtervezése és megvalósítása, majd a szisztematikus forráskód szintézis demonstrálása.

Letölthető fájlok

A témához tartozó fájlokat csak bejelentkezett felhasználók tölthetik le.