Absztrakt interpretációt használó keresési stratégiák Petri-háló alapú modellekhez
A Petri-hálók az aszinkron, elosztott, konkurens, párhuzamos és nemdeterminisztikus rendszerek elterjedt grafikus és matematikai modellező eszközei. Petri-háló alapú modellek 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. A probléma egyszerű Petri-hálók esetén eldönthető, azonban a végtelen állapottér és a Petri-hálók nagy kifejezőereje miatt a nagyon komplex, az EXPSPACE-nehéz komplexitási osztályba tartozik. A tiltó-élekkel kibővített Petri-hálók kifejezőereje azonos a Turing gépekkel, emiatt az elérhetőségi probléma ebben az esetben már nem eldönthető.
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ő állapotokat. 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 kiterjesztésvel 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.
szerző
-
Farkas Rebeka
mérnökinformatikus
nappali
konzulensek
-
Dr. Vörös András
egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék -
-
helyezés
Ericsson Magyarország II. helyezett