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.