Időzített rendszerek CEGAR alapú analízise

OData támogatás
Konzulens:
Vörös András
Méréstechnika és Információs Rendszerek Tanszék

A napjainkban egyre inkább elterjedő biztonságkritikus rendszerek hibás működése súlyos károkat okozhat, emiatt kiemelkedően fontos a matematikailag precíz ellenőrzési módszerek alkalmazása a fejlesztési folyamat során. Ennek egyik eszköze a formális verifikáció, amely már a fejlesztés korai fázisaiban képes felfedezni tervezési hibákat. A biztonságkritikus rendszerek komplexitása azonban gyakran megakadályozza a sikeres ellenőrzést, ami különösen igaz az időzített rendszerekre: a lehetséges állapotok és átmenetek halmaza (állapottér) akár kisméretű rendszerek esetén is hatalmas, vagy akár végtelen nagy is lehet. Ezért kiemelkedően fontos a megfelelő modellezőeszköz valamint hatékony verifikációs algoritmusok kiválasztása. Az egyik legelterjedtebb formalizmus időzített rendszerek leírására az időzített automata, ami a véges automata formalizmust óraváltozókkal egészíti ki, lehetővé téve az idő múlásának reprezentálását a modellben.

A formális verifikáció egyik alapvető feladata az állapotelérhetőségi analízis, amely során azt vizsgáljuk, hogy lehetséges-e, hogy a rendszer működése során elér egy adott hibaállapotba. A probléma komplexitása már egyszerű (diszkrét változó nélküli) időzített automaták esetén is exponenciális, így nagyméretű modellekre ritkán megoldható. Ezen probléma leküzdésére nyújt egy lehetséges megoldást az absztrakció módszere, amely a releváns információra koncentrálva próbál meg egyszerűsíteni a megoldandó problémán. Az absztrakció-alapú technikák esetén azonban a fő probléma a megfelelő pontosság megtalálása. Az ellenpélda vezérelt absztrakciófinomítás (counterexample-guided abstraction refinement, CEGAR) iteratív módszer, amely a rendszer komplexitásának kézben tartása érdekében egy durva absztrakcióból indul ki és ezt finomítja a kellő pontosság eléréséig.

Munkám célja hatékony algoritmusok fejlesztése időzített rendszerek verifikációjára. Munkám során időzített automatákra alkalmazott CEGAR-alapú elérhetőségi algoritmusokat vizsgálok, fejlesztek és közös keretrendszerbe foglalom őket, ahol az algoritmusok komponensei egymással kombinálva új, hatékony ellenőrzési módszerekké állnak össze. A keretrendszer a CEGAR módszer kétféle megvalósítását is lehetővé teszi: az egyik az elérhető állapotok halmazának (az állapottérnek) felülbecsléséhez az automatát egyszerűsíti, míg a másik közvetlenül az állapottéren alkalmaz absztrakciót.

A kifejlesztett algoritmusok hatékonyságát méréseken keresztül demonstrálom, amelyek bemeneteit időzített automáták modellellenőrzésére kifejlesztett algoritmusok összehasonlító elemzéséhez gyakran használt modellek közül választottam.

Letölthető fájlok

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