Statikus hiba lokalizációval támogatott modellellenőrzés biztonságkritikus rendszerekben

A különböző szoftveres megoldások egyre több feladatot látnak el biztonságkritikus rendszerekben. Példaként lehet említeni a gépjárművek kormányműjét, vagy akár a repülőgépek, atomerőművek irányítórendszerét. Ami ezen rendszerekben közös, az egy esetleges hiba következménye: hatalmas anyagi veszteség, súlyos környezeti kár, vagy akár emberéletek elvesztése.

Ezen biztonságkritikus szoftverkomponensek egyrészt kritikusak a rendszer működése szempontjából, másrészt meglehetősen összetettek. A komponensek helyes működését garantálni kell, ami miatt különféle módszereket lehet bevetni. A tesztelés egy bevett módszer hibák keresésére, éppen ezért minden, biztonságkritikus rendszerek fejlesztését szabályozó szabvány elvárja a használatát. Ugyanakkor a tesztelés önmagában a helyességet nem tudja igazolni. Egy merőben más megközelítés a formális verifikáció, ami a szoftver matematikai modelljét elemezve ad egy bizonyítást a szoftver helyességére vagy egy ellenpéldát egy hiba jelenlétének tanúsítására. Egy ellenpélda - egy hibás teszt nyomához hasonlóan - egy hibához vezető útvonalat ír le a rendszerben, és elemezni lehet a hiba okának feltárása érdekében. Azonban egy komoly probléma, hogy minél összetettebb a vizsgált rendszer, annál összetettebb lesz az ellenpélda is, és nehezebb az értelmezése. Egy ipari rendszer esetén az ellenpélda több száz vagy akár több tízezer utasítást tartalmazhat, amiknek nagy része irreleváns a hiba elhárításához.

A munkám célja egy olyan módszer kidolgozása, ami képes a hiba helyét megállapítani az ellenpéldákban anélkül, hogy azokat futtatni kéne. A módszer egy irodalomban ismert algoritmuson alapszik, ami a leggyengébb előfeltétel alapú érvelést használ ellenpéldák vizsgálatára. Munkám során továbbfejlesztettem az algoritmust, hogy a hiányosságait kijavítsam, valamint, hogy képes legyen a biztonságkritikus rendszerek verifikációs sajátosságait kezelni. Az algoritmus eredményét egyéb heurisztikákkal kombinálva a módszer egy pontszámot rendel a vizsgált szoftver utasításaihoz, ami az adott utasítás hibához való hozzájárulását jelzi. Ezt követően, a pontszámok értelmezésével a fejlesztő képes meghatározni, hogy a vizsgált kód mely kis részében keresse a hiba okát. A módszert C nyelvű szoftvereken, valamint ipari partnerektől származó PLC kódokon értékelem ki, és hasonlítom össze a hatékonyságát az eredeti algoritmuséval.

szerző

• 
  Dobos-Kovács Mihály
  Mérnök informatikus szak, mesterképzés
  mesterképzés (MA/MSc)

konzulens

• 
  Dr. Vörös András
  egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék

helyezés