Petri-hálók szaturációs algoritmuson alapuló korlátos modellellenőrzésének inkrementális kiterjesztése

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

Napjainkban a biztonságkritikus alkalmazásoknál és azokon kívül is egyre elterjedtebb a formális módszerek, mint például a modellellenőrzés használata a minőség és megbízhatóság növelése érdekében. Azonban a komplex rendszerek vizsgálata az erőforrások korlátossága miatt nehéz feladatnak bizonyul. Emiatt számos új modellellenőrző algoritmus látott napvilágot. Közülük egy a szaturációs algoritmus, amely kompakt adatreprezentációjának és speciális iterációs stratégiájának köszönhetően igen hatékonynak bizonyult, különösen aszinkron rendszerek vizsgálata esetén.

A szaturációs algoritmusnak létezik korlátos állapottér-felderítést megvalósító variánsa, amely az ún. sekély problémák vizsgálata esetén ideális. Azonban az eddigi, ezen alapuló korlátos modellellenőrző algoritmus csak neminkrementális módon (minden iterációban a folyamatot teljesen újrakezdve) képes működni.

Diplomatervemben megvizsgálom a Petri-hálókon alapuló modellellenőrzés valamint a szaturációs algoritmusok elméleti alapjait. Áttekintem az ide vonatkozó szakirodalmat és ez alapján a diplomatervemhez szükséges alapismeretek kivonatát, amely bemutatja a modellellenőrzés, a Petri-hálók, a döntési diagramok és a szaturációalapú algoritmusok alapjait.

Megvizsgálom továbbá a korábban publikált főbb szaturációalapú korlátos és nemkorlátos állapottér-felderítő algoritmusokat, illetve modellellenőrzési megoldásokat. Áttekintem a szaturációalapú algoritmusok közös vonásait, közös alapelveit, illetve a megvalósítás kihívásait. Megvizsgálom ezeken kívül a különböző szaturációalapú megoldások újdonságait, illetve olyan vonásait, amelyek segítségével a korlátos inkrementális modellellenőrző algoritmusok megtervezhetők.

Munkám során két új, inkrementális modellellenőrző algoritmust terveztem meg (a „folytató” és „kompaktáló” algoritmusokat), amelyek különböző módon képesek inkrementális modellellenőrzést végezni. A megtervezett algoritmusokat implementáltam, majd mérésekkel hasonlítottam össze teljesítményüket különböző esetekre.

Letölthető fájlok

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