Regisztráció és bejelentkezés

A modelltranszformáció granularitásának hatása komponensalapú reaktív rendszerek formális ellenőrzésében

Napjainkra a legtöbb biztonságkritikus rendszer működésének biztosítása szoftverek feladata, ahol nem elegendő a vélhetően helyes működés, hanem formálisan is bizonyítanunk kell azt. Egy szoftver helyességének bizonyításakor azt vizsgáljuk, hogy teljesít-e bizonyos biztonsági követelményeket. A formális verifikáció alacsony szintű formalizmusokon lehetséges, a valós, komplex rendszerekről viszont általában nem állnak rendelkezésre ilyen modellek – helyette a mérnökök magas szintű modellekkel dolgoznak.

A két eltérő absztrakciós szint áthidalása modelltranszformációk segítségével történhet. Ez a gyakorlatban azt jelenti, hogy a magas szintű modell szemantikáját felhasználva leképezzük azt egy olyan alacsony szintű formalizmusra, amelyen már alkalmazható a formális verifikáció. Ezt visszafele is meg kell tennünk, amikor a formális verifikáció alacsony szintű eredményét visszavetítjük a magas szintű modellre. A Gamma modelltranszformációs keretrendszer ezt az elvet követve alkalmas többek között komponensalapú reaktív rendszerek formális verifikációjára. A bemenetként kapott magas szintű modelleket és követelményeket a Gamma letranszformálja (többek között) az alacsony szintű XSTS (eXtended State Transition System) nyelvre, elvégzi az XSTS modell formális verifikációját, majd ennek eredményét visszavetíti az eredeti modellre.

Dolgozatomban azt vizsgálom, hogyan hat a magas szintűről alacsony szintűre leképező modelltranszformáció granularitása a formális ellenőrzésre, elsősorban annak teljesítményére. Ez a gyakorlatban annak vizsgálatát jelenti, hogy a magas szintű modell (atomi) állapotátmeneteit hány alacsony szintű (atomi) állapotátmenetre képezzük le, azonos szemantika megtartása mellett. Részletesen áttekintem a granularitás megválasztásának lehetőségét és az azt végző általam fejlesztett algoritmust, amelyet a Gamma keretrendszer kiterjesztéseként implementáltam. A prototípus segítségével méréseken keresztül vizsgálom, hogyan hat a granularitás az alacsony szintű modellre, valamint az azon elvégzett formális verifikációra. Munkám hozzájárul a magas szintű, gyakran igen összetett mérnöki modellek hatékony verifikációjához, végső soron tovább segítve a modellellenőrzés gyakorlati elterjedését.

szerző

  • Szkupien Péter
    Mérnök informatikus szak, mesterképzés
    mesterképzés (MA/MSc)

konzulensek

  • Dr. Molnár Vince
    Adjunktus, Méréstechnika és Információs Rendszerek Tanszék
  • Graics Bence
    Doktorandusz, Méréstechnika és Információs Rendszerek Tanszék