Reduction and Abstraction Techniques for Model Checking

PELÁNEK, Radek. Reduction and Abstraction Techniques for Model Checking. Brno: Masarykova univerzita, 2006, 160 s.

Základní údaje

• Originální název: Reduction and Abstraction Techniques for Model Checking
• Název česky: Redukční a abstrakční techniky pro ověřování modelu
• Autoři: PELÁNEK, Radek.
• Vydání: Brno, 160 s. 2006.
• Nakladatel: Masarykova univerzita

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Odborná kniha
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Česká republika
• Utajení: není předmětem státního či obchodního tajemství
• Organizační jednotka: Fakulta informatiky
• Klíčová slova anglicky: Ph.D. thesis, model checking, abstraction, state space explosion
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

Model checking is an increasingly popular method for verification of safety-critical systems. The main obstacle of this verification method is a state space explosion problem and consequently high computational requirements of model checking algorithms. In order to make the model checking method practically feasible, it is necessary to develop powerful techniques for fighting state space explosion. This thesis is focuses on fighting state space explosion in the context of embedded system verification. Verification of embedded systems is particularly difficult due to intricate interferences of software and real-time aspects of these systems. In this setting, the most useful techniques are abstraction and reduction. These represent the main topics of this thesis. The thesis contributes in several ways to the development of abstraction and reduction techniques, which are both practical and theoretically grounded. Our first contribution is the systematic presentation of reduction and abstraction techniques in a single formal setting. This facilitates understanding and application of these techniques. Our main innovative contribution lies in the novel under-approximation refinement algorithm for software model checking. Similarly to other automatic refinement algorithms, our algorithm is based on predicate abstraction. However, it uses under-approximation refinement instead of the classical over-approximation refinement. The thesis also contains several important technical results about abstraction and reduction techniques. Particularly, we provide two interesting results for timed automata: a decidability result for a non-emptiness problem of timed automata with sampled semantics and a new extrapolation technique for zone based abstractions of timed automata.

Anotace česky

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ů.

Návaznosti

• MSM0021622419, záměr: Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy