Abstrakt
Formální verifikace hierarchických komponentových aplikací zahrnuje (i) ověřování korektnosti komunikace mezi sub-komponentami každé složené komponenty, a (ii) ověřování implementace každé primitivní komponenty proti její specifikaci chování a dalším vlastnostem jako absence chyb souběžnosti. V této práci se zaměřujeme na verifikaci primitivních komponent implementovaných v jazyce Java proti vlastnostem dodržování specifikace chování definované ve formalismu behavior protocols a absence chyb souběžnosti.
Používáme Java PathFinder model checker jako hlavní nástroj pro verifikaci. Navrhujeme množinu technik, které řeší hlavní problémy formální verifikace realistických komponent v jazyce Java pomocí techniky model checking: podpora pro vysoko-úrovňovou vlastnost dodržování specifikace chování, modelování a konstrukce prostředí, a stavová exploze.
Techniky zahrnují (1) rozšíření nástroje Java PathFinder, který umožňuje ověřování Java kódu proti frame protokolu, (2) automatické generování prostředí pro kom