Modell-alapú kényszerkielégítési problémák megoldása SMT környezetben

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

Modellvezérelt tervezés során az alkalmazási terület fogalmainak és az ö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 szakdolgozatom célja, hogy olyan eszközt készítsek, amellyel formális analízist végezhetek a szakterület-specifikus nyelveken, fényt derítve a DSL ellentmondásaira.

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 dolgozatomban egy keretrendszert mutatok be a szakterület-specifikus nyelvek vizsgálatára a következő módon:

(i) A jólformáltsági kényszereket és a származtatott értékeket elsőrendű logikai kifejezésekké fordítom, amelyeken SMT megoldóval végzek következtetéseket.

(ii) Approximációs technikákkal egy hatékonyan elemezhető logikai fregmensbe képzem le a komplexebb nyelvi elemeket.

(iii) Az elkészült eszközt ipari modellező eszközökhöz integrálom, amely az ellentmondásokat a nyelv szabványos példányaként állítja elő.

A módszer magja egy olyan leképezésen alapszik, amely egy származtatott attribútumokkal és relációkkal gazdagított EMF metamodellt, OCL 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 az R3COP ARTEMIS ipari követelményekkel rendelkező esettanulmányon sikerrel alkalmaztam, amelyben biztonságkritikus autonóm rendszerek (pl. ipari robotok) tesztelésének támogatása a cél. Az eszköz feladata a konkrét tesztesetek előállítása volt az OCL kényszerekkel meghatározott absztrakt tesztleírások alapján.

Letölthető fájlok

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