Modelltranszformációk helyességellenőrzése formák analízisével
Modellvezérelt tervezés során egy mérnöki modellből modelltranszformáció segítségével egy matematikailag precíz analízis modellt származtatunk, melyen már a fejlesztés korai szakaszában elkezdődhet a rendszer helyességellenőrzése. A gráftranszformációk paradigmája egy intuitív és egyben precíz formális módszert ad e modelltranszformációk specifikációjára. 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.
Valós informatikai rendszerek gyakran potenciálisan végtelen állapottérrel rendelkeznek, amely a formális verifikáció egyik legkomplexebb esete, hiszen a kimerítő állapottér-bejárás közvetlenül nem lehetséges. Így az ellenőrzés végrehajtásához szükséges valamilyen absztrakció alkalmazása. A forma (shape) analízis módszere egy ilyen absztrakciós technikát ad meg. Ennek során gráf alapú modelljeinket ekvivalencia osztályokba soroljuk, és ezeket címkézett gráfok speciális halmazával, formákkal ábrázoljuk. A gráftranszformációs lépések absztrakt megfelelőjét végigvezetve a formákon biztosan véges állapotteret kapunk, melynek analízisével bizonyíthatjuk a gráftranszformációs rendszer helyességét.
Dolgozatom célja, hogy egy egyesített, jól paraméterezhető, gráfelemek ekvivalencia relációján alapuló forma analízissel megteremtsem a lehetőséget arra, hogy a szakirodalomban leggyakrabban használt módszereket keverve vagy egyszerre lehessen alkalmazni, így növelhető legyen azok hatékonysága. Az eljárás egyik legfontosabb és egyben leggyakrabban használt részfeladatai a formák levezethetőségének és ellentmondásosságának felfedése, így ezek végrehajtása kutatásra érdemes terület.
Dolgozatomban megadok egy ekvivalencia relációkkal parametrizálható általános formázási módszert, amellyel figyelembe vehető a bizonyítandó követelmény specifikus tartalma. Leírok egy automatikus módszert a formákon végrehajtandó transzformációs lépés kiszámítására és a formák konzisztenciaellenőrzésére, amely gráfmintaillesztési technikák, ontológiai lekérdezések és dedikált tételbizonyítók kombinált felhasználásán alapul. Fenti módszerek implementációjára architektúrát és megvalósíthatósági tanulmányt adok, mely korszerű szoftverkomponensek (VIATRA2, Pellet és Prover9) felhasználásán alapul.
Mindezekkel egy olyan bővíthető architektúrát adok meg, amely képes létező forma analíziseket és következtető módszereket integráltan alkalmazni. Így elérhető, hogy a kombinált módszer többfajta követelmény bizonyítására legyen képes.
szerző
-
Semeráth Oszkár
mérnök informatikus
nappali
konzulens
-
Dr. Varró Dániel
egyetemi tanár, Méréstechnika és Információs Rendszerek Tanszék
