Verifikációs fordító fejlesztése C programokhoz

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

Ahogy a beágyazott rendszerek egyre inkább életünk szerves részévé válnak, biztonságos és hibamentes működésük egyre kritikusabb a felhasználók és a gyártók számára egyaránt. A tesztelési módszerekkel ellentétben a formális verifikációs technikák nem csak a hibák jelenlétét, hanem hiányát is képesek bizonyítani, ezáltal kiváló eszközzé téve őket biztonságkritikus rendszerek verifikációjához. Ennek egy módja a már elkészült forráskód formális modellé alakítása és a modell ellenőrzése a hibás állapotok bekövetkezhetősége szempontjából.

Sajnos a forráskódból formális modellt előállító eszközök gyakran állítanak elő kezelhetetlenül nagy és komplex modelleket, így téve ellenőrzésüket rendkívül bonyolulttá és időigényessé. Munkámban bemutatok egy olyan komplex folyamatot, amely képes forráskódból formális modellt előállítani. A folyamat részeként fordítótervezésben gyakran használt optimalizációs algoritmusokat (konstans propagálás, halott kódrészletek törlése, ciklus kihajtogatás, függvények ,,inline''-olása) alkalmazok a bemeneten, illetve egy program szelető algoritmus segítségével több egyszerűsített modellt állítok elő egy nagy probléma helyett. A munkafolyamat végén egy korlátos modellellenőrző és egy k-indukciós algoritmus segítségével verifikálom a kapott részproblémákat. Az optimalizációk hatékonyságát és hatását mérésekkel demonstrálom.

Letölthető fájlok

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