Bejárási stratégiák és adatszerkezetek vizsgálata szimbolikus modellellenőrzésben

Biztonságkritikus rendszerekben gyakran szükséges a működés helyességének formális ellenőrzése. Az automatikus ellenőrzésre jól használható megoldásnak bizonyult az ún. modellellenőrzés, melynek során a rendszermodell lehetséges működéseit kimerítően vizsgáljuk. Aszinkron, konkurens rendszerek vizsgálatakor gyakori probléma az ún. állapottér-robbanás, amikor a rendszer lehetséges állapotainak száma már kevés komponens esetén is óriásira nőhet. Ennek gyakori oka, hogy a rendszer sok, nagy értékkészletű változóval dolgozik, rendkívül sok elérhető kombinációt és nagyméretű állapotleírókat eredményezve. A szimbolikus modellellenőrzés célja az ilyen helyzetek kezelése a hasonló állapotok kompakt tárolásával. Ehhez gyakran használnak ún. döntési diagramokat, amik az állapottér egyfajta tömörítéseként is felfoghatók. Az ezeken közvetlenül működő algoritmusok gyakran hatalmas állapottereket is képesek hatékonyan kezelni és tárolni.

A hallgató feladata a döntési diagramok és hozzájuk tartozó modellellenőrzési stratégiák megismerése és vizsgálata, illetve a szélességi típusú bejárási stratégia implementálása a tanszéken fejlesztett PetriDotNet keretrendszerben. Az implementációhoz a hallgatónak tanulmányoznia kell az algoritmus által használt hatékony adatszerkezeteket is, úgymint a többértékű döntési diagramokat (Multi-value Decision Diagram, MDD), illetve az állapotátmeneti szabályok hatékony reprezentációit.