Hatékony absztrakcióalapú modellellenőrzés doménspecifikus információk kihasználásával

A biztonságkritikus rendszerek helyes működésének szavatolása kulcsfontosságú, mivel az azokban jelenlévő legkisebb hiba is súlyos anyagi kárral járhat, szélsőséges esetekben akár emberi életekbe is kerülhet. A formális verifikáció képes a rendszerek helyességének matematikailag precíz bizonyítására és a rejtett hibák megtalálására is, széleskörű elterjedését azonban hátráltatja nagy számításigénye. A beágyazott fejlesztők és a hardvertervező mérnökök számára mára kiterjedt formális verifikációs eszközkészlet áll rendelkezésre, ugyanez azonban a rendszertervező mérnökökről sajnos nem mondható el.

A rendszertervező mérnökök jellemzően magas szintű, összetett, heterogén modelleken dolgoznak. Egy ilyen rendszermodell ellenőrzése más jellegű kihívást jelent, mint szoftverek vagy hardvermodellek analízise - az ezeknél használt reprezentációk, algoritmusok más jellegű problémákhoz lettek kifejlesztve. Egy rendszerterv általában több heterogén komponenst is tartalmaz, így a teljes rendszer formális leírásához egy olyan közös nyelvre van szükség, amely jó kompromisszumot jelent a különböző paradigmák között. Egy ilyen nyelv megtervezése során az általánosság és a hatékonyság között egyensúlyozunk: hogyan tudunk minél több problémaspecifikus információt kihasználni az ellenőrzés során úgy, hogy az általánosságot - és ezáltal a különböző heterogén komponensek közös leírásának lehetőségét - ne veszítsük el?

Korábbi kutatási munkám során kidolgoztam a kiterjesztett szimbolikus rendszer (röviden XSTS) formalizmust, mely az első lépés volt egy ilyen nyelv megalkotásának irányába. Jelen dolgozatomban olyan kiegészítéseket és optimalizációkat mutatok be, melyekkel az XSTS nyelv és infrastruktúra képessé vált nagyméretű, ipari modellek ellenőrzésére. A nyelv kifejezőerejének növelésével szélesítettem az ellenőrizhető magas szintű modellek körét. A szorzat absztrakciós domén továbbfejlesztésével létrehoztam egy olyan dedikált absztrakt domént, mely hatékonyan képes együtt kezelni a vezérlési és általános információkat. Kidolgoztam olyan algoritmikus optimalizációkat is, melyek az adott absztrakciós szinten rendelkezésre álló információ leghatékonyabb felhasználását segítik, ezzel egyszerűsítve az algoritmus mögötti kényszermegoldónak átadott logikai kifejezéseket. Emellett javaslok olyan modellezési, illetve leképzési gyakorlatokat, melyek a legjobb teljesítményhez vezetnek adott forrásmodell esetén. A dolgozatban bemutatott kiegészítések egy jelentős és határozott lépést jelentenek a heterogén rendszertervek ellenőrzéséhez optimális absztrakciós szint megtalálásában. Eredményeim alátámasztására dolgozatomban egy olyan, SysML modellezési nyelven készült esettanulmányt is bemutatok, amely az XSTS nyelv segítségével vált verifikálhatóvá és demonstrálja a nyelv gyakorlati alkalmazhatóságát. Megközelítésem alaposabb kiértékeléséhez egy kiterjedt mérési kampányt folytattam, melynek eredményei alátámasztják az XSTS nyelv kiegészítéseinek hatékonyságát.

szerző

• 
  Mondok Milán
  Mérnök informatikus szak, mesterképzés
  mesterképzés (MA/MSc)
  

konzulens

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

helyezés