Petri-hálók CEGAR alapú vizsgálatának kiterjesztése

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

Napjainkban a formális verifikáció a hibamentesség igazolásának egyre gyakrabban alkalmazott módszere, különösen a biztonságkritikus rendszerek területén, ahol matematikailag precíz módon kell bizonyítani a specifikációnak való megfelelést és a hibátlan működést. A formális módszerek nagy hátránya azonban a nem triviális méretű problémáknál fellépő, gyakran hatalmas számítási igényük. Ez a probléma az egyik legfontosabb formális verifikációs módszernél, az elérhetőségi analízisnél is előjön: egészen kicsi modelleknek is lehet óriási, vagy akár végtelen nagy állapottere. Ezen probléma leküzdésére mindig újabb és hatékonyabb algoritmusokra van szükség, hiszen a módszerek fejlődésével párhuzamosan a megoldandó problémák komplexitása is egyre nő. Az egyik ilyen algoritmus az úgynevezett ellenpélda-alapú absztrakció finomítás (CEGAR) módszerét alkalmazza. Lényege, hogy az eredeti modell egy absztrakcióján dolgozik, és igény esetén finomítja az absztrakciót az állapottér bejárása során szerzett információk alapján. Az absztrakt modell állapotterének reprezentációja általában egyszerűbb, mint az eredeti modellé volt, így az absztrakt probléma könnyebben megoldható.

Szakdolgozatomban egy, a közelmúltban publikált algoritmust vizsgálok, amely az ellenpélda-alapú absztrakció finomítást a Petri-hálók elérhetőségi analízisére alkalmazza. Megmutatom, hogy bizonyos speciális esetekben az algoritmus helytelen eredményt adhat, és számos ellenpéldát mutatok be az algoritmus teljességére. Szakdolgozatomban új fejlesztéseket dolgozok ki, amelyek biztosítják az algoritmus helyességét és szélesítik az eldönthető problémák körét. Az algoritmust és az új fejlesztéseket implementáltam, dolgozatomban mérésekkel vizsgálom meg a kidolgozott új eljárások teljesítményét.

Letölthető fájlok

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