Szaturáció alapú modellellenőrzés kiterjesztésének vizsgálata

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

A lineáris temporális logikai (LTL) specifikációk verifikációjára számos explicit és szimbolikus modellellenőrzési technikát dolgoztak ki az elmúlt évtizedekben. Manapság a kutatások meghatározó iránya a két algoritmuscsalád előnyeinek kombinálása, legfőképp az ún. "on-the-fly" (menet közbeni) modellellenőrzés megvalósítása szimbolikus kódolást használva. Az LTL modellellenőrzés megvalósításához két problémát kell megoldani: ki kell számolni a rendszer állapotterének és a követelményt leíró automatának a szinkron szorzatát, majd ebben ellenpéldákat, vagyis hibás lefutásokat keresni. Utóbbi visszavezethető körök vagy erősen összefüggő komponensek keresésére a szorzatot leíró gráfban. Konkurens rendszerek esetén az ún. szaturációs algoritmus nagyon hatékony megoldásnak bizonyult a szimbolikus állapottér-felderítés problémájának megoldására.

Jelen diplomamunka célja egy olyan új megoldás bemutatása, amely a szaturációs algoritmus előnyeit mind a szorzat közvetlen kiszámításában, mind egy erősen összefüggő komponenseket kereső inkrementális fixpont-számító algoritmusban kiaknázza. A keresést kiegészítve explicit megoldások és absztrakció segítségével a bemutatott algoritmus menet közben az ellenpélda hiányát is megpróbálja bebizonyítani. Az eredmény egy "on-the-fly" működésű, inkrementális LTL modellellenőrző algoritmus ami a Model Checking Contest modelljein végzett kísérletek alapján jól skálázódik a vizsgálandó modell méretével.

Letölthető fájlok

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