Inkrementális, induktív algoritmusok szoftver-modellellenőrzéshez
Egyre nagyobb szerepet kapnak az életünkben a különböző szoftvereszközök. Ma már olyan, biztonságkritikus alkalmazási területeken is elterjedten alkalmaznak szoftvereket, ahol egy esetleges meghibásodás végzetes következményekkel is járhat: szoftverhibák hatására vagyonok úszhatnak el, repülőgépek zuhanhatnak le, atomerőművek állhatnak le. Az ilyen, kritikus szoftverek helyességének biztosítása tehát kiemelten fontos feladat.
Szoftverek megfelelő működésének ellenőrzése a verifikáció során történik. Kritikus szoftverek ellenőrzésére gyakran alkalmaznak formális módszereket, melyekkel - ellentétben a hagyományos ellnőrzési módszerekkel (pl. tesztelés) - nemcsak hibák jelenléte mutatható ki, hanem akár a rendszer helyessége is bizonyítható. Az egyik legelterjedtebben alkalmazott formális módszer a modellellenőrzés, ahol a szoftver állapotterének bejárásával próbáljuk a vele szemben megfogalmazott formális követelmények teljesülését bizonyítani, vagy éppen cáfolni.
Az IC3 egy korszerű, eredetileg hardvermodellek ellenőrzésére alkalmas modellellenőrző algoritmus. Az IC3 algoritmus egyedi jellemzője, hogy a rendszer helyességének ellenőrzését inkrementálisan, számos egyszerű lemma indukciós bizonyításán keresztül végzi. Amennyiben a rendszer helyes, a felfedezett lemmák összessége a rendszer helyességének bizonyítását (az állapottér biztonságos felülbecslését) adják; ellenkező esetben pedig a keresést egy ellenpélda irányába irányítják, ezáltal hatékonyan vezérelve az állapottérfelderítést. Az eredeti algoritmus hátránya, hogy elsősorban véges állapotterű rendszerek (pl. sorrendi hálózatok) hatékony kezelését teszi lehetővé. Az algoritmus így jelenleg is aktív kutatás tárgyát képezi, és számos kiterjesztéssel bír.
Dolgozatomban az algoritmusnak két ismert kiterjesztését kombinálom, így lehetővé téve szoftverek hatékony modellellenőrzését.
1) A végtelen állapottér hatékony kezeléséhez (implicit) predikátumabsztrakciót használok. Ez a módszer a végtelen állapotteret véges sok partícióra osztja fel a változókon értelmezett logikai állítások (predikátumok) mentén. A partíciók mentén egy véges absztrakt állapottér jön létre, melynek állapotait az határozza meg, hogy a predikátumok közül melyik teljesül, melyik nem. A futás során az algoritmus új predikátumokat tanul, ezzel szükség szerint pontosítja a képét a rendszerről, mégis megtartja az absztrakció általánosságát.
2) A program vezérlési szerkezetében rejlő többletinformáció kihasználásához az absztrakciót az eredeti, minden utat egyszerre vizsgáló eljárás helyett a vezérlési gráf kihajtogatásával, elérhetőségi fa építésével oldom meg. Az így létrejövő absztrakció lokális, a vezérlés adott pontjaira vonatkozik, ami hatékony helyességbizonyítást tesz lehetővé a program egyes ágaira vonatkozólag.
A kombinált algoritmus különböző konfigurációinak hatékonyságát mérésekkel vizsgálom.
Az algoritmusok implementációját a Theta nyílt forráskódú modellellenőrző keretrendszer moduljaként készítem el, ami további kiterjesztési lehetőségeket biztosít.
