Petri-hálók irányított modellellenőrzése

OData támogatás
Konzulens:
Molnár Vince
Méréstechnika és Információs Rendszerek Tanszék

A modellellenőrzés egy formális verifikációs technika, melynek feladata a rendszerrel szemben támasztott követelmények matematikailag precíz ellenőrzése a rendszer viselkedésmodelljén. A modellellenőrzés előnye, hogy a követelmények megsértése esetén képes végrehajtási szekvenciával (ellenpéldával) demonstrálni a rendszer helytelen működését. Állapotelérhetőség vizsgálatakor kiemelten fontos az elérhető állapotokba vezető szekvenciák generálása, mivel sok alkalmazási területen (például modellalapú tesztelés) a fő kimenet maga az ellenpélda.

Az első modellellenőrzők a problémát a rendszer lehetséges állapotainak szisztematikus és gyakran kimerítő átvizsgálásával, vagyis az állapottér gráfjának előállításával oldották meg. Ezeket az algoritmusokat explicit modellellenőrzőknek nevezzük, mivel az állapotokat és állapotátmeneteket explicit módon tartják nyilván. Ez a megoldás azonban nagyon hamar korlátokba ütközik, mivel az állapottér már viszonylag kis modellek esetén is kezelhetetlenül nagyméretű lehet: ezt a jelenséget a szakirodalom állapottér-robbanásnak nevezi.

Konkurens rendszerekben az állapottér-robbanásnak gyakori oka az egymástól független aszinkron műveletek teljes sorrendezése, amely rengeteg, a követelmény szempontjából érdektelen köztes állapothoz vezet. A részleges rendezéses redukció az ekvivalens sorrendezéseket egyetlen reprezentatív szekvenciával helyettesítve csökkenti a bejárt állapotok számát. A módszer az explicit modellellenőrzésre épít, így az ott használt technikák többnyire alkalmazhatóak maradnak.

Az állapottér-robbanás kezelésének egy másik módja az irányított modellellenőrzés. Ez a módszer csak akkor hatékony, ha előre tudjuk, hogy a keresett állapot elérhető (ez többféleképp biztosítható, például egy szimbolikus ellenőrzéssel). A módszer kihasználja, hogy ha a célállapot elérhető akkor elegendő egy oda vezető utat felfedezni a teljes állapotér helyett, ezáltal csökkentve a memóriahasználatot. Ezt úgy valósítjuk meg, hogy hagyományos keresési algoritmusok helyett vezérelt keresést alkalmazunk és egy heurisztikával irányítjuk az állapottér-bejárást a célállapot felé, tehát nem végzünk hagyományos kimerítő keresést.

A dolgozatban bemutatunk egy irányított modellellenőrzőt, ami egy új heurisztikával irányítja az állapottér bejárást. Ezt a módszert kombináltuk a részleges rendezés redukcióval, hogy az algoritmus nem elérhető célállapotok esetén is hatékony maradjon. A dolgozat végén mérésekkel demonstráljuk az általunk készített eszköz képességeit és kiértékeljük megközelítésünk előnyeit és hátrányait.

Letölthető fájlok

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