Időzített rendszerek ellenőrzése

A tanszéken fejlesztett PetriDotNet keretrendszer (http://petridotnet.inf.mit.bme.hu/) hatékony alanízist biztosít diszkrét aszinkron rendszerekhez. Azonban elsősorban a biztonságkritikus, beágyazott rendszerek esetén fontos feladat a időzítési tulajdonságok modellezése és ellenőrzése.

Időzített modellek ellenőrzése azonban nem egyszerű, mert az idő (változók) folytonos jellege miatt absztrakciót kell alkalmazni, emellett az absztrakt állapottér is hatalmas, emiatt hatékony algoritmusokra van szükség.

A tanszéken évek óta fejlesztünk különböző szimbolikus állapottér bejáró és tároló algoritmusokat (lásd: http://petridotnet.inf.mit.bme.hu/publications/), a jelentkező feladat megismerni ezeket, és továbbfejleszteni őket úgy, hogy időzített rendszerek vizsgálatára is alkalmassá váljanak!

A munka során új algoritmusok kifejlesztésére van lehetőség, amelyek implementálásra kerülnek a tanszéki modellező és modellellenőrző keretrendszerünkben.

Témacsoport: 
Ellenőrzés és tesztelés
Konzulens: 
Vörös András
TDK lehetőség: 
TDK lehetőség
Megismerhető technológiák: 
.Net algoritmusok
Előismeretek: 
.Net
Állapot: 
Folyamatban