Absztrakció alapú algoritmusok konfigurálható automataelméleti modellellenőrzéshez
A mindennapi életünk kritikus rendszereken alapszik: ebbe beletartoznak járművek, az energetikai és közlekedési hálózatok, digitális infrastruktúrák. Ezen rendszerek megbízhatósága és biztonsága létfontosságú, mivel még a legkisebb észrevétlen hibák is katasztrofális következményekkel járhatnak, szélsőséges esetekben emberéletekbe is kerülhetnek. A modellellenőrzés lehetővé teszi a tervezőmérnököknek, hogy szigorúan elemezzék és ellenőrizzék ezeket a rendszereket helyességük és megbízhatóságuk biztosítása érdekében. A kritikus rendszerek matematikai modellezésével és ezek kimerítő vizsgálatával a modellellenőrzés segít azonosítani a potenciális hibákat a fejlesztés korai szakaszában.
A Lineáris Temporális Logika (LTL) egy erős követelményspecifikációs nyelv a kritikus rendszerek számára. Az LTL nemcsak elérhetőségi feltételeket, hanem dinamikus tulajdonságokat is képes kifejezni, például összetett élőségi és stabilizációs követelményeket. Az LTL modellellenőrzés legelterjedtebb megoldása az automatelméleten alapul.
A modellellenőrzés gyakorlati alkalmazását az állapottér-robbanás problémája hátráltatja: a lehetséges állapotok száma akár exponenciális is lehet a változók számában. Egy gyakran alkalmazott megoldás az állapottér csökkentése absztrakció segítségével. Azonban az absztrakció potenciális alkalmazása az automatelméleti modellellenőrzés hatékonyságának növeléséhez még nincs kimerítően feltérképezve a szakirodalomban.
Dolgozatomban hatékony moduláris automatelméleti modellellenőrzési algoritmusokat és fogalmakat mutatok be, amelyeket alapvető építőelemként lehet felhasználni magasabb szintű absztrakció alapú algoritmusokhoz. (1) Bemutatok egy hatékony új nyelvi üresség ellenőrző algoritmust, és összehasonlítom annak teljesítményét egy másik, a szakirodalomban megtalálható megközelítéssel. (2) Leírok egy új absztrakció finomítási algoritmust, és összehasonlítom azt egy, a szakirodalomban fellelhetővel. (3) Bővítem a nyílt forráskódú Theta modellellenőrzési keretrendszert egy új kombinált formalizmussal, amelyet használhatunk tetszőleges számú címkézett állapotátmeneti rendszer szorzatának előállításához. A bemutatott algoritmusok moduláris jellegét azzal demonstrálom, hogy egy kibővített ellenpélda-vezérelt absztrakció finomítási algoritmussá kombinálom őket, amely képes LTL tulajdonságok ellenőrzésére. Az algoritmusokat a nyílt forráskódú Theta modellellenőrzési keretrendszerben implementáltam, majd ipari partnerek által biztosított esettanulmányokon értékeltem ki, mely során teljesítményük ígéretesnek bizonyult.
szerző
-
Rippl Balázs Róbert
Mérnök informatikus szak, alapképzés
alapképzés (BA/BSc)
konzulensek
-
-
Szekeres Dániel
Doktorandusz, Méréstechnika és Információs Rendszerek Tanszék