Hibrid rendszerek verifikációs algoritmusainak vizsgálata

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

Napjainkban biztonságkritikus rendszerek egyre inkább kezdenek elterjedni, azonban a hibás működésük komoly károkat okozhat. Ennél fogva nagyon fontos matematikailag precíz verifikációs technikák használata segítségével a működésük helyességét.

A legtöbb biztonságkritikus rendszer hibrid rendszer, tehát folytonos és diszkrét tulajdonságokkal is rendelkezik, ami meglehetősen bonyolult viselkedéshez vezethet. Formális verifikációhoz ezen rendszerek viselkedését a hibrid automata magasszintű, állapotalapú formalizmussal modellezik. Ezen formalizmus a diszkrét viselkedést a hagyományos véges automatákhoz hasonló módon, míg a folytonos viselkedést differenciálegyenletek segítségével írja le.

Ezzel a formalizmussal egyszerűen le lehet írni hibrid rendszereket, ellenben helyességük sikeres bizonyításához hatásos verifikációs technikákra van szükség. Mind a diszkrét, mind a folytonos rendszerek ellenőrzése önmagában is nehéz probléma, hibrid rendszerek verifikációja pedig általánosságban algoritmikusan eldönthetetlen feladat.

Ennek ellenére ilyen rendszerek ellenőrzése elkerülhetetlen probléma, melynek megoldására különböző eszközök és megközelítések születtek. A komplexitás csökkentése végett ezen eszközök gyakran csak a hibrid automaták bizonyos típusaival foglalkoznak, vagy a verifikációs problémák módosított verzióival. Szintúgy gyakori módszer a számítások közben közelítések használata (ami esetleg helytelen eredményhez vezethet).

Munkám során összehasonlítom a legfontosabb hibrid automaták modellezésére és ellenőrzésére szolgáló eszközöket és algoritmusokat, a támogatott hibrid automata típusok figyelembevételével. Ennek érdekében fejlesztettem egy eszközt, ami egy közös felületet biztosít hibrid automaták modellezésére és létező eszközök segítségével lehetővé teszi a verifikációt. Ezáltal lehetőség nyílik hibrid verifikációs eszközök összehasonlítására azonos bemeneteken.

Letölthető fájlok

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