Hibaterjedés-modellezés támogatása Java PathFinderrel

OData támogatás
Konzulens:
Kocsis Imre
Méréstechnika és Információs Rendszerek Tanszék

Az informatikai, rendszerszintű hibaterjedés-diagnosztika célja, hogy különálló szoftver- és hardverkomponensekből álló rendszerekben különböző hibaok-típusok hatásanalízisét és a hibahatások okának meghatározását lehetővé tegye. A rendszerszintű következtetés támogatásához azonban szükséges a rendszer alkotóelemeire vonatkozó hibaterjedési szabályok ismerete – egy adott komponens(típus) kimenetein milyen hibák jelen(het)nek meg külső és belső hibaokok hatására.

Komponensszintű hibaterjedési szabályok előállítására ismertek modellellenőrzési (model checking) technikák. Ezek gyakorlati alkalmazhatóságát azonban kérdésessé teszi, hogy a szokásosan alkalmazott modellellenőrző eszközök többsége komponens modellt, nem pedig rendelkezésre álló szoftvert vizsgál. Az ismert kivételek egyike a Java PathFinder, mely egy közvetlenül Java bytecode-ot vizsgáló modellellenőrző eszköz. Különlegessége, hogy a „külvilággal” (pl. állományrendszer, hálózat) való kommunikáció modellezését Java könyvtári osztályok egyfajta „lecserélésével” teszi lehetővé. A hálózatba kötött Java alkalmazások ellenőrzésére a Java PathFinderhez elérhető megoldások azonban erősen kezdetlegesek; hibaterjedési szabályok felderítésére csak korlátozásokkal alkalmazhatóak.

Célom olyan megoldás összeállítása, mellyel hibaterjedést tudok vizsgálni adatfolyam hálózatokban. A hiba komponensről komponensre terjedhet hálózati kommunikáció által, ezért a Java PathFindert fel kell készíteni hálózati forgalmat generáló, és hálózati forgalom által vezérelt működésű programok verifikációjára. A kommunikációs hálózatot használó programoknál ismertek különféle modellellenőrzési akadályok, melyeket előfeltételezésekkel, vagy más módon ki kell küszöbölni. A dolgozatban megoldási lehetőségeket vizsgálók meg, és ezeket összehasonlítom több szempont szerint.

Letölthető fájlok

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