caa a22 4500 605495572 CHVBK 20210128100532.0 cr unu---uuuuu 210128e20150301xx s 000 0 eng 10.1007/s11219-014-9237-3 doi (NATIONALLICENCE)springer-10.1007/s11219-014-9237-3 PBCOV: a property-based coverage criterion [Elektronische Daten] [Kassem Fawaz, Fadi Zaraket, Wes Masri, Hamza Harkous] Coverage criteria aim at satisfying test requirements and compute metrics values that quantify the adequacy of test suites at revealing defects in programs. Typically, a test requirement is a structural program element, and the coverage metric value represents the percentage of elements covered by a test suite. Empirical studies show that existing criteria might characterize a test suite as highly adequate, while it does not actually reveal some of the existing defects. In other words, existing structural coverage criteria are not always sensitive to the presence of defects. This paper presents PBCOV, a Property-Based COVerage criterion, and empirically demonstrates its effectiveness. Given a program with properties therein, static analysis techniques, such as model checking, leverage formal properties to find defects. PBCOV is a dynamic analysis technique that also leverages properties and is characterized by the following: (a) It considers the state space of first-order logic properties as the test requirements to be covered; (b) it uses logic synthesis to compute the state space; and (c) it is practical, i.e., computable, because it considers an over-approximation of the reachable state space using a cut-based abstraction.We evaluated PBCOV using programs with test suites comprising passing and failing test cases. First, we computed metrics values for PBCOV and structural coverage using the full test suites. Second, in order to quantify the sensitivity of the metrics to the absence of failing test cases, we computed the values for all considered metrics using only the passing test cases. In most cases, the structural metrics exhibited little or no decrease in their values, while PBCOV showed a considerable decrease. This suggests that PBCOV is more sensitive to the absence of failing test cases, i.e., it is more effective at characterizing test suite adequacy to detect defects, and at revealing deficiencies in test suites. Springer Science+Business Media New York, 2014 Software testing nationallicence Coverage criteria nationallicence Property-based coverage nationallicence State space coverage nationallicence Specification-based coverage nationallicence Test suite evaluation nationallicence Reachability analysis nationallicence Logic synthesis nationallicence Fawaz Kassem University of Michigan, Ann Arbor, MI, USA aut Zaraket Fadi American University of Beirut, Beirut, Lebanon aut Masri Wes American University of Beirut, Beirut, Lebanon aut Harkous Hamza Swiss Federal Institute of Technology in Lausanne (EPFL), Lausanne, Switzerland aut Software Quality Journal Springer US; http://www.springer-ny.com 23/1(2015-03-01), 171-202 0963-9314 23:1<171 2015 23 11219 https://doi.org/10.1007/s11219-014-9237-3 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s11219-014-9237-3 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Fawaz Kassem University of Michigan, Ann Arbor, MI, USA aut NATIONALLICENCE 700 1- Zaraket Fadi American University of Beirut, Beirut, Lebanon aut NATIONALLICENCE 700 1- Masri Wes American University of Beirut, Beirut, Lebanon aut NATIONALLICENCE 700 1- Harkous Hamza Swiss Federal Institute of Technology in Lausanne (EPFL), Lausanne, Switzerland aut NATIONALLICENCE 773 0- Software Quality Journal Springer US; http://www.springer-ny.com 23/1(2015-03-01), 171-202 0963-9314 23:1<171 2015 23 11219