Adatintenzív rendszerek szimbolikus modellellenőrzése

OData támogatás
Konzulens:
Molnár Vince
Méréstechnika és Információs Rendszerek Tanszék

Biztonságkritikus rendszereknél egyre elterjedtebb a tervezésidejű verifikáció. Egy ilyen technika az ún. modellellenőrzés. Ahogy a rendszerek egyre komplexebbé válnak, úgy nő a rendszerek állapotváltozóinak száma is. Az ilyen ``adatintenzív'' rendszerek állapotainak száma robbanásszerűen nőhet, az állapotteret explicit módon már nem lehetséges eltárolni.

Ezen probléma megoldására jelentek meg a szimbolikus modellellenőrző technikák, melyek az állapotteret kompakt adatszerkezetek, jellemzően döntési diagramok segítségével tárolják. Az ezeken dolgozó algoritmusok gyakran hatalmas állapottereket képesek hatékonyan kezelni és tárolni.

Komplex, komponensekből felépülő rendszerek esetében komoly előrelépést jelenthet az állapottér-reprezentáció során a rendszermodell struktúrájának kiaknázása a redundancia csökkentéséhez. Az utóbbi néhány évben jelentek meg az úgynevezett hierarchikus döntési diagramok, melyek a modellek hierarchikus adatszerkezeteihez illeszkedve képesek hatékonyan csökkenteni az állapottér-reprezentáció méretét.

Jelen szakdolgozat célja a hierarchikus döntési diagramok vizsgálata és implementálása az azokon értelmezett műveletekkel és állapottér felderítő algoritmusokkal együtt, illetve ezek összehasonlítása a megszokott szimbolikus modellellenőrző technikákkal.

Letölthető fájlok

A témához tartozó fájlokat csak bejelentkezett felhasználók tölthetik le.