Korszerű modellellenőrző eszközök felmérése (2 fő)

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. Napjainkban a modellellenőrzés már számos eszközben elérhető, hatékony stratégiákat és optimalizációkat dolgoztak ki hozzá. Az elérhető eszközök köre igencsak széles, ám ezek nagyban különböznek képességeik, illetve bemeneti modellek és specifikációs nyelvek terén. Ugyancsak probléma, hogy az egyes eszközök összehasonlítása jellemzően csak publikálásukkor történik meg, természetes módon torzítva az eredményeket az éppen publikált megoldás javára.

A hallgató feladata modellellenőrző eszközök és azok funkcióinak megismerése és kategorizálása, majd az arra érdemesek szisztematikus összehasonlítása. Ehhez ki kell dolgozni egy mérési környezetet, fel kell mérni az ellenőrzők tulajdonságainak vizsgálatához rendelkezésre álló modell készleteket (benchmark készleteket), illetve adott esetben ki kell dolgozni az egyes bemeneti modellek közötti konverziókat.

A hosszabb távon megszerezhető kompetenciák közül az egyik leghasznosabb az eszközök ismeretéből adódó know-how, ami az iparban (elsősorban biztonságkritikus beágyazott alkalmazások fejlesztésének területén) mind értékesebbnek számít.

Jelleg: 
Elméleti és gyakorlati
Konzulens: 
Molnár Vince
Konzulens: 
Darvas Dániel
TDK lehetőség: 
TDK lehetőség
Megismerhető technológiák: 
modellellenőrzés, modellezés
Előismeretek: 
szkript nyelvek
Állapot: 
Folyamatban