Abstract
Application of model checking to isolated software components is not directly possible because a component does not form a complete program - the problem of missing environment occurs. A solution is to create an environment of some form for the component subject to model checking.
As the most general environment can cause model checking of the component to be infeasible, we model the environment on the basis of a particular context the component is to be used in. More specifically, our approach exploits hierarchical component architecture and component behavior specification defined via behavior protocols, all that provided in ADL.
This way, the environment represents the behavior of the rest of the particular application with respect to the target component. We present an algorithm for computing the model of environment?s behavior that is based on syntactical expansion and substitution of behavior protocols.