Hierarchikus állapottérképek absztrakció-alapú ellenőrzése

OData támogatás
Konzulens:
Hajdu Ákos
Méréstechnika és Információs Rendszerek Tanszék

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 precizitással 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 egyszerű á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 solver-ek 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 általában 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ókra építve akár komplex állapottérképek ellenőrzését is lehetővé teszi. Az elkészített algoritmusok hatékonyságát egy ipari példán demonstrálom illetve hasonlítom össze.

Letölthető fájlok

A témához tartozó fájlokat csak bejelentkezett felhasználók tölthetik le.