Kombinált explicit és implicit állapottér felderítő és modellellenőrző algoritmusok fejlesztése, implementálása

A mai nagyméretű szoftver és hardver rendeszerek esetében sokszor a különböző modellellenőrző algoritmusok nem elég hatékonyak önmagukban. Ilyenkor a már meglévő módszerek kombinálása eredményre vezethet.

A részleges rendezés egy speciális algoritmus, amely egy redukált állapotgráfot jár be, ezáltal csökkentve probléma komplexitását.

A szimbolikus módszerek, mint a PetriDotNet keretrendszerbe implementált szaturációs algoritmus is egy speciális kódolást használ az állapottér méretének csökkentésére.

A két módszer ötvözése kézenfekvő lehet olyan nagyméretű rendszerek esetén, amelyek verifikációja során a módszerek külön-külön korlátokba ütköznek. Korábbi kutatások alapján a módszer kiaknázza és ötvözi a különböző algoritmusok előnyeit. A munka során a hallgató olyan új algoritmust hoz létre, amely túlmutat a jelenleg elérhető eredményeken, másrészt jó lehetőség egyéb ötletek kipróbálására is, gráfbejárások és állapottérredukció területén. A feladatot kifejezetten ajánljuk TDK-zni vágyó hallgatóknak, de a téma nagysága miatt akár az MSc végéig is elvihető.

Az érdeklődő hallgatónak ajánljuk, hogy látogassa meg a keretrendszer honlapját, ahol az eddig elkészült eszköz letölthető, kipróbálható: https://www.inf.mit.bme.hu/research/tools/petridotnet