Szaturáció alapú modellellenőrzés lineáris idejű tulajdonságokhoz

Napjainkban a legtöbb területen, így a biztonságkritikus rendszerek területén is egyre elterjedtebbek a beágyazott vezérlő és felügyelő eszközök. Egy biztonságkritikus rendszer hibája akár katasztrofális következményekhez is vezethet, így e beágyazott eszközök helyes működésének bizonyítása kiemelten fontos feladat. Formális módszerek használatával már a fejlesztési folyamat elején, tervezési időben, matematikai precizitással vizsgálható a rendszerek helyes működése. A modellellenőrzés az egyik leggyakrabban használt formális módszer, mert komplex kérdéseket képes vizsgálni és sok információt szolgáltat. A modellellenőrzés végrehajtása során a rendszer modelljén vizsgáljuk az ún. temporális logika segítségével megfogalmazott követelmények teljesülését. Többféle temporális logika létezik, ezek közül a lineáris idejű (LTL) és az elágazó idejű (CTL) temporális logika a legelterjedtebb. Kifejezőerejük nem összehasonlítható, azonban az LTL sokszor praktikusabb kompaktsága és átláthatósága miatt, ami a CTL-nél könnyebben használhatóvá teszi. Ennek azonban ára is van, az LTL modellellenőrzés komplexitása a PSPACE osztályba tartozik, tehát szükséges, hogy hatékony algoritmusokat alkalmazzunk.

A szaturáció egy szimbolikus iterációs algoritmus, amely hatékony állapottérfelderítésre és CTL modellellenőrzésre képes. Hatékonyságát egy speciális iterációs stratégiának és a szimbolikus, azaz tömören kódolt állapottárolásnak köszönheti. Szaturáció-alapú megoldások léteznek CTL modellellenőrzésre, azonban ezek nem használhatóak LTL modellellenőrzésre, annak eltérő karakterisztikája miatt. Szimbolikus algoritmusokat próbáltak már újabban LTL modellellenőrzésre használni, azonban a szaturációs algoritmust még senki sem alkalmazta sikerrel ezen a területen.

Dolgozatomban azt vizsgálom meg, miként lehetne a szaturációs algoritmust kiterjeszteni LTL modellellenőrzésre. Munkám eredménye egy olyan automataelméleti megközelítés, amelyet szaturációs alapokon valósítottam meg, így létrehozva egy új, hatékony modellellenőrző algoritmust.

Dolgozatomban bemutatom a szaturáció alapú lineáris idejű temporális logikán alapuló modellellenőrzés elméleti hátterét és az általam kifejlesztett új modellellenőrző algoritmust.

szerző

• 
  Molnár Vince Dr.
  mérnökinformatikus
  nappali

konzulensek

• 
  Dr. Vörös András
  egyetemi docens, Mesterséges Intelligencia és Rendszertervezés Tanszék
• 
  Dr. Bartha Tamás
  docens, Mesterséges Intelligencia és Rendszertervezés Tanszék

helyezés