Abstract
When using formal verification on critical software, an important question involves whether we have we specified enough properties for a given implementation model. To address this question, coverage metrics for property-based formal verification have been proposed. Existing metrics are usually based on mutation, where the implementation model is repeatedly modified and re-analyzed to determine whether mutant models are 'killed' by the property set. These metrics tend to be very expensive to compute, as they involve many additional verification problems. This paper proposes an alternate family of metrics that can be computed using the recently introduced idea of Inductive Validity Cores (IVCs). IVCs determine a minimal set of model elements necessary to establish a proof. One of the proposed metrics is both rigorous and substantially cheaper to compute than mutation-based metrics. In addition, unlike the mutation-based techniques, the design elements marked as necessary by the metric are guaranteed to preserve provability. We demonstrate the metrics on a large corpus of examples.
Original language | English (US) |
---|---|
Title of host publication | ASE 2017 - Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering |
Editors | Tien N. Nguyen, Grigore Rosu, Massimiliano Di Penta |
Publisher | Institute of Electrical and Electronics Engineers Inc. |
Pages | 194-199 |
Number of pages | 6 |
ISBN (Electronic) | 9781538626849 |
DOIs | |
State | Published - Nov 20 2017 |
Event | 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017 - Urbana-Champaign, United States Duration: Oct 30 2017 → Nov 3 2017 |
Publication series
Name | ASE 2017 - Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering |
---|
Other
Other | 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017 |
---|---|
Country/Territory | United States |
City | Urbana-Champaign |
Period | 10/30/17 → 11/3/17 |
Bibliographical note
Funding Information:This work was carried out within the HACMS and SOSITE Phase II grants (DARPA FA8750-12-9-0179 and FA8650-16-C-7656)
Keywords
- Coverage
- formal verification
- inductive proofs
- inductive validity cores
- requirements completeness