Részleges rendezéses redukció alkalmazása 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 a folyamatok egymástól független lépéseinek teljes sorrendezése, vagyis az összes lehetséges sorrend egyedi vizsgálata, miközben azok a magas szintű modellben csak részlegesen rendezettek. A részleges rendezéses redukció célja az ilyen helyzetek kezelése egyetlen reprezentatív sorrend vizsgálatával. A technika alkalmazásával az állapottér mérete drasztikusan csökkenthető, miközben a vizsgált tulajdonságok megtarthatók.

A hallgató feladata a részleges rendezéses redukció ismert módszereinek megismerése és vizsgálata, illetve egy kiválasztott megoldás implementálása egy egyszerű (parancssoros) modellellenőrző eszközben. Az eszköznek Petri-hálókon kell elérhetőségi kérdéseket megválaszolnia, részleges rendezéses redukció alkalmazásával gyorsítva a számítást. Teljesítmény okokból javasolt programozási nyelv a C++.