Biztonságkritikus protokoll tesztelése formális modell alapján

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

A szakdolgozat témája egy biztonságkritikus protokoll (az úgynevezett SCAN protokoll) megvalósításának ellenőrzése modell alapú teszteléssel, azt a modellt felhasználva, amelyet előtanulmányaim során hoztam létre. A modell alapon generált tesztekkel ellenőrizni kell, hogy az implementáció pontosan megvalósítja-e a modell által meghatározott viselkedést.

A SCAN protokoll célja, hogy a vasúti irányítástechnikában a vasúti objektumok (pl. váltók, jelzők) objektummoduljainak logikai egységei, és a vezérlő alkalmazás adatátviteli moduljainak kommunikációs egységei üzenetküldéssel megteremtsék a modulok közötti kapcsolatfelvételt, és –fenntartást biztonságos módon. A protokollt az UPPAAL eszközzel modelleztem, amely egy időzített automaták modellezésére és ellenőrzésére szolgáló eszköz. A modellellenőrző segítségével néhány kritikus eset ellenőrzését is elvégeztem, melyekkel a protokoll helyessége bizonyítható.

A modell megvalósítása és leírása után a modell alapú tesztelési lehetőségek szerepelnek. Ezeket egyesével végignézve kiderül, hogy melyek alkalmazhatóak a megvalósítás modell alapú tesztelésére, és melyek nem, vagyis melyek nem adnak új tesztesetet.

A következő fejezetben a tesztgenerálásra alkalmas eszközök leírása található. A tesztcélok meghatározása mellett szükséges kiválasztani a tesztgeneráló eszközöket, és elkészíteni a tesztgenerálás megvalósításához szükséges segédkomponenseket (modelleket).

Legvégül a kiválasztott tesztgeneráló eszköz által generált absztrakt tesztesetek (lépéssorozatok) szerepelnek, valamint annak leírása, hogyan kell alkalmazni ezeket egy konkrét teszt környezetben.

Letölthető fájlok

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