The Community for Technology Leaders
2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE) (2017)
Urbana, IL, USA
Oct. 30, 2017 to Nov. 3, 2017
ISBN: 978-1-5386-3976-4
pp: 194-199
Elaheh Ghassabani , Department of Computer Science & Engineering, University of Minnesota, MN, USA
Andrew Gacek , Rockwell Collins, Advanced Technology Center, IA, USA
Michael W. Whalen , Department of Computer Science & Engineering, University of Minnesota, MN, USA
Mats P. E. Heimdahl , Department of Computer Science & Engineering, University of Minnesota, MN, USA
Lucas Wagner , Rockwell Collins, Advanced Technology Center, IA, USA
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.
INDEX TERMS
Measurement, Computational modeling, Software, Safety, Mathematical model, Testing, Analytical models
CITATION

E. Ghassabani, A. Gacek, M. W. Whalen, M. P. Heimdahl and L. Wagner, "Proof-based coverage metrics for formal verification," 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), Urbana, IL, USA, 2017, pp. 194-199.
doi:10.1109/ASE.2017.8115632
91 ms
(Ver 3.3 (11022016))