Dovoľujeme si oznámiť, že dňa
17. 2. 2006 o 11.30 hod.
sa uskutoční na Fakulte informatiky a informačných technológií STU v Bratislave
v miestnosti D220 obhajoba dizertačnej práce
Ing. Martina Kardoša
Názov dizertačnej práce:
Automatizovaná formálna verifikácia UML návrhov vnorených systémov
Odbor: 25-21-9 Počítačové prostriedky a systémy
Školiteľ: prof. Ing. Norbert Frištacký, PhD., FIIT STU v Bratislave
Oponenti dizertačnej práce:
prof. Dr. rer. nat. Franz Jozef Rammig, Universität Paderborn, Germany
prof. Ing. Mária Bieliková, PhD., FIIT STU v Bratislave
prof. RNDr. Milan Češka, CSc., VUT v Brne
Abstrakt:
Hlavným cieľom dizertačnej práce bolo vyvinúť metódu umožňujúcu plne automatizovanú formálnu verifikáciu vnorených systémov (so zameraním sa na vnorené softvérové systémy) modelovaných a navrhnutých v jazyku UML. Pre dosiahnutie tohto cieľa boli realizované ďalej popísané úlohy.
Najprv bolo potrebné zanalyzovať špecifikáciu UML 2.0 a identifikovať vhodnú podmnožinu jazyka, ktorá umožní modelovanie hlavných aspektov vnoreného systému. Výsledkom tejto analýzy bola podmožina UML jazyka označená ako Verifiable UML obsahujúca diagramy pre modelovanie štruktúry systému ako diagram tried (Class diagram) a diagram balíkov (Package diagram), ďalej diagramy pre modelovanie správania ako diagram stavového stroja (State machine diagram) a diagram protokolového stavového stroja (Protocol state machine diagram), a tiež komunikačné primitívy na modelovanie asynchrónnej a synchrónnej komunikácie. Aplikovateľnosť tejto podmnožiny bola overená na príklade produkčného systému, ktorý bol kompletne vymodelovaný použitím Verifiable UML.
Nasledovne bola vypracovaná koncepcia verifikačnej metódy. Navrhnutá metóda pozostáva z dvoch hlavných logických častí, a to časti formalizácie sémantiky UML diagramov obsiahnutých v Verifiable UML a časti samotnej verifikácie aplikovaním techniky model checking-u. Proces formalizácie zahŕňal definíciu transformačných pravidiel na transformáciu štruktúrnych diagramov do štruktúr AsmL jazyka, formálny opis sémantiky behaviorálnych diagramov v AsmL jazyku, formálnu definíciu základných behaviorálnych konceptov pre opis dynamických elementov ako aktívne triedy, komunikačné primitívy, signály, a tiež definíciu celkovej paralelnej exekučnej sémantiky pre aktívne objekty.
Za účelom verifikácie bolo potrebné vyvinúť novú verifikačnú metódu pre verifikáciu AsmL špecifikácií. Vyvinutá metóda sa zakladá na technike model checking-u a umožňuje plne automatickú verifikáciu AsmL špecifikácií voči vlastnostiam opísaných pomocou formúl temporálnej logiky CTL*. Metóda bola následne implementovaná v nástroji AsmL on-the-fly-model checker a overená medzi inými na všeobecne známom probléme jediacich filozofov (Dining Philosophers). Výsledky boli porovnané s existujúcimi model checking nástrojmi.
Dizertačná práca je k nahliadnutiu na Študijnom oddelení FIIT STU.