Futásidőbeli verifikáció kritikus beágyazott rendszerekben

Kritikus beágyazott rendszerekben a működés közben előforduló hibák (pl. processzorhibák, kommunikációs hibák) detektálása kiemelt feladat, hiszen ezek bekövetkezése esetén veszélyes állapot alakulhat ki, ami balesethez, kárhoz vezethet. A hibadetektálás futásidőbeli verifikációval valósítható meg, ez a helyes és biztonságos működés folyamatos ellenőrzését jelenti. Az ellenőrzés alapja a rendszer specifikációja, valamint (ha a beágyazott rendszerben futó alkalmazás fejlesztése modellvezérelten történik) az elkészített és ellenőrzött tervezői modell is referenciaként szolgálhat.

A hallgató feladata egy olyan keretrendszer kialakítása, amely illeszkedik a modell alapú fejlesztési paradigmához, így a formális specifikáció és a tervezés során használt rendszermodellek alapján valósítja meg a futásidőbeli verifikációhoz szükséges többlet funkciók (komponens és rendszer szintű önellenőrzés és monitorozás) automatikus generálását és konfigurálását.

A feladatban kihívást (és kutatási lehetőséget) jelent a különféle specifikációs formalizmusok (pl. időzített temporális logikák, kiterjesztett üzenet-szekvencia diagramok) támogatása, valamint az integráció a már elkészült modell alapú kódgenerálási keretrendszerrel.

A feladat szakdolgozatként és TDK munkaként is folytatható.