Abstrakt
Formální verifikace chování komponentových aplikací vyžaduje vhodný specifikační jazyk. Je nezbytné, aby tento jazyk umožňoval zachytit důležité aspekty chování budoucí implementace ve vztahu k požadovaným vlastnostem.
Bylo ukázáno, že behavior protocols jsou vhodnou specifikační platformou pokud se návrhář aplikace soustřeďuje na absenci komunikačních chyb. V této práci navrhujeme nový specifikační jazyk založený na jazyku Behavior protocols a řešíme problém nízké efektivity verifikačního nástroje BPChecker pro jejich ověřování. Rozšíření jazyka byla motivována zkušenostmi z aplikace BP na případovou studii popisující skutečnou aplikaci.
Navrhovaná rozšíření sestávají z prostředků pro reprezentaci parametrů metod, lokálních proměnných, synchronizace a specifikace cyklů. Pro řešení problému efektivity ověřovacího nástroje navrhujeme transformaci BP do jazyka Promela, což umožňuje použití nástroje Spin.