Igényvezérelt heurisztikaszámítás informált kereséssel támogatott absztrakció alapú modellellenőrzésben
A modellellenőrzés módszere alkalmas arra, hogy automatizáltan bizonyítsuk a helyességét egy számítógépes alkalmazásnak, vagy megtaláljuk annak hibáit. A modellellenőrzés lényege a lehetséges hibaállapotok megkeresése a rendszer állapotterében, egy intelligens keresés segítségével.
Az állapottér mérete gyakran a program/rendszer leírásának méretében exponenciálisan nő, vagy akár végtelen is lehet összetett adat esetén. Egy hatékony megoldás a keresési feladat komplexitásának csökkentésére az absztrakció: az eredetileg vizsgált rendszer viselkedését konzervatívan közelítjük egy absztrakt modell létrehozásával. Az Ellenpélda vezérelt absztrakció finomítás (CEGAR) egy absztrakció alapú módszer, amely iteratívan finomítja az absztrakciót a modellellenőrzés során, amíg el nem jut a helyesség bizonyításáig vagy egy valódi ellenpélda megtalálásáig. Ennek a módszernek a hatékonysága nagyban függ az alkalmazott absztrakcióktól és az állapottér bejárása során alkalmazott keresési stratégiáktól.
Egyes területeken gyakran nem csak a helyességről alkotott ítélet, hanem egy ellenpélda is a modellellenőrzés kimenete, ha a követelmény sérül. Az ellenpélda segítségként tud szolgálni szoftveres hibakereséskor vagy rendszerterv javítása során. Azonban elengedhetetlen, hogy az ellenpélda a probléma valós gyökerére mutasson rá, ezért az ellenőrzést végző mérnökök számára legkisebb méretű ellenpélda szükséges.
A CEGAR algoritmusok szakirodalmában találhatunk példát mélységi és szélességi keresés alkalmazására, illetve számos más prioritás alapú stratégiára, melyek a modell előzetes elemzésén alapulnak. Viszont a keresés az absztrakciós séma minden iterációja során újraindul, így elveszítjük az előző keresések eredményeit, ami a jelenlegi keresésben sok többlet számítást okoz.
Korábbi kutatásom során a korábbi iterációkban található információk későbbi iterációkban történő felhasználását dolgoztam ki az úgynevezett Hierarchikus A* algoritmus keretében, mely ezen információkat használja ki, illetve bizonyítottam, hogy a legrövidebb ellenpéldát fogja biztosítani. Az algoritmusnak több változatát is kidolgoztam, melyek az A* heurisztika pontosságában és számítási igényében térnek el. Ezen változatokban azonban még maradtak kiaknázatlan optimalizációs lehetőségek.
Ezen munka során a már elkészült heurisztika számítási módszerek kerülnek kiegészítésre a Teljesen igény szerint történő Hierarchikus A* változat kidolgozásával és annak helyességbizonyításával. A már kidolgozott Igény szerinti változat hátránya, hogy nem veszi figyelembe a többi kifejtésre jelölt, ismert heurisztikával rendelkező csúcsnak a heurisztikáját, ami lehetőséget adna arra, hogy a korábbi iterációkban történő kereséseket megszakítsuk, amint annak során bebizonyosodik, hogy a legközelebbi hibás állapot távolságértéke nagyobb lesz egy, a jelenlegi iterációban ismert heurisztikával szemben. A Teljesen igény szerinti változat prototípus változatát implementálom a nyílt forráskódú Theta modellellenőrző-keretrendszerbe, illetve annak hatékonyságát szoftverek és mérnöki modellek verifikálásának benchmarkolásával kiértékelem, összehasonlítva a Thetában megtalálható keresési stratégiákkal, illetve a korábbi Hierarchikus A* változatokkal.
szerző
-
Vörös Asztrik
Mérnök informatikus szak, alapképzés
alapképzés (BA/BSc)
konzulens
-
Szekeres Dániel
Doktorandusz, Méréstechnika és Információs Rendszerek Tanszék
