Intervallum-alapú absztrakt interpretációs algoritmus fejlesztése invariáns tulajdonságok ellenőrzésére

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

Mindennapi életünket egyre jobban meghatározzák a szoftverrendszerek. Ezek sokszor biztonságkritikusak

(pl. autonóm járművek, erőművek), tehát helyes működésük garantálása

kiemelten fontos feladat. Ennek egyik eszköze a formális verifikáció, ami nemcsak hogy

képes megtalálni a hibákat, de akár be is tudja bizonyítani a szoftver helyességét. Sok algoritmus

létezik, amik különböző problémák esetén adnak megfelelő megoldást, de sokszor

a teljesen precíz analízis lehetetlen, ezért szükség van absztrakcióra.

Az absztrakció alapú interpretáció egy olyan technika, ami absztrakciós domaint hoz

létre a szoftver számára és azon végzi az analízist, amivel még mindig képes matematikailag

bizonyítani a rendszer helyességét. Az absztrakcióval ugyanis csak felülbecsűljük a rendszer

lehetséges állapotait, ha a hibás állapot még mindig nem elérhető akkor az a becslés előtt se

volt az. Előfordulhat viszont, hogy hibás jelzést adunk, vagyis azt mondjuk, hogy elérhető

hibás állapot, de ez valójában csak az absztrakció miatt lett elérhető. Az intervallum

absztrakció az absztrakciónak egy olyan típusa, ahol a domain intervallumokkal van leírva.

Munkám során létrehoztam egy könyvtárat az intervallum absztrakció domainjéhez.

A könyvtár az interpretációt Control Flow Automatákon végezi, ami egy formális model

a programkódokhoz. Csináltam egy keretrendszert, ami megvalósítja az absztrakciós interpretáció

analízist felhasználva ezt könyvtárat. A keretrendszer teljesítményének lehetséges

javítása érdekében implementáltam egy új megközelítést az intervallum leírására,

szín osztályok alkalmazásával. Továbbá készítettem néhány különböző algoritmust, különböző

widening taktikák felhasználásával. Szoftverrendszerek széles skáláján futtattam

a méréseimet, többek között ipari vezérlő (PLC) kódokon. Ezzel teszteltem a különböző

konfigurációkat és megvizsgáltam az előnyeiket és hátrányaikat.

Letölthető fájlok

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