Abstract The inferences which can validly be drawn about a software system based on reasoning about a model of the system depend on the precise relationship between the system and the model. Formal properties of a variety of such modeling relationships are examined, particularly relationships in which, if a given computation is possible in the system, the corresponding computations (if any) are also possible in the model. Therefore, if a particular (perhaps undesirable) computation is not possible in the model, no corresponding computation is possible in the original system. Inferences like these can be used to show, for example, that a particular error is absent from the original system if it is not manifested in the model. It is shown that many modeling techniques that are intuitively rather natural and easy to describe are of this kind.