Reduction and Abstraction Techniques for Model Checking
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 pra...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2006.
|
| Témata: | |
| On-line přístup: | Elektronická verze přístupná pouze pro studenty a pracovníky MU |
| Shrnutí: | 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 ab. |
|---|---|
| Popis jednotky: | Vedoucí práce: Ivana Černá. |
| Fyzický popis: | ix, 160 s. + CD-ROM. |