Specification and Generation of Environment for Model Checking of Software Components

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 an environment of the component which is the intended subject to model checking. We present our approach to automated environment generation that is based on behavior protocols [Plasil, F., and S. Visnovsky, Behavior Protocols for Software Components, IEEE Transactions on Software Engineering, 28(2002)]; to our knowledge, this is the only environment generator designed for model checking of software components. We compare it with the approach taken in the Bandera Environment Generator tool [Tkachuk, O., M. B. Dwyer and C. S. Pasareanu, Automated Environment Generation for Software Model Checking, 18th IEEE International Conference on Automated Software Engineering (ASE03), p. 116, 2003], designed for model checking of sets of Java classes.