Hierarchikus absztrakció alkalmazása állapot alapú rendszerek ellenőrzésére
Napjainkban a beágyazott rendszerek az élet minden területén egyre nagyobb teret nyernek, így helyességük ellenőrzése is egyre fontosabb, ugyanis kritikus esetben vállalatok sorsa vagy akár emberi élet is múlhat rajta. Ennek egyik fontos eszköze a formális verifikáció, melynek segítségével matematikai alapokon lehet a modellek helyességét már a tervezési fázisban vizsgálni.
A hierarchikus állapottérképek a viselkedésmodellek egyik gyakran használt eszközeként a mérnöki tervezés alapjául szolgálnak, verifikációjuk ezért kiemelt jelentőséggel bír. Gyakran azonban egy önmagában álló állapottérkép ellenőrzése is nehéz feladat, ugyanis a változók számával exponenciálisan növekvő állapottér megakadályozhatja a sikeres verifikációt. Az állapottér hatékony kezelésére és bejárására az irodalomban többféle algoritmust is kidolgoztak. Ezek közül az egyik legelterjedtebb a korlátos állapotelérhetőségi analízis, amelyet leggyakrabban logikai megoldók, azaz SAT/SMT solverek segítségével valósítanak meg. Ehhez az állapotgépet logikai formulákkal írják le (elkódolás), majd ezeket a formulákat adják be a megoldóknak.
Gyakran azonban ezek az algoritmusok sem tudnak megbirkózni a komponensmodellekben használt változatos adattípusok és konstrukciók okozta komplex viselkedésekkel. A nagyméretű állapottér által jelentett komplexitás csökkentésére megoldást jelenthet az absztrakció alkalmazása, amely azonban elrejthet az ellenőrzés sikerességéhez elengedhetetlen részleteket. Ilyenkor finomítani kell az absztrakciót és gazdagítani a reprezentált információt. Ezen elv mentén működik az ellenpélda alapú absztrakciófinomítás (CounterExample-Guided Abstraction Refinement, CEGAR) módszere.
A gyakorlatban használt verifikációs eszközök nem használják ki az állapottérképekben levő hierarchiát. Dolgozatomban a célom olyan algoritmusok fejlesztése, amelyek hatékonyan tudják kezelni a hierarchikus állapottérképeket, továbbá ki tudják használni a verifikáció során a hierarchiában rejlő extra információt. Bemutatok egy általam tervezett módszert, amely lehetővé teszi komplex állapottérképek hatékony elkódolását logikai formulákká a hierarchia kihasználásával. Ezt továbbfejlesztve egy olyan absztrakciófinomításon (CEGAR) alapuló algoritmust ismertetek, amely az állapotok közötti hierarchiát felhasználja a finomítás során, és különböző logikai megoldókat felhasználva akár komplex állapottérképek ellenőrzését is lehetővé teszi. Az elkészített algoritmusok használhatóságát mérésekkel demonstrálom.
szerző
-
Czipó Bence
Mérnök informatikus szak, alapképzés
alapképzés (BA/BSc)
konzulensek
-
Dr. Hajdu Ákos
Software engineer, Meta (külső) -
