Felhőalapú 4-értékű parciális modellező környezet gráftranszformációs környezetekhez
A szoftverfejlesztés számos területén alkalmaznak gráf alapú modelleket: biztonságkritikus rendszerek modell alapú tervezéséhez, autonóm járművek teszteseteinek reprezentálásához, vagy objektumorientált programok állapotainak leírására. A korszerű verifikációs eszközök képesek fejlett analízis technikák futtatására az ilyen modelleken: tervezési tér bejárással előállíthatók modelljavaslatok mérnöki feladatok automatikus megoldására, lehetséges rendszer architektúrák automatikus optimalizálása, valamint a tesztesetek szisztematikus generálása.
A parciális modellezés egy olyan újszerű technika, mellyel lehetőség nyílik a modellek még hiányos, nem eldöntötött vagy ismeretlen részeinek explicit megadására. Ez a megközelítés már a modell fejlesztésének korai fázisaiban, akár befejezettlen modelleken is lehetővé teszi a verifikáció és validáció megkezdését. Így a parciális modellek hatékony kezelése és feldolgozása számos modellezési feladat alapját képezi a kritikus rendszerfejlesztésben.
Azonban a parciális modellek analízise továbbra is kihívást jelent. Hiányoznak az eszközök az parciális modellek általános célú specifikációjának és transzformációjának támogatásához. Szemantikailag a paricális modellek transzformációja matematikai szempontból is nehéz feladat, hiszen az ismeretlen modellrészek transzformációjának le kell fednie a konkrét modellek (tipikusan végtelen) halmazát. Továbbá, az ilyen matematikai műveletek végrehajtása számításigényes, így gyakran nem valósítható meg asztali számítógépen futtatott modellezési környezetben.
Dolgozatunkban egy Belnap-Dunn 4-értékű logikán alapuló parciális modellező nyelvet adaptálunk, hogy hiányos, illetve inkonzisztens modelleket írjunk le, valamint javasolunk egy hatékony modelltranszformációs keretrendszert a fenti kihívások legyőzésére. A dolgozatunkban bemutatunk (i) egy leképzést a parciális modellező nyelvről egy olyan hatékony adatszerkezetre, mely nagy teljesítményű modellellenőrző eszközökben is használatos, és ennek segítségével táruljunk a parciális modelleket és lekérezéseket futtatunk rajtuk; (ii) egy általunk definiált szintaxist és a hozzá tartozó szemantikát modell transzformációs szabályok leírására 4-értékű logika alapján; (iii) egy transzformációs szabályokat végrehajtó motort, valamint értékeljük a felhasználhatóságát és a teljesítményét egy esettanulmányon keresztül. Az esettanulmány egy ipari projekt, ami azt célozza meg, hogy autonóm vezetést segítő rendszereket (ADAS) verifikáljuk.
A javasolt architektúrával lehetőség nyílik a gráf alapú érvelést felhő szervereken végezni, így kihasználva a rendelkezésre álló nagy hatékonyságú számítási erőforrásokat. A keretrendszer elérhető egy nyílt forráskódú eszköz részekény, valamint rendelezik a parciális modell transzformációk specifikálására és végrehajtására alkalmas web alapú grafikus felülettel. A legjobb tudásunk szerint ez az első modellező környezet, mely támogatja a parciális modell menedzsmentet, illetve lehetővé teszi a 4-értékű logika használatát modelltranszformációkkal egy felhő alapú környezetben.
szerzők
-
Garami Bence
Mérnök informatikus szak, alapképzés
alapképzés (BA/BSc) -
Golej Márton Marcell
Mérnök informatikus szak, alapképzés
alapképzés (BA/BSc)
