CEGAR-alapú modellellenőrzés vizsgálata

OData támogatás
Konzulens:
Vörös András
Méréstechnika és Információs Rendszerek Tanszék

Napjainkban a formális verifikáció a hibamentesség és a specifikációnak való megfelelőség igazolásának egyre gyakrabban alkalmazott eszköze, különösen a biztonságkritikus rendszerek területén, ahol ezen tulajdonságok matematikailag precíz bizonyítására van szükség. A formális módszerek hátránya azonban a nagy számítási igényük. Ez az egyik legelterjedtebb formális verifikációs technikára, a modellellenőrzésre is igaz. A modellellenőrzés célja, hogy automatikusan bizonyítsa egy rendszer helyességét a lehetséges viselkedéseinek kimerítő (explicit vagy szimbolikus) vizsgálatával. Gyakran azonban kisméretű rendszerek is rendelkezhetnek kezelhetetlenül sok vagy akár végtelen számú viselkedéssel. Bár léteznek megoldások ezen probléma leküzdésére, a modellek komplexitásának növekedésével mindig újabb és hatékonyabb algoritmusokra van szükség.

Az ellenpélda-alapú absztrakció finomítás (Counterexample-Guided Abstraction Refinement, CEGAR) módszere egy gyakran alkalmazott technika az előbbi probléma leküzdésére. A CEGAR-alapú algoritmusok a rendszer modelljének egy absztrakcióján dolgoznak, amely kisebb számítási kapacitással is kezelhető. Egy elterjedt technika a lehetséges viselkedések felülbecslése a modell bizonyos kényszereinek egyszerűsítésével. Az absztrakció durvasága miatt azonban a modellellenőrzés eredménye pontatlan lehet. Ilyen esetekben az absztrakció finomítására van szükség. A CEGAR-alapú megközelítések általában egy durva absztrakcióval kezdenek, hogy minimalizálják a számítási igényüket és ezt finomítják addig, amíg el nem érik a pontos eredményt.

Diplomamunkámban megvizsgálom a tranzíciós rendszerek CEGAR-alapú modellellenőrzésének elméleti hátterét és a kapcsolódó szakirodalmat. A rendszerek és a velük kapcsolatos követelmények formalizálására bemutatom az elsőrendű- és temporális logikákat valamint megvizsgálok két konkrét CEGAR-alapú algoritmust, amely felülbecslésen alapszik. Emellett számos, a CEGAR hatékony megvalósítását lehetővé tevő technikát is bemutatok, többek között a SAT/SMT-megoldást, az interpolációt és a "lusta" absztrakciót. Ezen algoritmusok és technikák előnyeit ötvözve elkészítek egy új algoritmust. A bemutatott módszerek implementációját is elkészítettem annak érdekében, hogy kiértékelhessem és összehasonlíthassam a különböző technikák teljesítményét. A különféle modelleken elvégzett mérések elemzései rávilágítanak az algoritmusok előnyeire és hátrányaira.

Letölthető fájlok

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