Szakterület-specifikus nyelvek konzisztencia ellenőrzése
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 dolgozat fő célja, hogy olyan eszközt biztosítsunk, 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 TDK dolgozatunkban egy egységes keretrendszert javasolunk 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ítjuk, amelyeken SMT megoldókkal végzünk következtetéseket. (ii) Approximációs technikákat alkalmazva egy hatékonyan elemezhető logikai fregmensbe képezzük az komplexebb nyelvi elemeket. (iii) A validációs eszközünket ipari modellező eszközhöz integráltuk, amely az ellentmondásokat a nyelv szabványos példánymodelljeiként állítja elő.
Módszerünk 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özünket két ipari követelményekkel rendelkező esettanulmányon is sikerrel alkalmaztuk. 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ünk feladata a konkrét tesztesetek előállítása volt az OCL kényszerekkel meghatározott absztrakt tesztleírások alapján.
szerzők
-
Barta Ágnes
mérnökinformatikus
nappali -
konzulensek
-
Dr. Varró Dániel
egyetemi tanár, Méréstechnika és Információs Rendszerek Tanszék -
Szatmári Zoltán
Tudományos segédmunkatárs, Méréstechnika és Információs Rendszerek Tanszék -
Dr. Horváth Ákos
tudományos munkatárs, Méréstechnika és Információs Rendszerek Tanszék
helyezés
Morgan Stanley I. helyezett