Absztrakcióval támogatott hierarchikus keresési stratégiák a modellellenőrzés támogatására

Az informatika sok területén fontos a hibák elkerülése, a helyes működés garantálása. A hibák megtalálásának elterjedt módszere a tesztelés, a helyesség ellenőrzésének pedig a formális verifikáció. A szoftver rendszerek formális verifikációja nehéz feladat a problémák magas algoritmikus komplexitása miatt. Gyakran az állapottér exponenciálisan nő a probléma méretében, vagy akár az állapotok száma végtelen is lehet. Ilyenkor absztrakciót érdemes használnunk, amely során egy kisebb méretű, véges reprezentációján dolgozunk az állapottérnek. Az ellenpélda alapú absztrakció finomítás (CEGAR) módszere is egy absztrakció alapú technika, amely során az absztrakciót állapottérbejárások és keresések során finomítjuk, vagy ha nem szükséges már finomítani, akkor sikeresen bizonyítottuk a rendszer biztonságosságát. A módszer hatékonysága erősen függ az alkalmazott absztrakcióktól és keresési stratégiáktól.

A CEGAR algoritmusban az irodalomban alkalmaztak már mélységi és szélességi bejárást is a keresések során, azonban a keresést minden új absztrakciós fázisban lényegében újrakezdjük. Ez pazarló, hiszen a korábbi bejárások eredményeit elveszítjük így. Az új megközelítés alap gondolata az, hogy felhasználva a korábbi bejárások eredményeit, követve az absztrakció finomítás által definiált relációt, megpróbáljuk az újonnan felmerült absztrakt állapotok felé irányítani a keresést. A keresés során tekintettel kell lenni, hogy az absztrakt állapottér reprezentációban többféle szemantikájú él szerepel.

Munkám során kidolgoztam egy hierarchikus keresési stratégiát, amely hatékonyan eltárolja a korábbi fázisok eredményeit, majd ezt felhasználva hatékonyan vágja a keresési teret a rákövetkező keresések során. A kidolgozott algoritmust implementáltam a nyílt forráskódú Theta formális verifikációs keretrendszerbe és mérésekkel vizsgáltam a módszer alkalmazhatóságát.

szerző

Vörös Asztrik
Villamosmérnöki szak, alapképzés
alapképzés (BA/BSc)

konzulensek

Dr. Vörös András
egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék
Dr. Molnár Vince
Adjunktus, Méréstechnika és Információs Rendszerek Tanszék