Absztrakció alapú technikák CHC problémák hatékony megoldására
A biztonságkritikus rendszerek szoftveres komponensei egyre komplexebbek. Egy biztonságkritikus rendszerben fellépő hiba hatalmas gazdasági veszteségekkel, környezeti károkkal vagy akár életvesztéssel járhat, emiatt az ilyen rendszerek helyességét biztosítani kell. Hagyományos tesztelési technikák nem tudnak kimerítőek lenni, így más módszerekre van szükség. A formális verifikáció matematikailag precíz bizonyítékot vagy cáfolatot tud előállítani a program biztonsági tulajdonságairól, mint például a hibaállapot elérhetősége.
A formális verifikáció programok formális modelljein működik, ezen formalizmusok egyike a Control Flow Automaton (CFA). Ez egy gráfszerű reprezentációja a programoknak, amelyben a hibahelyek a gráf adott csomópontjaiként jelennek meg, melyek elérhetetlenségét kell bizonyítani. Egy másik széleskörűen használt köztes nyelv a verifikációs folyamatokban a Constrained Horn Clauses (CHCs). Ezek a programokat és kívánt tulajdonságaikat az elsőrendű logikai formulák egy jól definiált részhalmazában írják le változókkal és nem-interpretált függvényekkel. Ebben a reprezentációban a helyesség kérdése a formulák kielégíthetőségeként jelenik meg, melyet a logikai formulák kielégíthetőségének eldöntésére tervezett SMT megoldók tudnak meghatározni.
A hibaállapotok elérhetőségének megítélésére CFA-ban egy elterjedt megoldás a CHC-re való konverziójuk, melyben SMT megoldók segítségével lehet kielégítő hozzárendelést találni. Ezen feladat azonban nehéznek bizonyul az SMT megoldók számára, köszönhetően az exponenciális számú lehetséges értékadásnak a változók számához viszonyítva. Ebben a munkában egy fordított megközelítés, a CHC megoldásának CFA-vá transzformált verziójában való keresése kerül bemutatásra. Ezen reprezentációban ugyanis elérhetővé válnak absztrakció-finomítás alapú modellellenőrzési algoritmusok, melyek absztrakció segítségével csökkentik a lehetséges értékadások terét, ezzel potenciálisan jelentős hatékonyságnövelést érve el a hagyományos CHC megoldási technikákhoz képest. A megközelítés szintetikus és ipari példákon is kiértékelésre kerül.
szerző
-
Somorjai Márk István
Mérnök informatikus szak, alapképzés
alapképzés (BA/BSc)
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
helyezés
Knorr-Bremse VJRH Kft I. helyezett