Symbolic model checkers can construct proofs of properties over highly 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, measure completeness of a set of requirements over a model, and assist with design optimization given a set of requirements for an existing or synthesized implementation. In this paper, we present a comprehensive treatment of a suite of algorithms to compute inductive validity cores (IVCs), minimal sets of model elements necessary to construct inductive proofs of safety properties for sequential systems. The algorithms are based on the UNSAT core support built into current SMT solvers and novel encodings of the inductive problem to generate approximate and guaranteed minimal inductive validity cores as well as all inductive validity cores. We demonstrate that our algorithms are correct, describe their implementation in the JKind model checker for Lustre models, and present several use cases for the algorithms. We then present a substantial experiment in which we benchmark the efficiency and efficacy of the algorithms.
Bibliographical noteFunding Information:
This work was sponsored by the DARPA Systems of Systems Integration Technology and Experimentation phase 2 project (contract: FA8650-16-C-7656) as well as the NASA Compositional Verification of Flight-Critical Systems (contract: NNA13AA21C). We would like to thank Mona Rahimi for discussions that led to the initial IVC idea, John Backes and Anitha Murugesan for discussions on various aspects of IVCs, and Lucas Wagner for his work integrating them into the Spear requirements tool.
© 1976-2012 IEEE.
- Inductive validity cores
- proof explanation
- requirements analysis
- SMT-based model checking