Thesis supervisor: Zoltán Imre Micskei
Location of studies (in Hungarian): Méréstechnika és Információs Rendszerek Tanszék Abbreviation of location of studies: MIT
Description of the research topic:
Napjainkban a komplex beágyazott, elosztott rendszerek tervezésénél egyre nagyobb szerepet kapnak a formális módszereken alapuló technikák. Különösen igaz ez a biztonságkritikus rendszerek területére, ahol matematikailag precíz bizonyításokra van szükség. A formális módszerek legnagyobb előnye, hogy már a tervezés kezdeti fázisától lehetővé teszik a rendszer működésének vizsgálatát. A modellellenőrzés egy olyan formális ellenőrzési technika, amely a rendszer formális modelljének állapotterét bejárva vizsgálja a formális specifikáció teljesülését. A formális módszerek alkalmazásának hátránya azonban a számítási igényük: akár már kis rendszereknek is nagy állapottere lehet, valós rendszerek ellenőrzésnek pedig gyakran gátat szab a rendszer komplexitása, és az ebből fakadó állapottér-robbanás jelensége. Ahogyan a modellek komplexitása nő, újabb és hatékonyabb algoritmusokra van szükség. A probléma kezelésére számos megközelítés született a szakirodalomban. Ezek közül az egyik leghatékonyabb technika az absztrakció, azonban a megfelelő absztrakció előállítása és a keresés automatizálása nehéz feladat.
Az ellenpélda-alapú absztrakció finomítás (CounterExample-Guided Abstraction Refinement, röviden CEGAR) algoritmusa is absztrakciót használ. A megközelítés lényege, hogy a konkrét állapottér egy részének bejárása során nyert információkat felhasználja az absztrakció finomítására, így nyújtva megoldást nemcsak az állapottér hatékony kezelésére, hanem a megfelelő absztrakció automatikus előállítására is. A megfelelő absztrakciós függvény megtalálása és a finomítási folyamat nagy számításigényű lehet valós rendszerek esetén. A létező megoldások egy része különböző logikai megoldókat használ erre a feladatra, mások szimbolikus módszereket, de alkalmaznak explicit modellellenőrzőt is az állapottér bejárása során. A különböző megközelítések kombinálása ötvözheti ezeknek az előnyeit.
A hallgató feladata megvizsgálni az irodalmat és CEGAR-alapú modellellenőrző algoritmusokat fejleszteni beágyazott és elosztott szoftver rendszerek ellenőrzésére. Fontos célja a doktori munkának a különböző megközelítések alapján egy hibrid megközelítés implementálása, amely ki tudja használni az explicit állapottér felderítés hatékonyságát és a logikai megoldók azon tulajdonságát, hogy állapottér halmazok felett is hatékonyan tudnak következtetni. Emellett a hallgató feladata továbbfejleszteni a létező, explicit bejárást használó megoldásokat olyan irányba, hogy az állapottér inkrementális felderítésére és kiértékelésére is képesek legyenek.