Petri-háló alapú formális modellek analízise hatékony korlátos modellellenőrzési technikák segítségével

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

A rendszertervezés során a szoftver- és hardverrendszerek helyességének ellenőrzése, azaz verifikációja egyre nagyobb szerepet kap. A verifikációval kapcsolatban alapvető elvárás, hogy teljes körű és matematikai precizitású legyen, ami formális módszerek alkalmazását igényli. Komplex rendszerek esetén a formális verifikáció igen számításigényes probléma. Bár a rendelkezésre álló számítási kapacitás növekszik, még mindig komoly kihívást jelent a nagyméretű, összetett architektúrák ellenőrzése.

A verifikáció folyamatában gyakran alkalmazott módszer a modellellenőrzés. Ennek során elkészítjük a rendszer egy modelljét – jelen esetben Petri-hálók segítségével –, majd felderítjük annak állapotterét. Utána az állapottérben a specifikációhoz kötődő kritériumok teljesülését ellenőrizzük – jelen esetben temporális logikai kifejezések segítségével megfogalmazott követelmények formájában – matematikai módszerek alkalmazásával.

Korábbi munkáinkban bemutattuk, hogy az ún. szaturációs algoritmus használatával az állapottér hatékonyan felderíthető és kompakt formában tárolható. Összetett rendszerek modellellenőrzése során azonban felmerülnek olyan problémák, amelyekre az eddigi algoritmusaink nem nyújtottak megoldást. Ilyenek többek között a nagy komplexitású és/vagy végtelen állapotterű modellek analízise.

Munkám során a korlátos modellellenőrzési technikákat vizsgáltam meg a felmerült problémákra.

– Megvizsgáltam a szaturáció alapú korlátos állapottér-felderítést és modellellenőrzést, amelynek segítségével a teljes állapottér bejárása nélkül is lehetőség van bizonyos követelmények ellenőrzésére, így lehetővé téve a komplex rendszerek, nagy vagy végtelen állapotterű modellek vizsgálatát.

– Megvizsgáltam az ún. vezérelt szaturációt, amely a kifejezések ellenőrzése során mutatkozó, felesleges bejárási lépések redukálásával gyorsítja a modellellenőrzést.

– A korlátos állapottér-felderítést és a vezérelt szaturációt ötvözve létrehoztam egy hatékony szaturáció alapú korlátos modellellenőrző algoritmust, amely a korábbi algoritmust jelentősen felgyorsítja.

– Megvizsgáltam a korlátos modellellenőrzés teljességét háromértékű logikák segítségével, amely következtében pontosabb válasz adható korlátos modellellenőrzés alapján a kiértékelendő kritériumokra.

A vizsgált korlátos szaturációs modellellenőrzési algoritmusokat és vezérelt szaturációs algoritmusokat a Méréstechnika és Információs Rendszerek Tanszéken fejlesztett PetriDotNet keretrendszer részeként a gyakorlatban is megvalósítottam, hatékonyságukat mérésekkel támasztottam alá dolgozatomban.

Letölthető fájlok

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