Absztrakció alapú modellellenőrzési technikák valós idejű rendszerekhez
Kritikus valós idejű rendszerek fejlesztésekor egy kulcsfontosságú kihívás a szoftverrendszerek biztonságának verifikációja. Az ilyen rendszerekkel szemben gyakran szigorú időzítési követelményeink is vannak, melyek megsértése akár életvesztéshez vagy jelentős anyagi károkhoz vezethet. Ezen követelmények kielégítésének biztosítására automatizált modellellenőrzés használható, melyben egy automatizált eszköz ellenőrzi a kívánt biztonsági követelményeket a rendszer egy formális leírásán. Az analízis eredménye egy bizonyíték a rendszer helyességére, vagy pedig egy hibaút, ami ellenpéldaként szolgál.
A modellellenőrzés azonban még közepes méretű rendszerek esetén is nehéz feladat, hiszen a bejárandó állapotok száma gyakran a rendszer méretében exponenciálisan növekszik. Ezen kívül az időzítések figyelembe vételéhez az állapotoknak egy megszámlálhatatlanul végtelen halmazával szükséges dolgozni. A mérnöki alkalmazásokban az imént említett kihívásokkal megbirkózó modern verifikációs algoritmusok használatához a rendszerek és kritériumok komplex leírásait alacsonyszintű matematikai formalizmusokra szükséges fordítani.
Ezen munka célja az absztrakció alapú modellellenőrzés támogatása a széles körben használt időzített automata formalizmushoz és a hozzá tartozó tulajdonság specifikációs nyelvhez. A már létező algoritmusok adaptálása mellett a technikák egy olyan újszerű kombinációjára teszünk javaslatot, mely ötvözi az irodalomban elérhető megközelítések hatékonyságát az adatok és az idő absztrakciójára. Ezen kívül támogatást adunk egy már létező modellellenőrző eszközben az időzített automaták tulajdonság specifikációinak kezelésére.
Különösen a következő kontribúciókat mutatjuk be: (i) Visszavezetjük az időzített automaták elérhetőségi tulajdonságait egy keresési problémára. (ii) Kombináljuk az absztrakciófinomítás lusta és mohó megközelítését egy újszerű vegyes stratégiaként. (iii) Implementáljuk a javasolt technikákat a nyílt forráskódú Theta modellellenőrző keretrendszerben. (iv) Kiértékeljük a létező és az általunk javasolt technikákat ipari és szintetikus benchmark modelleken.
Legjobb tudomásunk szerint a miénk az első olyan megközelítés, ami kombinálja a lusta és mohó absztrakciós technikák előnyeit az időzített automaták hatékony verifikációjára.
szerzők
-
Cziborová Dóra
Mérnök informatikus szak, mesterképzés
mesterképzés (MA/MSc) -
Vizi Béla
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 -
Szekeres Dániel
Doktorandusz, Méréstechnika és Információs Rendszerek Tanszék -
helyezés
Morgan Stanley II. helyezett