Abstrakt
S rostoucí popularitou tvorby aplikací skládáním ze znovupoužitelných komponent je stále více třeba zajišťovat korektnost výsledné aplikace. Na jedné straně toto vyžaduje formální popis komponent.
Na straně druhé pak existenci patřičných nástrojů. V tomto článku popisujeme formalismus Extended Behavior Protocols a nástroje pro verifikaci korektnosti komponentové aplikace.
Výhodou zvoleného přístupu je použití dobře testovaného model checkeru Spin. Zmiňujeme také naše zkušenosti s aplikací popsaného postupu a nástroje.