Portfólió-alapú futásidejű technikák formális verifikációhoz

A formális verifikációs módszerek lényege a matematikailag precíz reprezentációk és algoritmusok használata programok és modellek tulajdonságainak ellenőrzésére. Térnyerésük, különösen a biztonságkritikus rendszerekben, folyamatosan erősödik. Ugyanakkor a formális módszerek magas számításigénye miatt sok, különböző területre szabott algoritmus létezik.

Az esetek többségében megfelelő algoritmus és konfiguráció választása egy adott problémára komoly szakmai tudást igényel (például annak kiválasztása, hogy milyen absztrakciós módszert állítsunk be). Még egy szakértőnek is gyakran több konfiguráció kipróbálására van szüksége ahhoz, hogy találjon egy, az adott problémán jól teljesítő beállítást. Ugyanakkor a verifikációra rendelkezésre álló idő és erőforrások az esetek többségében korlátozottak.

Munkám célja olyan technikák ajánlása, amelyek a rendelkezésre álló idő hatékonyabb kihasználását segítik. Felteszem, hogy adott egy konfigurálható, szekvenciálisan futtatható eszköz, egy bemeneti probléma és egy időkorlát. Olyan módszereket javaslok, amelyek dinamikusan választanak és változtatnak az éppen futtatott konfiguráción ezzel egy összetett portfóliót képezve. A módszer újdonságértéke, hogy nem csak a bemenetből kinyerhető, de futás közben gyűjtött információkat is használ, hogy beavatkozzon az algoritmusba vagy éppen új konfigurációra váltson.

A javasolt technikákat megvalósítottam a Theta keretrendszerben, C programok verifikálására fókuszálva. Az eszközt kiegészítettem egy, az algoritmus megakadását felismerni képes futásidejű funkcióval, illetve egy ehhez jól illeszkedő portfólióval, amely változatos konfigurációk közül választ, ezzel is növelve a siker esélyét.

A kiértékeléshez az International Competition on Software Verification (SV-COMP) verifikációs problémáinak egy részhalmaza került ellenőrzésre. Az SV-COMP egy széleskörűen elismert, de-facto standard C nyelvű programgyűjtemény, kifejezetten szoftver ellenőrző eszközök számára. A javasolt javításokat néhány, általában jól teljesítő konfiguráció mérési eredményeivel vetettem össze, melyeket egyesével, illetve naiv szekvenciális portfólióban is futtattam. A mérési eredmények megmutatták, hogy az eszköz a hozzáadott technikákkal több feladatot képes megoldani, ráadásul lényegesen kevesebb idő alatt, mint a többi esetben.

Összefoglalva, munkám során olyan megközelítéseket dolgoztam ki, amelyek a hatékony verifikációt segítik a konfiguráció és algoritmus szakértői tudást igénylő kiválasztásának automatizálásával. Eredményeim bármely verifikációs keretrendszer fejlesztőjének segítséget nyújthatnak. A kiértékeléshez egy konkrét eszközön el is végeztem a módszerek megvalósítását, megmutatva, hogy milyen módon lehetséges ezek segítségével a teljesítmény javítása.

szerző

• 
  Ádám Zsófia
  Mérnök informatikus szak, alapképzés
  alapképzés (BA/BSc)

konzulens

• 
  Dr. Micskei Zoltán
  egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék

helyezés