Modellek viselkedésének ellenőrzésére jól bevált módszer az ún. modellellenőrzés.
Ennek során a rendszermodell lehetséges viselkedéseit kimerítő módon és automatikusan elemzik, illetve temporális logikák segítségével megfogalmazott követelmények teljesülését vizsgálják rajtuk. Számos algoritmus és technika született a probléma hatékony megoldására. A megoldások különböznek a megcélzott logikákban, az állapottér kezelésében (explicit és szimbolikus modellellenőrzés), illetve a feladat egyszerűsítését célzó különböző redukciókban (absztrakció, részleges rendezés, szimmetria-redukció).
A kutatás célja a különböző módszerek sajátosságainak feltérképezése és összehasonlítása volt. A kutatás során számos kutatócsoporthoz és ellenőrző eszközhöz kapcsolódó publikáció és beszámoló került megvizsgálásra, ezek főbb jellegzetességei és működésük alapelvei a beszámolóban bemutatásra kerültek. A kutatás tanulsága szerint rengeteg nagyhatékonyságú modellellenőrző technika elérhető mind az egyes eszközökben, mind a kapcsolódó irodalomban, de ezek összekapcsolása nem triviális feladat. Az eszközfejlesztők és kutatók együttműködése komoly lehetőségeket rejt, az eszközök erősségeinek kombinálásával a megoldható problémák száma valószínűleg jelentősen nőhetne.
A kutatási beszámoló letölthető innen (PDF)
Molnár Vince, doktorandusz, Budapesti Műszaki Egyetem, molnarv@mit.bme.hu
2015. június 4.