Szaturáció alapú Lineáris Temporális Logikai modellellenőrzés

Napjainkban a beágyazott és ezen belül is a biztonságkritikus rendszerek tervezésénél egyre nagyobb szerepet kapnak a különböző formális módszereken alapuló technikák. Legnagyobb előnyük, hogy már a tervezés kezdeti fázisától lehetővé teszik a rendszer helyes működésének vizsgálatát. Ilyen ellenőrzési technika a modellellenőrzés, amely során a modell állapotterének bejárása során győződünk meg a temporális logikai formában adott specifikáció teljesüléséről. Sajnos akár kis modelleknek is hatalmas állapottere lehet: az állapottér robbanás problémája miatt hatékony algoritmusokra van szükség. Erre nyújt megoldást aszinkron rendszerek esetén a szaturáció alapú állapottér bejárás és modellellenőrzés.
Korábbi munkák bemutattak már szaturációs alapon működő lineáris idejű temporális logikai (LTL) specifikációs nyelvet támogató modellellenőrzőket. A hallgató feladata megvizsgálni a korábbi megvalósításokat, áttekinteni a vonatkozó szakirodalmat, és ez alapján továbbfejleszteni a tanszéki fejlesztésű PetriDotNet keretrendszerben található meglévő algoritmusokat.