Tenzorreprezentációs módszerek a komplex biztonságkritikus rendszerek megbízhatóságának vizsgálatában
A biztonságkritikus komplex kiberfizikai rendszerek helytelen működése emberi életet veszélyeztet, vagy nagy mértékű üzleti kárt okozhat. Az ilyen rendszerek tervezésekor különösen fontos a funkcionális követelményeken túl a különböző extra-funkcionális követelményeket is szem előtt tartani, mint
a biztonság, a megbízhatóság, vagy a rendelkezésre állás. Ezen követelmények alapvetően kvantitatívak, azaz különböző mérőszámokra határoznak meg elérendő célértékeket. Teljesülésük biztosításával már a rendszertervezés fázisában is foglalkozni kell, amikor még nem áll rendelkezésre a működő rendszer, csak annak modellje.
A megbízhatósági és rendelkezésre állási metrikák meghatározásához a rendszer viselkedésére jellemző véletlenszerűséget tartalmazó, sztochasztikus modelleket használunk. A munkámban egy elterjedt sztochasztikus modellezési formalizmust, a hibafákat vizsgálom. Ez a formalizmus a rendszerszintű hiba dekomponálásán alapul: az egyes elemi komponensek meghibásodásának egy logikai függvényével írja azt le.
A modellből a szükséges megbízhatósági mutatók, mint as első meghibásodásig tartó várható időtartam számításához egy alacsonyabb szintű, matematikailag kezelhető analízis modellt kell származtatni. Az analízis modell elkészítésekor és elemzésekor felvetődő probléma az állapottérrobbanás: bár a magas szintű mérnöki modell még kezelhető méretű, a hozzá tartozó analízis modell mérete ennek exponenciális függvénye. Így az elterjedt explicit elemzési módszerek csak korlátozottan skálázhatóak.
A probléma egy lehetséges megoldása, hogy az elemzés során megoldandó lineáris egyenletrendszert tenzorreprezentációs módszerek segítségével, tömör közelítő formában tároljuk, és a megoldást is ebben a formában keressük. Munkám során a Tensor Train (TT) formátumú reprezentáció alkalmazhatóságát vizsgálom a hibafák elemzésére, melyet a szimbolikus modellellenőrzésben elterjedt döntési diagram állapottér reprezentáció segítségével állítok elő.
A számítások elvégzéséhez több különböző iteratív algoritmus áll rendelkezésre TT formátumú egyenletrendszerek megoldására. Munkám során ezeket hasonlítom össze, valamint egészítem ki a hibafákból származó problémák megoldására.
Az elméleti eredmények helyességét különböző, nagy méretű hibafákon végzett mérésekkel támasztom alá, nemcsak az iteratív TT algoritmusok, hanem a széles körben alkalmazott explicit módszerek felhasználásával is.
szerző
-
Szekeres Dániel
Mérnök informatikus szak, alapképzés
alapképzés (BA/BSc)
