Valós idejű szoftverintenzív rendszer modellek absztrakció alapú modellellenőrzése
A valós idejű szoftverintenzív rendszerek biztonságának biztosítása kulcsfontosságú számos kritikus alkalmazásban, mint az automatikus vezetéstámogató rendszerek, vasúti rendszerfigyelők, okos városok. A formális verifikációs módszerek, mint az automatizált modellellenőrzés matematikailag precíz bizonyítékot adhatnak a rendszerek helyességére a biztonságos működés érdekében.
A valós idejű időzítési követelmények és a bonyolult időbeli viselkedések megnehezítik a valós idejű szoftverintenzív rendszerek verifikációját. Ezek a rendszerek tartalmaznak továbbá külső adatokkal, például beérkező szenzor adatokkal végzett számításokat, melyek erősen adatfüggő viselkedéseket eredményeznek. Emiatt kétféle kihívással is találkozunk: (1) a szoftverek fejlesztéséhez gyakran összetett eszközök szükségesek, mint például az állapottérkép alapú modellezőeszközök a viselkedés megfelelő kifejezőerejű leírásához, valamint (2) a formális verifikációt hátrátatja az esetleges időzítések és bejövő adatok által okozott állapottér-robbanás.
Az utóbbi probléma ellensúlyozására az irodalomban absztrakció alapú modellellenőrző eszközök kerültek kifejlesztésre. Korábbi munkám során kifejlesztettem absztrakció alapú algoritmusok egy olyan kombinációját, mely képes az időzített viselkedések és összetett bejövő adatok egyidejű kezelésére. Az időzített modellellenőrzésben használt alacsonyszintű formalizmusok azonban nem rendelkeznek kellő kifejezőerővel a magasszintű modellező eszközökből származó rendszer modellek reprezentálására. Bár az időzített viselkedés diszkrét közelítése elterjedt megoldás az olyan, kifejezőbb verifikációs algoritmusok használatának lehetővé tételére, melyek natívan nem támogatják az időzített viselkedést, ezzel a diszkretizáció hibája miatt elveszhet a helyesség.
A dolgozat célja egy köztes formalizmus javaslata a valós idejű rendszer modellek reprezentálására, valamint ehhez a formalizmushoz létező absztrakció alapú modellellenőrző algoritmusok adaptálása. Ehhez (i) javasolok egy kiterjesztést a Gamma állapottérkép alapú modellezőeszközben köztes modellként használt kiterjesztett szimbolikus tranzíciós rendszer (XSTS) formalizmushoz, hogy lehetővé tegyem időzített rendszerek leírását, kihasználva a Gamma és az XSTS létező képességeit az összetett adatvezérelt viselkedés és a rendszer komponensek közti kommunikáció reprezentálására. Ezen kívül (ii) absztrakció alapú modellellnőrzési megközelítéseket adaptálok az időzített XSTS modellek verifikációjára, beleértve (iii) a komponensek kommunikációja és a hierarchikus modellezés által okozott összetett vezérlési folyamok kezelését a kombinált verifikációs algoritmusomban. Továbbá, (iv) az időzített XSTS formalizmust és a verifikációs algoritmusokat implementálom a nyílt forráskódú Theta verifikációs keretrendszerben. Végül (v) a javasolt megközelítéseket ipari projektetből származó esettanulmányokon és szintetikus benchmark modelleken értékelem ki.
Munkám eredményeképp lehetővé válik az összetett valós idejű szoftverintenzív rendszerek verifikációja a kifejezőerő korlátozása és diszkretizációs hiba nélkül.
szerző
-
Cziborová Dóra
Mérnök informatikus szak, mesterképzés
mesterképzés (MA/MSc)
konzulensek
-
-
Dobos-Kovács Mihály
doktorandusz, Méréstechnika és Információs Rendszerek Tanszék
