Nagyméretű aszinkron rendszerek korlátos modellellenőrzése

Napjainkban elterjedtek az olyan elosztott, komplex rendszerek, melyeket jellemzően nehéz verifikálni. A csoportunkban folyó kutatások ezt a területet célozzák meg, amely során egy jól használható, hatékony modellellenőrző eszköz megalkotása a célunk. Az eszköz fejlesztése már elkezdődött, és idén már több TDK dolgozat témáját is szolgáltatta.

Az eddig elkészült modellellenőrző modul képes volt nagy állapottereken modellellenőrzést végezni, azonban mivel struktúrális modellellenőrző algoritmusok kerültek megvalósításra, a temporális logikai kifejezések teljesülését tudtuk csak vizsgálni, a feltételek nem teljesülése esetén nem kaptunk ellenpéldát. A széles körben való használhatóság azonban megkövetelné ezt.

Az önálló labor során a hallgató feladata az aszinkron rendszerek korlátos modellellenőrzésének vizsgálata lesz, majd a kiválasztott algoritmusok implementálása a PetriDotNet keretrendszerbe.

A témát olyan diákok számára ajánljuk, akik érdeklődnek az algoritmusok iránt, továbbá akiknek nem okoz gondot komplex algoritmusok implementálása sem.

A téma során a hallgató betekintést nyer a legújabb rendszerverifikációs algoritmusokba, elsajátítja a formális módszerek használatát, továbbá megismerkedhet egy összetett modellellenőrző keretrendszer működésével.

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: 
C#
Előismeretek: 
algoritmusok, programozás
Állapot: 
Folyamatban