Komplex események feldolgozása automataelméleti alapokon

OData támogatás
Konzulens:
Vörös András
Méréstechnika és Információs Rendszerek Tanszék

A hagyományos kritikus rendszerekben gyakorta alkalmazott módszer a futási idejű ellenőrzés. Ennek célja olyan ellenőrző programok szintézise, melyek segítségével felderíthető egy kritikus komponens hibás, a követelményektől eltérő viselkedése a rendszer működése közben. Többek között ezt a célt szolgálja egy, a tanszéken fejlesztett keretrendszer is, amely élő modelleket használ és az azok fölött értelmezett modelltranszformációs szabályok segítségével definiálja a vizsgálandó temporális kifejezést. Modelltranszformációk helyességének ellenőrzése azonban algoritmikusan eldönthetetlen feladat általánosságban, így a definiált temporális viselkedéseket is nehéz formálisan vizsgálni. Az irodalomban többféle megközelítés létezik a temporális viselkedések definiálására és többféle formalizmust is definiáltak automata alapokon. Ezekben közös, hogy az automaták többnyire jól vizsgálhatóak algoritmikusan, az általuk definiált és elfogadott nyelvekkel kapcsolatban lehetőség van formális analízisre és ellenőrzésre.

Ebben a dolgozatban megvizsgáljuk az irodalomban ismert legfontosabb automataelméleti megközelítéseket, és ez alapján kiterjesztjük a tanszéki keretrendszert a temporális viselkedések automata elméleti reprezentációjával. Bemutatjuk egy automata reprezentáció implementációját amely alkalmas temporális tulajdonságok ellenőrzéséhez. Elemezzük a megoldást kifejezőerő szempontjából, és megvizsgálunk egy mérnöki leíró nyelvet és annak leképzését automata reprezentációra.

Letölthető fájlok

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