Finding Environment Guarantees
When model checking a software component, a model of the environment
in which that component is supposed to run is constructed. One of the
major threats to the validity of this kind of analysis is the
correctness of the environment model. In this paper, we identify and
formalize a problem related to environment models ---
environment guarantees. It captures those cases where the
correctness of the component under analysis is due solely to the model
of its environment. Environment guarantees provides a model-based
analog to a property-based notion of vacuity by identifying
cases when the component is irrelevant to satisfaction of a property.
The paper also presents a model checking technique for the detection
of environment guarantees. We show the effectiveness of our technique
by applying it to a previously published study of TCAS II, where it
finds a number of environment guarantees.