Reduction and Abstraction Techniques for Model Checking

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Redukční a abstrakční techniky pro ověřování modelu
Autoři

PELÁNEK Radek

Rok publikování 2006
Druh Odborná kniha
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Popis Ověřování modelu je stále oblíbenější metodou pro verifikaci systémů, které jsou bezpečnostně kritické. Hlavní překážkou této verifikační metody je problém stavové exploze a následně vysoká výpočetní náročnost algoritmů pro ověřování modelu. Abychom učinili metodu ověřování modelu prakticky použitelnou, je nezbytné vyvíjet účinné techniky pro boj se stavovou explozí. Tato práce se zaměřuje na boj se stavovou explozí v kontextu verifikace vestavěných systémů. Verifikace vestavěných systémů je obzvláště náročná díky složitým kombinacím softwarových a časových aspektů těchto systémů. Nejužitečnějšími technikami jsou v tomto případě techniky abstrakční a redukční. Tyto techniky jsou hlavním tématem této práce. Práce přispívá k vývoji abstrakčních a redukčních technik, které jsou jak prakticky užitečné, tak teoreticky dobře podložené. Prvním přínosem je systematická prezentace redukčních a abstrakčních technik v jednotném formalismu. Tato prezentace usnadňuje porozumnění a aplikaci popsaných technik. Hlavním inovačním přínosem je nový algoritmus pro oveřování modelů softwaru, který je založen na zjemňování aproximací. Podobně jako ostatní algoritmy pro automatické zjemňování aproximací, nový algoritmus je založen na výrokové abstrakci. Ovšem narozdíl od klasických algoritmů založených na aproximacích zhora, nový algoritmus používá aproximace zdola, což umožňuje rychlejší detekci chyb. Práce také obsahuje několik důležitých technických výsledků o abstrakčních a redukčních technikách. Zejména prezentuje dva zajímavé výsledky o časových automatech: rozhodnutelnost problému neprázdnosti časových automatů ve vzorkovací sémantice a novou extrapolační techniku pro abstrakce časových automatů.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.