Aszinkron rendszerek heurisztikával támogatott modellellenőrzése

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

Napjaink informatikai alkalmazásaival szemben támasztott fontos követelmény a szolgáltatásbiztonság, azaz annak az igénye, hogy mindig, igazoltan bízni lehet a rendszer által nyújtott szolgáltatásokban. A szoftver és hardver rendszerek azonban mára olyan komplexitást értek el, hogy támogatás nélkül azt a fejlesztőmérnökök már nem képesek átlátni. Manapság a probléma megoldására a különböző formális módszereken alapuló megoldások terjedtek el leginkább. A szakdolgozat ezek közül a modellellenőrzés témakörével foglalkozik részletesen, amely egy automatizált verifikációs módszer a rendszerrel szemben támasztott követelmények kimerítő ellenőrzéséhez. Ehhez a legtöbb esetben szükség van arra, hogy a rendszer elérhető állapotait előállítsuk, ez után nyílik lehetőség a kívánt tulajdonság ellenőrzésére.

A modellellenőrzés során problémát jelent az úgynevezett állapottér robbanás nevű jelenség, amely azt mondja, hogy a rendszer komplexitásának növekedésével a rendszer állapotterének felderítéséhez szükséges futási idő és az állapotok tárolásához szükséges tárigény exponenciálisan nő. Ezen nehézségek orvoslására számos irányban indultak el a kutatók. Az idő –és tárigény problémáját hatékonyan lehet kezelni az úgynevezett szaturációs algoritmus alkalmazásával, amelyet aszinkron rendszerek állapotterének felderítéséhez fejlesztettek ki. Jogos igényként merül fel a párhuzamos modellellenőrző kialakítása is, hiszen a manapság használatos hardverek nagy része már több processzormaggal rendelkezik. A TDK dolgozatunkban a szaturációs algoritmus párhuzamosítási lehetőségeivel foglalkoztunk, amelynek fontosabb részei a szakdolgozatban is bemutatásra kerülnek.

A modellellenőrzés során a futási idő csökkentésében a párhuzamos megoldások mellett nagy szerepet kapnak a különböző heurisztikán alapuló megoldások is. A szakdolgozatban részletesen bemutatásra kerül az úgynevezett heurisztikán alapuló tranzíció-előretüzelés módszere, amely a TDK dolgozat egyik megjelölt lehetséges folytatási iránya volt. Az algoritmus motivációját az adta, hogy a párhuzamos szaturációs algoritmus egyes modellek esetén nem használta ki teljesen a rendelkezésre álló számítási erőforrásokat. Ezeket a tartalék erőforrásokat arra lehetne kihasználni, hogy az állapottér egyes részeit előre felderítésük, ezzel tovább gyorsítva a párhuzamos algoritmus futását. Ebben kapnak szerepet a heurisztikák, ugyanis nem triviális az, hogy milyen módon kell az állapottér részeket előre felderíteni úgy, hogy az ténylegesen hasznos legyen később.

A szakdolgozat keretében különféle heurisztikákat dolgoztam ki és ezeket különböző statisztikák alapján hasonlítottam össze. Az elkészült modult integráltam a Méréstechnika és Információs Rendszerek Tanszéken fejlesztett PetriDotNet modellellenőrző keretrendszerbe és több modellre is összehasonlítottam a meglevő szekvenciális és párhuzamos állapottér-felderítő algoritmusok futási sebességét az előretüzeléses változatéval. A mérések alapján elmondható, hogy több esetben sikerült valós sebességnövekedést elérni a párhuzamos változathoz képest, de olyan eset is volt, amelyre a szekvenciális változat ugyan gyorsabb volt, mint a párhuzamos, de az előretüzeléssel is kiegészítve a párhuzamos algoritmust már nem volt tapasztalható jelentős különbség a két változat futási idejében.

Letölthető fájlok

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