Absztrakciós módszerek a modellellenőrzésben

Napjaink szoftver és hardver rendszerei összetettségükből következően nehezen vizsgálhatóak. A modellellenőrzés egy elterjedt technika ezen rendszerek vizsgálatára, azonban a nagy vagy végtelen állapottér sokszor meghiúsítja az algoritmusok futását.

A kompexitásbeli problémák hatékony kezelésére elterjedt technika az automatikus absztrakciós módszerek alkalmazása, amely egy elterjedt technika az ipari alkalmazásokban is (lásd Microsof SLAM project vagy Linux driver verification).

A hallgató feladata áttekinteni az irodalmat, és egy kiválasztott algoritmust megvizsgálni és implementálni a PetriDotNet keretrendszerbe. Megfelelően gyors algoritmus esetén lehetőség van nemzetközi megmérettetésen való részvételre is (Model Checking Contest).

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