témavezető: Majzik István
helyszín (magyar oldal): Méréstechnika és Információs Rendszerek Tanszék helyszín rövidítés: MIT
A kutatási téma leírása:
Az informatikai rendszerek egy jelentős részében merül fel az átkonfigurálhatóság és adaptivitás igénye, hogy kezelhetők legyenek a környezet és a felhasználói igények változásai valamint a bekövetkező hibák. Ezt kiszolgálják egyrészt tervezési idejű megoldások (pl. „product line” megközelítés és tervezési tér bejárás), másrészt futásidőbeli technológiák is (pl. dinamikus komponens integrációs keretrendszerek, intelligens adaptív algoritmusok, hibák öngyógyítása). Kritikus alkalmazások esetén mindinkább elvárás az, hogy a szolgáltatások helyessége (illetve legalább biztonságossága) a komponensek dinamikus átkonfigurálása és az adaptivitás mellett is biztosítható legyen. Ennek egyik lehetséges megoldása a formális módszereket alkalmazó verifikáció: modellek biztosítják a tervek egyértelmű rögzítését valamint a futásidőbeli információk precíz reprezentálását, az ezekből képzett analízis modelleken pedig formális verifikációval vizsgálhatók az elvárt tulajdonságok. A formális verifikáció részben tervezési időben, részben pedig – különösen előre nem figyelembe vehető környezeti változások esetén – futási időben hajtható végre.
A doktori kutatás célja új formális verifikációs technikák kidolgozása átkonfigurálható és adaptív rendszerekhez. Ennek során jelentős kihívás a tervezési és futásidőbeli verifikáció módszereinek összehangolása (többek között a futásidőbeli verifikáció garanciáinak és erőforrásigényének tervezhetősége érdekében). Előrelépést ígérnek azok a megoldások, amelyek a változások függvényében lehetővé teszik az analízis modellek inkrementális generálását és megoldását. Ehhez meg kell vizsgálni és ki kell dolgozni az utóbbi években felmerült új ötletek és módszerek (pl. sztochasztikus játék-absztrakció dinamikus struktúrájú analízis modellek esetén, döntési diagram és tenzor műveletek egységes kezelése az inkrementális analízishez és az állapottér dinamikus változtatásához) integrált alkalmazását. Szintén új megoldások szükségesek ahhoz, hogy paraméterezhető rendszerek esetén a verifikációval garanciák legyenek adhatók a futásidőben beállítható biztonságos értéktartományokra.
A kutatás építhet az R5-COP nemzetközi kutatási projekt eredményeire és használati eseteire, valamint kapcsolódik a BME Kiválósági program tervezett témáihoz.
előírt nyelvtudás: angol felvehető hallgatók száma: 1
Bejelentkezés
