Experimental research in explicit model checking - Pelánek, Radek, 1980- (2010)
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).