Részleges rendezés redukció többszálú programok absztrakcióalapú formális verifikációjának támogatásához

A többmagos processzorok biztonságkritikus rendszerekben történő térhódításának köszönhetően egyre gyakrabban használnak többszálú programokat ilyen rendszerekben is, hiszen így lehet legjobban kiaknázni a párhuzamos számítás előnyeit. A szoftververifikáció komplexitása új szintre emelkedik a párhuzamosság megjelenésével a szálak nagyszámú lehetséges átlapolódása miatt. A komplexitásnövekedés eredménye, hogy a megfelelő tesztlefedettség elérése még nagyobb kihívást jelent, a naiv verifikációs technikák pedig gyakorlatilag használhatatlanná válnak. A részleges rendezés redukció (POR) hatékony modellellenőrzési megközelítés a párhuzamosság kezelésére. Az ellenpéldaalapú absztrakciófinomítás (CEGAR) pedig eredményes absztrakción alapuló technika állapot térben történő elérhetőségvizsgálatra.

A részleges rendezés alapú redukció aktívan kutatott területe az utóbbi évtizedeknek. Számos algoritmust publikáltak azzal a céllal, hogy minél nagyobb redukció által minél jobb teljesítményt érjenek el. Jelen dolgozatomban bemutatok néhányat a terület legmeghatározóbb algoritmusai közül. Ugyanakkor ezek a módszerek többnyire egy egyszerű állapottér bejárásra építenek csupán, ami korlátozza a további optimalizálási lehetőségeket.

Munkámban új megközelítését mutatom be a dinamikus POR technikák absztrakcióalapú verifikációba történő integrálásának. Az új módszer egy program utasításai között épített függőségi reláció számítása során az aktuálisan alkalmazott absztrakciót leíró információt is felhasználja. Ha két utasítás közti összefüggőség forrása el van absztrahálva, nyugodtan tekinthetjük ezt a két utasítást függetlennek. A modellbeli összefüggőség mértékének csökkenésével a POR nagyobb redukciót képes elérni. A CEGAR technikákat többféle módon is optimalizálhatjuk, például lusta kiértékeléssel. Dolgozatomban kitérek arra is, hogyan lehet a bemutatott absztrakciót figyelembe vevő POR algoritmust az állapottér lusta kiértékelésű számításával kombinálni. Végül kiértékelem a prezentált algoritmusok teljesítményét.

szerző

• 
  Telbisz Csanád Ferenc
  Mérnök informatikus szak, alapképzés
  alapképzés (BA/BSc)

konzulensek

• 
  Bajczi Levente
  PhD student, Méréstechnika és Információs Rendszerek Tanszék
  
• 
  Szekeres Dániel
  Doktorandusz, Méréstechnika és Információs Rendszerek Tanszék
• 
  Dr. Vörös András
  egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék

helyezés