Absztrakció-alapú interprocedurális szoftververifikáció
A technológiavezérelt világunkban egyre több feladat van automatizálva szoftver által. Szoftvert használunk üzenetek küldéséhez és fizetéshez, de manapság rábízzuk nukleáris erőművek működtetését és autók vezetését is. Az ilyen biztonságkritikus rendszerekben a szoftverbe vetett bizalom nem elegendő, mert egy fellépő hiba hatalmas gazdasági veszteséggel, környezeti károkkal vagy akár életvesztéssel is járhat. A biztonságkritikus rendszerek szoftverének helyességét tehát biztosítani kell. Bár a hagyományos tesztelési technikák tudnak példát mutatni a rendszer helytelen viselkedésére, a hibák hiányát nem tudják garantálni. A formális verifikáció ezzel szemben matematikai bizonyítást vagy cáfolatot tud adni a rendszer biztonsági tulajdonságairól.
A formális verifikációnak megvannak a saját kihívásai. Ahhoz, hogy egy program helyes legyen, az elérhető állapotai, azaz az a változók lehetséges értékei az elérhető vezérlési helyeken nem sérthetik meg a biztonsági kritériumot. A program állapoterének mérete azonban exponenciálisan nő a programváltozók számának függvényében, ami gyakorlatban lehetetlenné teszi az összes állapot ellenőrzését. Az állapotteret tovább növelik a szoftver minden területén megjelenő procedurák. Ezek struktúrálják és újrahasznosíthatóvá teszik a szoftvert, azonban megnehezítik a szoftver interprocedurális analízisét a végrehajtás folyamának megzavarásával és új változópéldányok generálásával a meghívási helyeiknél. Ezen felül a program állapotát a hívási veremmel egészítik ki, amely végtelen mély lehet rekurzív programok esetén, így egy végtelen nagy állapotteret eredményezve.
A hatalmas állapotterek problémáját tipikusan redukciós eljárásokkal kezelik formális szoftververifikációban. Az absztrakciós technikák az állapottér elemeit valamilyen információ elhagyásával csoportosítják absztrakt állapotokba, így egy redukált absztrakt állapotteret állítva elő. Hagyományosan az absztrakciót a változók értékeire alkalmazzák. A dolgozatomban az absztrakció kiterjesztését mutatom be hívási vermekre egy absztrakció-alapú modellellenőrző algoritmusban, az ellenpélda-alapú absztrakciófinomításban (CEGAR). A hívási verem részeinek elabsztrahálásával különböző hívási veremmel rendelkező, hasonló állapotok tovább csoportosíthatók, így csökkentve az absztrakt állapottér mértetét. Ez javítja a szoftverek interprocedurális verifikációjának hatékonyságát, különösképp rekurzív progamok esetén, ahol a hívási verem nagyobb mértékben járul hozzá az állapottér növekedéséhez. A bemutatott ötlet egy prototípusát a Theta modellellenőrző keretrendszerben implementálom, hatékonyságát pedig egy esettanulmányon értékelem ki.
szerző
-
Somorjai Márk István
Mérnök informatikus szak, mesterképzés
mesterképzés (MA/MSc)
konzulensek
-
Dobos-Kovács Mihály
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
