Publikace na Matematicko-fyzikální fakulta |
2010
Abstrakt
Model checkery software jsou používány hlavně pro objevení určitých chyb v kódu, protože kompletní verifikace složitých programů není možná kvůli explozi stavů. Navíc typické model checkery nemohou být použity na izolované komponenty jako knihovny a třídy.
Běžné řešení je vytvořit abstraktní prostředí pro komponentu. V tomto článku prezentujeme metodu, která umožnuje objevit aspoň nějaké chyby souběžnosti v kódu komponenty v rozumném čase.
Hlavní myšlenky jsou (i) použití abstraktního prostředí, které provádí náhodné sekvence metod v každém vlákně, a (ii) restarty procesu hledání chyb podle určité strategie.