Absztrakció-alapú trace generálás formális verifikációs eszközök szemantikájának validációjára

A biztonságkritikus beágyazott rendszerek komplexitása folyamatosan növekszik. Ennek a komplexitásnak a kezelésére többek között különböző mérnöki modellek (pl. állapotgépek) tervezésben és verifikációban való használata ad megoldást. Formális verifikációs technikák segítségével bizonyos tulajdonságok teljesülése bizonyítható vagy hibák is megtalálhatóak, de ehhez a mérnöki modellezési nyelv pontos végrehajtási szemantikájának definiálására van szükség.

A formális verifikációs eszközökben szükség van ezen szemantikák formalizálására a bemeneti modell formális reprezentációra transzformálása során. Ez egy komplex elméleti és implementációs feladat, mivel a szemantika sokszor fél-formális és alulspecifikált. Ennek köszönhetően bizonyos hibák, például a koncepció félreértése (mely gyakran az alulspecifikált részek kiegészítésére adott ad-hoc döntésekben nyilvánul meg), gyakoriak. Ezen problémák később a felhasználó zavarodottságát vagy az eszköz által adott eredmények észrevétlen érvénytelenségét is eredményezhetik.

Ennélfogva a szemantikát implementáló modell-transzformáció validálása egy nélkülözhetetlen lépés. A jelenlegi gyakorlat teszt modellek készítése az adott modellezési nyelven majd érvényes lefutások megadása (általában manuálisan). Ezeket ezután a verifikációs eszköz vagy szimulátor által visszaadott lefutásokkal hasonlítják össze a konformancia bizonyítására. Ez a módszer hibákra hajlamos és nem hatékony, mivel bizonyos érvényes lefutások könnyen kihagyásra kerülhetnek.

A teszt lefutások automatikus generálása egy aktív kutatási terület. Minden lehetséges lefutást legenerálni egyszerű modellekre és modellezési nyelveken könnyű feladat. Azonban a feladat nehézsége könnyen megnövekedhet: például ha a modell nem csak vezérlési folyamot ír le, de adatokat is tartalmaz vagy ha az állapottere végtelen. Ilyen esetekben a lefutásokat legtöbbször valamilyen fedettségi kritérium teljesítésére korlátozzák. Azonban a probléma specifikus eseteiben precízebb megoldások is adhatóak.

A formális verifikációs eszközök egy gyakori típusa az absztrakció-alapú model checker. Munkámban ezen eszközök absztrakció alapú technikáit kihasználó automatikus lefutás generálási módszert javaslok. Egy olyan absztrakció alapú lefutás generáló algoritmust alkottam meg, mely sokszor képes a végtelen állapotterek kezelésére. Az absztrakciót konfigurálható módon képes alkalmazni és nem generál olyan lefutásokat, melyek szükségtelenül ismétlik a modell már korábban lefedett állapotait. A dolgozatomban megvizsgálom az algoritmus garanciáit, erősségeit és gyengeségeit, beleértve különböző elérhető fedettségeket és a skálázhatóságot.

Az algoritmust egy esettanulmány során ki is értékeltem reaktív állapotgépekhez készült eszközökön. A validált eszközök saját modellezési nyelvet alkalmaznak, mely megfelelően összetett ahhoz, hogy validálása szükséges legyen. A bemutatott elsődleges felhasználás mellett ismertetem, hogy az algoritmus milyen más felhasználásokra ad lehetőséget, mint például modellezési hibák azonosítása.

szerző

• 
  Ádám Zsófia
  Mérnök informatikus szak, mesterképzés
  mesterképzés (MA/MSc)

konzulens

• 
  Dr. Micskei Zoltán
  egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék

helyezés