Abstrakt
Pro analyzu komponent verifikacnimi nastroji je vhodne popsat chovani komponenty pomoci konecne-stavoveho modelu. To je vsak casto nemozne v dobe navrhu komponenty, pokud tato pouziva neomezeny paralelismus.
V tomto pripade totiz chovani komponenty zavisi na prostredi, ve kterem je komponenta pouzivana, a pokryti vsech moznych prostredi pak vede k nekonecne-stavovemu modelu. V tomto clanku navrhujeme reseni tohoto problemu zalozene na myslence transformace sablony chovani na konkretni model (template-to-model transformation): v dobe navrhu komponenty je chovani popsano tzv. sablonou chovani, ktera je automaticky transformovana v konkretni model ve chvili, kdy je komponenta nasazena v konkretnim prostredi.
Tento konkretni model je jiz konecne-stavovy, a je proto vhodnym vstupem verifikacnich nastroju.