A DDS kommunikációs szabvány memóriamodelljeinek formalizálása
A kritikus rendszerekben gyakran elosztottan futó, beágyazott komponensek együttműködése biztosítja a megfelelő működést. A helyes működés szempontjából kiemelten fontos a hálózati kommunikáció, a közösen használt adatok elosztott írásának és olvasásának helyes és kiszámítható működése. A szabványosító szervezetek többféle megoldást is kidolgoztak a gyors és megbízható adatcserére, ezek közül az egyik fontos szabvány a Data Distribution Service (DDS), melynek használata több iparágban is igen elterjedt, többek között a repülőgépekben, az autókban, nagyméretű ipari rendszerek vezérlésében. A szabvány jellemzője, hogy gyors adatmegosztást tesz lehetővé, melynek során különböző QoS paraméterek beállításán keresztül képesek vagyunk megszabni az adatok továbbításának tulajdonságait. Ezen beállítások különböző garanciákat adnak a kommunikáló komponensek számára, akik ezekre a garanciákra építve tudják a saját helyes működésüket garantálni.
Ezeket a DDS szabvány által nyújtott garanciákat derítettem fel a szabvány tanulmányozásával és kontrollált környezetben automatizáltan futtatott mintaalkalmazások viselkedésének vizsgálatával, majd a formális módszerek eszköztárát felhasználva a matematika nyelvén definiáltam őket. Erre a célra egy memóriamodell-alapú leíró nyelvet választottam, amely alkalmas elosztott rendszerekben az adatműveletek lehetséges végrehajtásainak precíz modellezésére, ábrázolására. Az általam készített memóriamodellek az első ilyen jellegű formalizálásai a DDS szabványnak. A memóriamodellek felhasználásával lehetőségünk van a DDS protokoll viselkedésének részletes leírására, hogy az azt használó elosztott alkalmazások rendszer szintű formális analízisét is elvégezhessük.
Munkám során az adatvesztésre és az adatok átrendeződésére fókuszáltam, mivel ezek azok a problémák, amelyek leginkább veszélyeztetik az adatkonzisztenciát nagyobb, kritikus rendszerekben. Az egyetlen komponens által végzett írások átrendeződésének elkerülését a DDS minden esetben biztosítani fogja, viszont probléma lehet a sorrendhelyesség akkor, ha több komponens is írja ugyanazt az adatot. Ezen túl készítettem egy valódi, fizikai demonstrátort is, amely jól ábrázolja, hogy miért is érdemes foglalkozni a QoS beállításokkal egy DDS-t használó rendszerben, és milyen katasztrofális meghibásodásokhoz vezethet egy hibásan beállított QoS profil.
szerző
-
Rádai Ronald
Villamosmérnöki szak, alapképzés
alapképzés (BA/BSc)
konzulens
-
Huszerl Gábor
mesteroktató, Méréstechnika és Információs Rendszerek Tanszék
