Inkrementális, induktív modellellenőrzés alkalmazása szoftverekre

OData támogatás
Konzulens:
Tóth Tamás
Méréstechnika és Információs Rendszerek Tanszék

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.

A szoftverek megfelelő működésének ellenőrzése a verifikációjuk 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ékát (az állapottér egy 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 IC3 algoritmusnak egy olyan kiterjesztését vizsgálom, amely a végtelen állapottér hatékony kezeléséhez (implicit) predikátumabsztrakciót használ. 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 egy véges absztrakt állapotteret hoznak létre, melynek állapotait az határozza meg, hogy mely predikátumok teljesülnek. 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. Annak érdekében, hogy az algoritmus alkalmas legyen programokat leíró vezérlésifolyam-automaták ellenőrzésére, egy olyan transzformációt is megadok, amely az automata alapján egy vele ekvivalens viselkedésű szimbolikus tranzíciós rendszert állít elő. Az algoritmust ezen a szimbolikus tranzíciós rendszeren futtatva lehetőség nyílik az automata helyességének ellenőrzésére.

Az algoritmus, illetve a transzformáció 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. Az implementált algoritmus különböző konfigurációinak hatékonyságát mérésekkel vizsgálom.

Letölthető fájlok

A témához tartozó fájlokat csak bejelentkezett felhasználók tölthetik le.