Inductive Validity Cores

Abstract

Symbolic model checkers can construct proofs of properties over very complex models. However, the results reported by the tool when a proof succeeds do not generally provide much insight to the user. It is often useful for users to have traceability information related to the proof: which portions of the model were necessary to construct it. This traceability information can be used to diagnose a variety of modeling problems such as overconstrained axioms and underconstrained properties, and can also be used to measure completeness of a set of requirements over a model. We propose the notion of inductive validity cores (IVCs), which are intended to trace a property to a minimal set of model elements necessary for proof. Such cores are not unique, and algorithms for efficiently producing both single IVC and all IVCs are pre- sented. IVCs can be used for several interesting analyses, including regression analysis for testing/proof, determination of the minimum (as opposed to minimal) number of model elements necessary for proof, the diversity examination of model elements leading to proof, and analyzing fault tolerance.