Informált keresési stratégiák 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, ami 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.

Ezen munka célja, hogy az absztraktabb állapottérben található információt kihasználva a finomabb állapottér bejárásakor javítsunk a CEGAR alapú modellellenőrző algoritmusokon, mindeközben az ellenpélda méretének minimalizálását is biztosítva.

A fő kontribúciónk az újszerű Hierarchikus A* algoritmus, ami egy - a CEGAR hurkon belül található - intelligens keresési stratégia. Az algoritmus a jelenlegi absztrakt állapottér A* alapú bejárásához az előző absztrakciókat felhasználva számít egy heurisztikát. A javasolt algoritmus több különböző változatának kiértékeljük a hatékonyságát, és összehasonlítjuk azokat a rendszerint használt keresési stratégiákkal. A méréseket a nyílt forráskódú Theta modellellenőrző-keretrendszerbe beépített prototípus implementációnkon hajtjuk végre.

szerző

• 
  Vörös Asztrik
  Mérnök informatikus szak, alapképzés
  alapképzés (BA/BSc)

konzulensek

• 
  Szekeres Dániel
  Doktorandusz, Méréstechnika és Információs Rendszerek Tanszék
• 
  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

helyezés