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
Tudományos segédmunkatárs, Méréstechnika és Információs Rendszerek Tanszék