Abstrakt
Při model checkingu kódu softwarových komponent, které se vyznačují vysokou úrovní paralelismu, se často vyskytne problem exploze stavového prostoru, bez ohledu na to, že jedna komponenta má obvykle menší stavový prostor než celý systém. Zde prezentujeme techniku, která adresuje problém exploze stavového prostoru pro ověřování kódu primitivních komponent s Java PathFinder v případě, že ověřovaná vlastnost je absence synchronizačních chyb.
Klíčová myšlenka je redukce paralelismu v prostředí komponenty tak, že pouze ty části kódu komponenty, které pravděpodobně mohou vyvolat synchronizační chybu, jsou vykonány paralelně; takové části jsou identifikovány pomocí heuristické statické analýzy kódu (hledáním podezřelých vzorů v kódu komponenty). Výhody této techniky, t.j. podpora objevení synchronizačních chyb v omezeném čase a prostoru a reportování čitelnějších protipříkladů, jsou ilustrovány na výsledcích několika experimentů.