Állapotgép-alapú monitorgenerálás C++ környezethez

OData támogatás
Konzulens:
Vörös András
Méréstechnika és Információs Rendszerek Tanszék

A dolgozat célja, hogy egy futásidejű monitorozó komponensek generálására alkalmas módszert mutasson be, melynek alapja a Theta frontend állapotdiagram leíró nyelve - valamint adjon egy példa megvalósítást, egy Eclipse plugin formájában.

A biztonságkritikus szoftverek készítése során olyan tervezési és implementációs módszerek szükségesek, amelyek minimalizálják a hibás komponensek, illetve hibás működés előfordulásának valószínűségét. Ezek elkerülésének érdekében a tradícionális tesztelés mellett a fejlesztők formálisan ellenőrzhetik a (szintén formálisan megfogalmazott) követelményeket. Az ellenőrzés elvégézése azonban általában igen nagy számítási kapacítást igényel, amely sokszor lehetetlenné teszi az összetettebb rendszereken való alkalmazását - illetve az ellenőrzött modellek általában nincsenek felkészülve a lehetséges hardware hibákra (a komplexitás nagymértékű növekedése miatt). A működés közben fellépő hibák kezelésének egy másik megközelítése a futásidejű monitorozó komponensek használata. Ezen komponensek a már működésbe helyezett rendszer azon tulajdonságait figyelik, amelyek alapján észlelhetik az esetlegesen fellépő hibákat - majd olyan lépéseket tehetnek, amelyek minimalizálják ezek hatását.

Az ezen dolgozatban bemutatott munka célja, hogy kiterjessze a fejlesztők által alkalmazható eszköztárat egy olyan eszközzel, amely állapotdiagram segítségével leírt modellekből alacson szintű, CPU- és memóriahatékony monitorozó komponenseket generál. Ezen monitorok felhasználhatóak a rendszer változóinak és állapotainak megfigyelésére vagy rögzítésére, illetve segítségükkel akár futásidejű biztonsági logikák is implementálhatóak - a rendszer alacsony többletterhelése mellett.

A választás azért esett az állapotdiagramokra, mert a legtöbb mérnöki területen ismertek, és absztrakciós erejük megfelelő a bonyolultabb rendszerek magas szintű, de a monitorgeneráláshoz még megfelelően részletes leírásához. A Theta frontend által használt állapotdiagram nyelv igen hasonló az UML szabványban megfogalmazotthoz, néhány kiterjesztéssel és megkötéssel. A monitorok C++ nyelvű megvalósítása lehetővég teszi, hogy erőforráskorlátozott környezetben, illetve a beágyazott rendszerek széles skáláján is felhasználhatóak legyenek, és a leképzett modellek továbbra is könnyen olvashatóak maradjanak. A generált komponensek pontos erőforrásigényének meghatározása érdekében néhány tíztől néhány ezer állapottal és tranzícióval rendelkező modellek teljesítménye került megmérésre.

Letölthető fájlok

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