Lusta absztrakciófinomítás algoritmusok általánosítása részbenrendezésekkel
Kritikus valósidejű rendszerek fejlesztésében egy kulcsfontosságú kihívás a szoftver-rendszerek biztonságának verifikációja. Az automatizált modellellenőrzésben a rendszernek egy formális leírásán kerülnek ellenőrzésre a kívánt biztonsági követelmények, egy automatizált eszköz által. Az analízis kimenetele lehet egy bizonyítás a rendszer helyességére, vagy pedig egy hibaút, ami a helyesség ellenpéldájaként szolgál.
A modellellenőrzés sajnos akár már közepes méretű rendszereken végezve is algoritmikusan nehéz feladat lehet. A modellellenőrzés során bejárnandó állapotok száma véges számú lehetséges viselkedéssel rendelkező rendszerek esetén is gyakran a rendszer méretében exponenciálisan nő. 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.
Az állapottér kompakt reprezentációjára számos absztrakció alapú módszer létezik az irodalomban. Ezen módszerek között a lusta absztrakció és változatai egy hatékony megoldást nyújtanak az időzített modellek analízisére. A vizsgált programok változatos tulajdonságai szükségessé teszik a különböző fajta lusta absztrakciókat. Ezek között nem létezik egyetlen legjobb algoritmus, így szükség van egy konfigurálható lusta absztrakció alapú keretrendszerre a lehetséges megközelítések általánosításaként.
Munkám során a részbenrendezések és Galois kapcsolatok elméletét alkalmazva egy konfigurálható lusta absztrakció alapú keretrendszer kidolgozását céloztam meg. Ezen belül is (i) definiálok egy általános lusta absztrakciófinomítási (elméleti) keretrendszert, (ii) integrálom a létező lusta absztrakciós módszereket a keretrendszerbe, (iii) új kombinációit és konfigurációit nyújtom a lusta absztrakciós módszereknek, valamint (iv) implementálok egy lusta absztrakció alapú modellellenőrző megközelítést a nyílt forráskódú Theta eszközben. Az algoritmusok alkalmazhatóságát benchmark modelleken értékeljük ki.
