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 ve volacím protokolu na základě informací poskytnutých statickou analýzou, která hledá v kódu komponenty vzory se vztahem k synchronizaci; pomocí heuristiky se některé patterny označí jako podezřelé. Potom se prostředí (potřebné, protože Java PathFinder ověřuje pouze kompletní Java programy) vygeneruje z redukovaného volacího protokolu tak, že se paralelně provádějí pouze ty části kódu komponenty, které pravděpodobně obsahují synchronizační chyby.