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

Jelleg: 
Elméleti és gyakorlati
Konzulens: 
Vörös András
TDK lehetőség: 
TDK lehetőség
Megismerhető technológiák: 
.Net, modellellenőrzés, C#
Előismeretek: 
algoritmusok szeretete
Állapot: 
Folyamatban