Natív pointer-támogatás absztrakció-alapú modellellenőrzésben
A biztonságkritikus rendszerek nagymértékben támaszkodnak szoftveres megoldásokra az elvárt működésük biztosítása érdekében. Ezen szoftveres megoldásoknak minden esetben megfelelően kell működniük, mivel meghibásodásuk veszélyes helyzetekhez vezethet. A rendszer tesztelésével találhatóak a szoftverben hibák; azonban a tesztelés nem kimerítő módszer, nem képes önmagában bizonyítani a szoftver hibamentességét. A formális verifikáció a szoftver lehetséges viselkedésformáinak kimerítő bejárására szolgáló technika, de a lehetséges állapotok nagy vagy akár végtelen száma megakadályozhatja a sikeres verifikációt.
A CEGAR (Counterexample Guided Abstraction Refinement) különböző absztrakciókat használ a komplex adatok kezelésére a szoftver verifikálásakor. A CEGAR számos felhasználási esetben bizonyította hatékonyságát. Eddig azonban nem volt hatékony pointer-támogatás.
A beágyazott rendszerekben használt programozási nyelvek gyakran erősen támaszkodnak pointerekre a hatékony memóriakezelés és adatmanipuláció érdekében. A pointerek használata azonban az indirekciók bevezetésével növeli a program bonyolultságát, ami nagyban megnehezíti az ilyen programok verifikációját. Annak ellenére, hogy a beágyazott és biztonságkritikus rendszerekben többnyire kerülik a pointerek használatát, valós programokban teljesítményi és funkcionalitási elvárások miatt mégis gyakran szükséges a használatuk.
A korábbi verifikációs megoldások a pointer-analízist a megoldó számára biztosított problémába kódolták. Célunk, hogy a problémát a verifikációs algoritmus szintjére emeljük: újszerű megoldásunk a CEGAR ciklus állapottér-bejárási részében próbálja megoldani a pointer analízis problémáját, lehetővé téve egy pontosabb, az absztrakció-alapú verifikáció által támogatott módszert. Kiértékeljük a javasolt módszer teljesítményét SV-COMP benchmarkokon, és célunk az SV-COMP 2023-as nevezés részeként szerepeltetni.
szerző
-
Sisák Botond Bendegúz
Mérnök informatikus szak, alapképzés
alapképzés (BA/BSc)
konzulensek
-
-
Dr. Vörös András
egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék
