Modelltranszformációk formális helyességellenőrzése

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 az alkalmazási terület fogalmainak és összefüggéseinek leírására széles körben használnak szakterület-specifikus nyelveket (Domain-Specific Language, DSL). A DSL-ek segítségével automatikusan származtathatunk egy ellenőrzött rendszermodellből teszteseteket, vagy bizonyíthatóan helyes forráskódot. Azonban maguk a DSL nyelvek is tartalmazhatnak tervezési hibákat, melyek érvényteleníthetik a rendszermodellen végzett vizsgálatok eredményeit. A diplomamunka célja, hogy olyan eszközt biztosítsak, amellyel formális analízist végezhetünk szakterület-specifikus nyelveken, fényt derítve a DSL specifikációk ellentmondásaira és többértelműségére.

A szakterület-specifikus nyelvek konzisztencia-vizsgálata komoly kutatási kihívást jelent, mert (i) az összetett DSL-eken történő logikai következtetés algoritmikusan eldönthetetlen probléma, (ii) további elméleti nehézségei vannak a hozzáadott jólformáltsági kényszerek és a származtatott értékek kezelésének, és (iii) olyan eszköz fejlesztésére van szükség, amit a következtetési eljárás ismerete nélkül is használhat a nyelv tervezője.

A diplomamunkámban egy egységes keretrendszert javasolok a szakterület-specifikus nyelvek konzisztenciavizsgálatára a következő módon: (i) A jólformáltsági kényszereket és származtatott érték definícióját egységesen elsőrendű logikai kifejezésekké fordítom, amelyeken SMT megoldókkal végzek következtetéseket. (ii) Approximációs technikákat alkalmazva egy hatékonyan elemezhető logikai fregmensbe képzem az komplexebb nyelvi elemeket. (iii) A validációs eszközüt ipari modellező eszközhöz integráltam, amely az ellentmondásokat a nyelv szabványos példánymodelljeiként állítja elő.

Módszerem magja egy olyan leképezésen alapszik, amely egy származtatott attribútumokkal és relációkkal gazdagított EMF metamodellt, OCL vagy EMF-IncQuery nyelven definiált jólformáltsági kényszereket és egy hiányos kezdeti példánymodellt vár bemenetül. Az eszköz a kezdeti modellt kiegészíti új elemek felvételével a generált axiómák és a Z3 SMT megoldó által ismert elméletek alapján, úgy, hogy az eredmény megfeleljen a nyelv specifikációjának.

Az eszközt két ipari követelményekkel rendelkező esettanulmányon is sikerrel alkalmaztam. Egy brazil repülőgépgyártóval közös projektben EMF-IncQuery gráfmintákkal megfogalmazott származtatott értékekkel és jólformáltsági kényszerekkel gazdagított EMF metamodell konzisztencia vizsgálata volt a cél, hogy a fejlesztés korai szakaszában detektáljuk a nyelv hibáit. Az R3COP ARTEMIS esettanulmányban biztonságkritikus autonóm rendszerek (pl. ipari robotok) tesztelésének támogatása a cél, ahol az eszköz feladata a konkrét tesztesetek előállítása volt.

Letölthető fájlok

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