Absztrakt modellek konkretizálása kényszerkielégítési problémák segítségével

OData támogatás
Konzulens:
Szatmári Zoltán
Méréstechnika és Információs Rendszerek Tanszék

A feladatom alapproblémáját a napjainkban egyre inkább elterjedő autonóm robotok adták. Ezen robotok tesztelését eddig egy valódi, a teszteléshez felépített környezetben végezték, ami általában sok pénzt és időt emésztett fel (pl.: robottargoncákhoz felépített raktárrészlet). Ezzel szemben a robotok virtuális környezetben való tesztelése gyors és olcsó megoldás lenne. A virtuális tesztkörnyezet generálásának a legnagyobb hátránya, hogy az egyes attribútumok értékkészlete nem lehet túl nagy, mert állapottér robbanás következik be a generálás során. Emiatt első körben csak absztrakt adatokkal felírt környezeti modell elkészítése lehetséges, viszont a későbbi felhasználáshoz pontos tesztadatokra van szükség.

A feladatom egy olyan szoftver elkészítése volt, amellyel az absztrakt tesztadatokkal felírt környezeti modellből elő lehet állítani a konkrét adatokkal felírt végleges modellt. Az absztrakt modellek konkretizálásának központi feladata az absztrakt adatokból előállított kényszerkielégítési problémák (CSP – Constraint Satisfaction Problem) megoldása. E köré épül a program többi eleme, melyek azt a célt szolgálják, hogy a problémát a megfelelő formátumban elő lehessen állítani, illetve hogy a megoldás során kapott eredményeket képesek legyünk feldolgozni, értelmezni, majd a szükséges adatokkal frissíteni az eredeti környezeti modellt.

A teljes folyamat egymástól elkülöníthető egységekre osztható, melyek mögött egy-egy már létező technológia áll. A modellek kezelése, bejárása és módosítása az EMF (Eclipse Modeling Framework) segítségével történik. A folyamat központját képező kényszerkielégítési probléma előállítását az Acceleo Eclipse pluginnal végezzük el, amely olyan szöveges kódot generál, mely a megoldandó CSP-t a további feldolgozásra alkalmas formátumban tartalmazza. Ezt követően a Microsoft Z3 elvégzi a probléma megoldását, és az eredményt egy szöveges fájlba menti. A megoldás értelmezését egy újabb Eclipse plugin, az xText alkalmazásával tesszük meg oly módon, hogy definiálunk egy nyelvtant, mely segítségével feldolgozhatóvá válik Z3 kimenete. Az utolsó lépésben az eredeti modell frissítéséhez ismételten az EMF használata szükséges.

A dolgozat bemutatja a probléma megoldásához felhasznált technológiákat, illetve részletesen ismerteti az absztrakt modellek konkretizálásának folyamatát.

Letölthető fájlok

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