Abstrakt
Jedna z výzev v oboru verifikace softwarových komponent je model checking izolovaných komponent. Prostředí izolované komponenty je neznámé, a proto chybí část vstupu model checkeru.
Tento problém může být řešen pomocí automatického generování umělého prostředí - komponenta a její prostředí tvoří kompletní program, který může být verifikován běžnými model checkery. Omezujíc se na chyby souběžnosti v Java komponentách, navrhujeme automaticky generovat rozumné umělé prostředí, které umožňuje efektivní detekci chyb souběžnosti s nástrojem Java PathFinder.
Takové prostředí vykonává paralelně ty metody komponent, které interagují přes konstrukty souběžnosti v jazyce Java a tedy pravděpodobně obsahují chyby souběžnosti. Používáme statickou analýzu kódu pro určení množin metod, které mají být vykonávány paralelně, a metriku pro seřazení množin podle stupně interakce.
Výhody techniky jsou ilustrovány na výsledcích experimentů provedených na realistických Java komponentách.