From Model Checking to a Temporal Proof for Partial Models

Three-valued model checking has been proposed to support verification when some portions of the model are unspecified. Given a formal property, the model checker returns true if the property is satisfied, false and a violating behavior if it is not, maybe and a possibly violating behavior if it is possibly satisfied, i.e., its satisfaction may depend on how the unspecified parts are refined. Model checking, however, does not explain the reasons …