Komplex rendszerek modellezése és verifikációja
A rendszertervezés során a szoftver- és hardverrendszerek helyességének ellenőrzése, azaz verifikációja egyre nagyobb szerepet kap. A verifikációval kapcsolatban alapvető elvárás, hogy teljes körű és matematikai precizitású legyen, ami formális módszerek alkalmazását igényli. Komplex rendszerek esetén a formális verifikácó igen számításigényes probléma. Bár a rendelkezésre álló számítási kapacitás növekszik, még mindig komoly kihívást jelent a nagyméretű, összetett architektúrák ellenőrzése.
A verifikáció folyamatában gyakran alkalmazott módszer a modellellenőrzés. Ennek során elkészítjük a rendszer egy modelljét – esetünkben Petri-hálók segítségével –, majd felderítjük annak állapotterét. Utána az állapottérben a specifikációhoz kötődő kritériumok teljesülését ellenőrizzük – esetünkben temporális logikai kifejezések segítségével megfogalmazott követelmények formájában – matematikai módszerek alkalmazásával.
Korábbi munkáinkban bemutattuk, hogy az ún. szaturációs algoritmus használatával az állapottér hatékonyan felderíthető és kompakt formában tárolható. Összetett rendszerek modellellenőrzése során azonban felmerülnek olyan problémák, amelyekre az eddigi algoritmusaink nem nyújtottak megoldást. Ilyenek többek között a nagy komplexitású és/vagy végtelen állapotterű modellek analízise. Emellett problémát jelentett az is, hogy bizonyos rendszerméret felett az egyszerű Petri-hálók már nem alkalmasak kompakt és szemléletes modellek készítésére.
Munkánk során a következő megoldásokat vizsgáltuk meg a felmerült problémákra:
– a szaturáció alapú korlátos állapottér-felderítést és modellellenőrzést, amelynek segítségével a teljes állapottér bejárása nélkül is lehetőség van bizonyos követelmények ellenőrzésére [1], így lehetővé téve a komplex rendszerek, nagy vagy végtelen állapotterű modellek vizsgálatát;
– az ún. vezérelt szaturációt [2], amely a kifejezések ellenőrzése során mutatkozó, felesleges bejárási lépések redukálásával gyorsítja a modellellenőrzést;
– a korlátos állapottér-felderítést és a vezérelt szaturációt ötvözve létrehoztunk egy hatékony szaturáció alapú korlátos modellellenőrző algoritmust, amely a korábbi algoritmust [1] jelentősen felgyorsítja;
– kidolgoztuk a színezett Petri-hálók szaturációs vizsgálatát, amely formalizmus segítségével a modellek kompaktabb, skálázható formában készíthetők el, így sok olyan probléma is modellezhető a segítségükkel, amelyekre az egyszerű Petri-hálók nem nyújtottak megfelelő megoldást.
A vizsgált algoritmusokat az általunk fejlesztett PetriDotNet keretrendszer részeként a gyakorlatban is megvalósítottuk, és hatékonyságukat mérésekkel támasztottuk alá dolgozatunkban.
szerzők
-
Darvas Dániel
mérnök informatikus
nappali -
Jámbor Attila
mérnök informatikus
nappali
konzulensek
-
Dr. Bartha Tamás
docens, Méréstechnika és Információs Rendszerek Tanszék -
Dr. Vörös András
egyetemi docens, Méréstechnika és Információs Rendszerek Tanszék
