MagicDraw állapottérképek formális verifikációja

OData támogatás
Konzulens:
Farkas Rebeka Krisztina
Méréstechnika és Információs Rendszerek Tanszék

Komplex rendszerek tervezése során szükségessé válik fejlett modellező eszközök különböző funkcióinak igénybevétele, pl. validáció, kódgenerálás, verifikáció. Az iparban az egyik legelterjedtebb eszköz a MagicDraw ami lehetőséget biztosít komplex rendszerek tervezésére és ezek viselkedésének modellezésére. MagicDraw-t gyakran használnak kritikus rendszerek tervezésére, melyek esetén elengedhetetlen, hogy megbizonyosodjunk a rendszer működésének helyességéről.

A MagicDraw számos hasznos funkcióval rendelkezik, azonban a formális verifikációt nem támogatja. Az ipari alkalmazhatóság szempontjából viszont jelentős előnyökkel járna ezeknek a módszereknek a támogatása.

A Gamma egy, a tanszéken fejlesztett modellező eszköz, amely nem rendelkezik a MagicDraw-éhoz hasonlóan kiterjedt eszközkészlettel, azonban viselkedésmodellek formális verifikációját támogatja. A munkám során MagicDraw modellek formális verifikációját azáltal teszem lehetővé, hogy megvalósítok egy leképzést a két eszköz modelljei között.

Dolgozatomban bemutatom a Gamma és MagicDraw eszközöket és a leképzés megvalósításához szükséges háttérismereteket. Továbbá részletesen kitérek az implementáció során használt technológiákra és elvekre. A módszert egy példán szemléltem és elméleti megfontolások alapján értékelem. A bemutatott eszköz lehetővé teszi modellek egy tágabb halmazának formális verifikációját.

Letölthető fájlok

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