Az LTSmin modellellenőrző vizsgálata és kiterjesztése

Biztonságkritikus rendszerekben gyakran szükséges a működés helyességének formális bizonyítása. 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. Az  LTSmin (http://fmt.cs.utwente.nl/tools/ltsmin/) a Twente-i Egyetemen fejlesztett modellellenőrző eszköz. Segítségével változatos bemeneti modellek ellenőrzése végezhető el, számos (párhuzamosított) algoritmus segítségével. Az algoritmusok és a modell szétválasztásáról a PINS (partitioned next-state interface) interfész gondoskodik.

A hallgató feladata az LTSmin modellellenőrző és a PINS interfész megismerése és kipróbálása. Ennek keretében létre kell hozni egy tesztkörnyezetet az egyes algoritmusok teljesítményének kiértékelésére, valamint a PINS interfész segítségével illeszteni kell a Petri háló modellformalizmust az LTSmin eszközbe.

A munkát a Twente-i Egyetemről is segítik, így lehetőség van külföldi egyetemmel történő kooperációra.