Forgatókönyv alapú specifikációk vizsgálata

OData támogatás
Konzulens:
Dr. Micskei Zoltán Imre
Méréstechnika és Információs Rendszerek Tanszék

Az elmúlt évek során az informatikai és azon belül is a biztonságkritikus rendszerek komplexitása rohamosan növekedett. Az összetett rendszerek tervezésében a bonyolultságukból adódóan meghatározó paradigmává vált a modell alapú megközelítés. Ennek során magasszintű modellekből kiindulva származtatjuk a rendszer konfigurációs beállításait, dokumentációt és akár forráskódját is. Így a magasszintű terveken különböző ellenőrzéseket lehet végrehajtani, miközben a folyamatos konzisztenciát megtartva automatikusan generálhatóak a platform-specifikus megvalósítások.

A dolgozatomban a rendszerkomponensek kommunikációjának modellezésére gyakran használt forgatókönyv-alapú specifikációs nyelv formalizmusokat vizsgálom. Ezek előnye, hogy még a konkrét komponensek megvalósítása nélkül, csupán a komponens szintű tervekből kiindulva vizsgálhatóak az egyes kommunikációs szekvenciák. Ezáltal korai fázisban detektálhatóvá válnak az inkonzisztens viselkedések, melyek a specifikációban rejlő hiányosságokra, ellentmondásokra vezethetőek vissza.

A dolgozatomban áttekintem a gyakran használt forgatókönyv-alapú specifikációs nyelveket, kiértékelem a hozzájuk tartozó nyílt forráskódú tervezőszoftvereket is. A szoftvereket két szempontból hasonlítom össze: az általuk támogatott specifikációs nyelv szabványossága, illetve az eszköz által megvalósított analízis és tervezési funkciók tekintetében.

Elosztott, beágyazott, biztonságkritikus rendszereket állapotgép formalizmussal is lehet tervezni. A Gamma állapotgép kompozíciós keretrendszer~\cite{graics-bsc, graics-tdk} egy eszköz, amely támogatja a komponens alapú, hierarchikus, reaktív rendszerek tervezését és analízisét. Ennek ellenére az eszközben jelenleg nem lehetséges egy adott komponens adott portjára vonatkozó kommunikációt modellezni és megtervezni.

Ezért dolgozatomban kiegészítem a Gamma keretrendszert egy modell alapú forgatókönyv nyelvvel, a Gamma szkenárió nyelvvel (GSL). A formalizmus a Live Sequence Chartokon alapul. A nyelv absztrakt és konkrét szintaxisát nyílt forráskódú modellezési technológiákkal készítettem el. Ezenkívül definiáltam a GSL formális működési szemantikáját is azáltal, hogy az egyes szkenáriókat véges automatákra képzem le.

Ezután a dolgozatomban bemutatok egy eljárást forgatókönyvek egymással való kompatibilitásának ellenőrzésére. Az eljárás olyan eseménysorozatok keresésén alapul, amelyek ellentmondásos döntésre juttatnak két forgatókönyvet. Azaz az eseménysorozatot az egyes forgatókönyveken szimulálva az egyik elfogadja (érvényesnek jelöli meg), míg a másik elutasítja (érvénytelennek jelöli meg) azt. A validációs eljárás eredményét visszavetítem a forgatókönyv szerkesztőbe azon célból, hogy a tervezőmérnök értesüljön az ellentmondásos definíciókról.

Végül bemutatom a GSL-nek a Gamma keretrendszerrel való integrálhatóságát egy modellvasút esettanulmányon keresztül. Ezenkívül méréseket is végeztem a szkenárió kompatibilitási eljárás futásidejének vizsgálatára.

Letölthető fájlok

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