Abstrakt
Aplikace model checkingu na izolované softwarové komponenty není přímo možná, protože komponenta netvoří kompletní program - nastává problém chybějícího prostředí. Řešením je vytvoření nějakého prostředí pro komponentu, kterou chceme ověřovat. Protože nejobecnější možné prostředí může způsobit nezvladatelnost ověřování komponenty, modelujeme prostředí na základě specifického kontextu, ve kterém se komponenta použije.
Konkrétně, naše řešení využívá hierarchickou komponentovou architekturu a specifikaci chování komponenty definovanou pomocí protokolů chování, všechno poskytované v ADL. Prostředí pak reprezentuje chování zbytku aplikace vzhledem k cílové komponentě.
Zpráva dále popisuje algoritmus pro výpočet modelu chování pro prostředí, který je založen na syntaktické expanzi a substituci protokolu chování.