Modelltranszformációk formális analízise

OData támogatás
Konzulens:
Dr. Varró Dániel
Méréstechnika és Információs Rendszerek Tanszék

Modellvezérelt tervezés során egy mérnöki modellből modelltranszformáció segítségével származtatunk egy analízis modellt. A modelltranszformációkban lévő hibák viszont érvénytelenné tehetik a matematikai modell precizitásából származó előnyöket. Így a modelltranszformációk hibamentességének biztosítását célszerű formális verifikációval garantálni.

A gráftranszformációk paradigmája egy intuitív, jól tervezhető, és egyben precíz formális módszert ad a modelltranszformáció megvalósításához. A gráftranszformációs rendszerek potenciálisan végtelen állapottérrel járnak, amely jelentősen gátolja a helyességellenőrzésüket. A shape analízis módszerével akár végtelen állapotterű gráftranszformációs rendszerek is ellenőrizhetőek. Ekkor állapotterünk gráfjait véges számú csoportokba rendszerezzük, a csoportokat címkézett gráfok speciális halmazával, shape gráfokkal ábrázoljuk. A gráftranszformációs lépések absztrakt megfelelőjét végigvezetve a shape gráfokon absztrakt állapotteret kapunk, amely analízisével bizonyíthatjuk gráfnyelvtanunk helyességét.

A szakirodalomban két fő irányvonal található a shape gráfok alkalmazására. Az egyik úgynevezett neighbourhood shape gráfok módszere a benne lévő csúcsok környezete alapján osztályozza gráfjainkat, míg a másik, állapotainkat háromértékű logikai struktúraként ábrázolja. Ezek a módszerek a különböző karakterisztikájú problémákat eltérő hatékonysággal képesek megoldani.

Szakdolgozatomban bemutatom, hogy e módszerek megadhatóak közös, gráfelemek ekvivalenciáján alapuló definícióval, melyben megfelelő paraméterezéssel mindkét absztrakció ábrázolható. A közös leírással elérhető, hogy a feladat ismeretében, a paraméterezés kombinálásával, a módszerek erősségét kiemelve javíthassunk az analízis kivitelezhetőségének és sikerességének esélyén.

A közös módszer VIATRA2 modelltranszformációs rendszer fölé tervezett megvalósíthatóságáról tanulmányt végeztem, lévén, hogy a rendszer alkalmas nagy modellterek kezelésére, illetve az inkrementális gráfmintaillesztés lehetőségét használva hatékonyan hajthatjuk végre a szükséges műveleteket.

Letölthető fájlok

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