Petri-háló elérhetőségi algoritmusok vizsgálata

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

Napjainkban sok informatikai rendszernél követelmény, hogy igazoltan bízni lehessen a rendszer által nyújtott szolgáltatásokban. Sokszor a rendszer túl komplex ahhoz, hogy a mérnökök teljesen átlássák a működését, ezért szükség van olyan automatizálható ellenőrzési módszerekre, melyek bizonyítják a rendszer helyes működését (verifikáció). Erre adnak lehetőséget a formális módszerek. A verifikáció egyik elterjedt módja a modellellenőrzés, amely a rendszer egy megfelelő modelljén hajt végre matematikai precizitású, teljes körű vizsgálatot.

Egyik modellellenőrzéssel vizsgálható tulajdonság az úgynevezett elérhetőségi probléma, amely azt vizsgálja, hogy a modell eljuthat-e egy meghatározott állapotba. A modellellenőrzést nehezíti, hogy akár végtelen sok állapota is lehet a modellnek.

Dolgozatomban egy verifikációs eljárásokra alkalmas modellező nyelv, a Petri-hálók elérhetőségi problémáját eldöntő algoritmusokkal foglalkoztam.

Korábbi munkáinkban foglalkoztunk egy ilyen megoldással, a Petri-hálók alkalmazott CEGAR módszerrel.

Munkám során megvizsgáltam a CEGAR hiányosságait, továbbá megvizsgáltam egy új megközelítést, ami a problémák egy eltérő körére teljesít jól. Elkészítettem az új megközelítés implementációját és összevetettem a két megközelítés hatékonyságát különböző típusú modellek esetén mérések segítségével.

Letölthető fájlok

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