Experimental research in explicit model checking
Předkládaná práce se skládá z úvodního komentáře a deseti příspěvků. Práce spadá do oblasti formální verifikace počítačových systémů, konkrétně se zabývá metodou explicitního ověřování konečně stavových modelů. Zaměřuje se především na experimentální aspekty výzkumu v této oblasti, a to jak na obecn...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2010
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/do/rect/habilitace/1433/18215901/ |
| Shrnutí: | Předkládaná práce se skládá z úvodního komentáře a deseti příspěvků. Práce spadá do oblasti formální verifikace počítačových systémů, konkrétně se zabývá metodou explicitního ověřování konečně stavových modelů. Zaměřuje se především na experimentální aspekty výzkumu v této oblasti, a to jak na obecné metodické úrovni (např. vyhodnocení dosavadního experimentálního výzkumu v oblasti), tak v oblasti konkrétního experimentálního vyhodnocení algoritmů. Na základě těchto výsledků pak jsou navrhnuty nové postupy verifikace. Výchozím bodem práce je srovnávací sbírka modelů BEEM - BEnchmarks for Explicit Model checkers. Tato sbírka jednak představuje samostatný důležitý výstup, který se setkal s dobrým přijetím mezi výzkumníky zabývajícími se explicitním ověřováním modelů (BEEM byl během 3 let použit ve více než 30 recenzovaných publikacích), a také tvoří základ, na kterém staví další příspěvky obsažené v práci. S využitím této sbírky modelů byly provedeny anylýzy vlastností prakticky používaných modelů (viz příspěvky Properties of State Spaces and Their Applications, Model Classifications and Automated Verification, and Estimating State Space Parametres) a porovnání různých algoritmů pro explicitní ověřování modelů (viz příspěvky Evaluation of State Caching and State Compression Techniques, Complementarity of Error Detection Techniques, and Fighting State Space Explosion: Review and Evaluation). The thesis consists of an introductory commentary and ten papers. Reported research falls within the general area of formal verification. More specifically the research deals with the explicit model checking technique for finite state systems with focus on experimental aspects of research. It contains both general methodological discussions (e.g., evaluation of use of benchmarking examples) and specific experimental comparisons of algorithms. These results serve as a basis for proposal of new methods and tools. The keystone of this work is the BEEM project: BEnchmarks for Explicit Model checkers. This benchmark set is an important output of the research in itself - in 3 years since it publication, BEEM was used in more than 30 research publications. The benchmark set also serves as a basis for follow-up research reported in the thesis. The set was used to analyze properties of practically used models and their state spaces (as reported in papers Properties of State Spaces and Their Applications, Model Classifications and Automated Verification, and Estimating State Space Parametres) and to experimentaly compare different algorithms for explicit model checking (as reported in papers Evaluation of State Caching and State Compression Techniques, Complementarity of Error Detection Techniques, and Fighting State Space Explosion: Review and Evaluation). |
|---|---|
| Fyzický popis: | ix, 158 s. |