Mérnöki modellek konfigurálható szemantikájú verifikációja moduláris modellezési nyelv segítségével
A kritikus rendszerek, például vasúti infrastruktúra, autonóm járművek, repülőgépek vagy atomerőművek hibás működése súlyos anyagi károkon felül akár emberéleteket is veszélyeztethet, így ezen rendszerek tervezése során kiemelt fontosságú a megbízhatóság garantálása. A megbízhatóság biztosítására léteznek a tervezés közben is alkalmazható különböző verifikációs és validációs (V&V) technikák, azonban, ahogy növekszik a rendszerek komplexitása, úgy nehezedik az ellenőrzésük is. A mérnöki tervezői munka egyszerűsítése érdekében egy elterjedt megközelítés a modellalapú rendszertervezés, amely módszertan a dokumentum-centrikus megoldásokhoz képest központi elemmé teszi a mérnöki modellezési nyelveket. Az ezek segítségével készített tervek verifikációja és implementációja megfelelő eszközök segítségével gyorsítható és automatizálható.
Számos mérnöki modellezési nyelv érhető el (pl. UML, SysML v1 és v2, AADL), melyek hasonló, de mégis eltérő megközelítéseket alkalmaznak. Az ellenőrzés és implementáció szempontjából fontos különbségeket jelentenek a szemantikai variációk – a nyelvek hasonló szintaktikájú elemeihez gyakran kis mértékben eltérő végrehajtási szemantika társul. Hasonlóan fontos, hogy gyakran ezek a nyelvek alulspecifikált végrehajtási szemantikával rendelkeznek, melyet a rendszermérnökök és a vállalatok egyénileg (gyakran eltérően) értelmeznek. Ezen különbségek megnehezítik a nyelvek egységes kezelését, ami jelentősen lassítja a fejlett verifikációs eszközök ipari elterjedését. Ilyen verifikációs eszköz az egyetemi fejlesztésű Gamma Állapotgép Kompozíciós Keretrendszer is, amely számos modelltranszformáció segítségével képes a különböző modellvariánsok és különböző alacsonyszintű nyelvek közötti átmenetre. A keretrendszer bonyolultsága azonban a variánsok miatt egyre jobban megnehezíti a bővíthetőségét és karbantarthatóságát.
Jelen dolgozat célja egy új, moduláris szemantikával rendelkező modellezési nyelv alkalmazásának vizsgálata, amely segítségével a Gamma keretrendszerben leprogramozott, nehezen újrahasznosítható modell-transzformációk helyettesíthetők egy olyan rugalmas modellezési nyelvvel, amely alkalmas a magasszintű nyelvek struktúrájának alacsony szintű elemekkel történő modellezésére, beleértve a magasszintű elemek szemantikáját is. A nyelv egyik fő erőssége, hogy a SysML v2 nyelvhez hasonlóan egy alap elemkészletből különféle kompozíciós technikákkal lehet összetett elemeket építeni, melyek szemantikáját vissza lehet vezetni az alap elemkészlet szemantikájára, és az így kapott elemeket újrahasználható könyvtárakba lehet szervezni. A magasszintű nyelvek leképezése így már nem modelltranszformációs, hanem modellezési feladattá válik, ahol a magasszintű nyelv szemantikai varianciáit az újrahasználható könyvtárak modellelemeinek megfelelő megválasztásával pontosíthatjuk.
Az eredményekkel lehetővé válik 1) a különböző modellezési nyelvek lehetséges szemantikáinak kipróbálása; 2) a különböző vállalatok saját konvencióinak figyelembevétele, vagyis a transzformáció testreszabhatósága; 3) a transzformáció optimalizálása mérésekkel alátámasztva; illetve 4) új nyelvek egyszerű bevezetése a keretrendszerbe. A javasolt módszer prototípus implementációját különböző esettanulmányokon keresztül vizsgálom, és hasonlítom össze a Gammában jelenleg is elérhető funkciókkal.
szerző
konzulensek
-
Dr. Molnár Vince
Adjunktus, Méréstechnika és Információs Rendszerek Tanszék -
Graics Bence
Tudományos segédmunkatárs, Méréstechnika és Információs Rendszerek Tanszék
