Lineáris tranzíciós rendszerek absztrakt interpretáció alapú verifikációja

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

A lineáris tranzíciós rendszerek, mint például a Petri-hálók, többek között az aszinkron, elosztott, konkurens, párhuzamos és nem-determinisztikus rendszerek elterjedt grafikus és matematikai modellező eszközei. A lineáris tranzíciós rendszer modellek viselkedését az állapottér, azaz az elérhető állapotok és az állapotátmenetek halmaza adja meg. Lineáris tranzíciós rendszerek analízisekor fontos kérdés az állapotelérhetőség, amely során azt vizsgáljuk, hogy egy adott célállapot része-e az állapottérnek. Az elérhetőségi probléma Petri-hálók esetén EXPSPACE-nehéz, lineáris tranzíciós rendszerek esetén eldönthetetlen.

Végtelen állapotterű modellek analízisére nyújtanak megoldást a különböző, matematikai absztrakción alapuló módszerek. Ezen módszerek előnye, hogy egy véges állapottér reprezentációt építve és azt bejárva vizsgálják az elérhetőségi és/vagy invariáns tulajdonságokat. Az absztrakt interpretáció algoritmusa a véges reprezentációt konvex poliéderek segítségével állítja elő, így felülbecsülve a lehetséges elérhető állapothalmazt. Petri-háló alapú modellek esetén azonban az irodalomban ismert módszerek sokszor nem képesek elég precíz becslést adni. Munkám során ezen módszerek továbbfejlesztésével és lineáris tranzíciós rendszerekre való kiterjesztésével foglalkoztam.

A dolgozatban bemutatok olyan, az absztrakt interpretáció finomításán alapuló algoritmusokat, amelyek segítségével olyan rendszerek vizsgálhatóságát is lehetővé tettem, amelyre a korábbi algoritmusok nem voltak képesek. Kifejlesztettem egy új algoritmust, amely a felderített állapotteret finomítja az elérhetőségi feltétel figyelembevételével. Emellett pedig mutatok egy módszert, amely az explicit állapottér bejáró és az absztrakt interpretáción alapuló algoritmusokat együttesen alkalmazza a hatékonyság növelése érdekében.

Az új algoritmusok előnyeit mintapéldákkal szemléltetem, hatékonyságukat méréssel bizonyítom.

Letölthető fájlok

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