Komplex kiberfizikai rendszerek állapotalapú megbízhatósági modelljeinek szimulációja, statisztikai inferenciája és verifikációja
A biztonságkritikus kiber-fizikai rendszereknek, melyek széles körben elterjedtek az olyan terülteken, mint autó-, repülőgép- és atomenergia ipar, a funkcionális követelmények mellett számos extra-funkcionális követelménynek (például biztonság, megbízhatóság, rendelkezésre állás) kell megfelelniük. A különböző szabványok (a autóiparban az ISO 26262, az atomengergia iparban az IEC 61523, illetve más elektronikus eszközöknél az IEC 61508) előírják ezen követelmények ellenőrzését a tervezési folyamat során. A tanúsítványozásnál általában deduktív (top-down) módon vizsgáljuk a rendszer architektúrájának és viselkedéseinek megbízhatóságát.
A rendszerek olyan viselkedéseinek, mint a fejlett hibaelkerülési stratégiáknak, szenzorfúziós algoritmusoknak és adaptív rekonfigurációknak egyre növekvő komplexitása kihívás elé állítja az elemzéseket. A nagy kifejezőerejű modellezési nyelvek mellett hatékony számítási eszközök szükségesek a megbízhatósági metrikák meghatározására.
A modellezési nyelvek közül legtöbbször a hibafákat és dinamikus hibafákat alkalmazzák, ám ezek csak korlátozottan alkalmasak belső állapottal rendelkező komponensek leírására. Az állapotalapú nyelvek (Markov-láncok, sztochasztikus Petri hálók) alacsony absztrakciós szintjük miatt speciális szaktudást igényelnek. Az AADL Error-Model Annex ezzel szemben egy, a rendszertervezési folyamathoz jobban illeszkedő modellezési módszert nyújt egymással kommunikáló állapotgépekre támaszkodva.
Az olyan számítási eszközök, mint a PRISM Model Checker vagy a GreatSPN az állapottér-robbanás jelenségével szembesülnek a nagy méretű modelleknél, valamint csak bizonyos hibaeloszlásokat támogatnak. A statisztikai módszerek, mint az UPPAAL-SMC jobban skálázhatóak, ám a mintavételezési eljárásaik pontossága csökkenhet a feltételes eloszlások számításánál és a kis valószínűségű eseményeknél.
Munkámban egy olyan megbízhatósági modellezési módszert javasolok, mely egy kommunikáló állapottérképekre épülő modellezőeszköz, a Gamma Statechart Composition Framework felhasználásával teszi lehetővé a hibaterjedési modellek elkészítését és formális analízisét. Így, kiterjesztve az AADL Error-Model Annex elveit, lehetővé válik olyan, az állapottérképekből megismert elemek használata, mint a hierarchikus állapotok (hibák), illetve a (szenzorfúziós algoritmusokat leíró) változók és akciók. A deduktív analízis mellett kidolgoztam a modellek transzformációját a Pyro mély probabilisztikus programozási környezetbe, mellyel a szimuláció, statisztikai elemzés és inferencia a legújabb feltételes mintavételezési algoritmusokkal végezhető el. Így megoldásom képes tetszőleges hibaeloszlások, kis valószínűségű és feltételes események kezelésére.
Módszerem alkalmazhatóságát egy autóipari projektből vett esettanulmányon keresztül mutatom be. A hibák, hibaterjedési és -elkerülési mechanizmusok modellezése mellett a rendszer megbízhatóságát deduktív módszerekkel és a Pyro algoritmusaival vizsgálom. Így elvégezhető a szokásos megbízhatósági elemzés, feltételes elemzés, valamit a kritikus komponenseket meghatározó Pareto-elemzés.
szerző
-
Nagy Simon József
Villamosmérnöki szak, alapképzés
alapképzés (BA/BSc)
