Edge Computing szolgáltatások ellenállóképességének modellalapú vizsgálata
Részben a felhőszámítástechnika evolúciójaként, részben pedig az 5G technológiához kapcsolódóan napjainkban kialakulóban van az úgynevezett Edge Computing, azaz a felhőszerű számítástechnikai képességek megjelenése az internet és a “terep” határán. A szolgáltatásbiztonság szempontjából az edge computing újszerű kihívásokat állít a rendszertervezés és szolgáltatásüzemeltetés elé. Dolgozatomban a platform és alkalmazási szintű védelmek megfelelőségét vizsgálom modellelleőrzés segítségével ilyen környezetben.
A tipikus szolgáltatások időkritikusak, továbbá nemcsak klasszikus szolgáltatásbiztonsági követleményekkel rendelkeznek (pl. magas rendelkezésre állás) , de emellett ellenállóképesnek is kell lenniük (resilience): a különböző belső és környezeti hibák hatásából minél kevésbé súlyos szolgáltatási hatású, és minél rövidebb tranziensekkel kell helyreállniuk. Köszönhetően annak, hogy felhőszerűségük miatt az edge platformok dinamikusan újrakonfigurálhatóak (illetve azok lesznek) , éshogy az edge és a felhő között taszkok dinamikusan is mozgathatóak, az újszerű követelmények kielégítésére a dinamikus szolgáltatás rekonfiguráció megfelelő választ adhat. Ehhez azonban kritikus, hogy a platformszintű futásidejű szolgáltatásbiztonsági mechanizmusokat (pl újraindítás vagy beépített terheléselosztás), és az alkalmazási szintű mechanizmusokat (pl. állapotreplikáció, heart-beat, stb.) is magában foglaló védelmi stratégiák helyesek legyenek abban az értelemben, hogy a különböző mechanizmusok együttes működése a különböző hibaokok hatását a követelményeknek megfelelően maszkolja, illetve csillapítsa.
Dolgozatomban a fenti problémára újrahasznosítható állapotgépek kompozíciójával és modellellenőrzésével adok megoldást. Az edge computing a jövőben várhatóan meghatározó platformja, a Kubernetes elemeinek és egészének a működését állapotgépekkel modellezem a Yakindu Statechart Tools keretrendszerben, és a kompozit állapotgépen formális vizsgálatot végzek.
Az újrahasznosítható bemeneti modellek és a leképezési lánc mellett önálló eredményként javaslatokat teszek a modellellenőrzés során tipikusan vizsgált tulajdonságokra.
Munkámban azt is demonstrálom, hogy a kompozit modellek hogyan alkalmazhatóak – autonóm számítástechnika ágens jelleggel – futásidejű állapotdekódolásra és vezérlésre, valamint SCADA-szerű vizuális állapotmegjelenítésre.
