Specification and Generation . . .

Model checking of isolated software components is inherently not possible because a component does not form a complete program with an explicit starting point. To overcome this obstacle, it is typically necessary to create a model of the environment of the component which is the intended subject of model checking. Two solutions to generating of environment are compared in this technical report: the Bandera Environment Generator tool [2] and our approach based on behavior protocols [1] employed for model checking of components by the Java PathFinder tool [8]