Fordító optimalizációk szoftver verifikációhoz

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 olyen 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 (konstant 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. Az optimalizációk hatékonyságát és hatását mérésekkel demonstrálom.

szerző

• 
  Sallai Gyula
  Mérnök informatikus szak, alapképzés
  alapképzés (BA/BSc)

konzulensek

• 
  Tóth Tamás
  tudományos segédmunkatárs, Mesterséges Intelligencia és Rendszertervezés Tanszék
  totht@mit.bme.hu
• 
  Dr. Hajdu Ákos
  Software engineer, Meta (külső)

helyezés