Attention-based coverage metrics

TY - CHAP

T1 - Attention-based coverage metrics

AU - Ben-David, Shoham

AU - Chockler, Hana

AU - Kupferman, Orna

PY - 2013/12/1

Y1 - 2013/12/1

N2 - Over the last decade, extensive research has been conducted on coverage metrics for model checking. The most common coverage metrics are based on mutations, where one examines the effect of small modifications of the system on the satisfaction of the specification. While it is commonly accepted that mutation-based coverage provides adequate means for assessing the exhaustiveness of the model-checking procedure, the incorporation of coverage checks in industrial model checking tools is still very partial. One reason for this is the typically overwhelming number of non-covered mutations, which requires the user to somehow filter those that are most likely to point to real errors or overlooked behaviors. We address this problem and propose to filter mutations according to the attention the designer has paid to the mutated components in the model. We formalize the attention intuition using a multi-valued setting, where the truth values of the signals in the model describe their level of importance. Non-covered mutations of signals of high importance are then more alarming than non-covered mutations of signals with low intention. Given that such "importance information" is usually not available in practice, we suggest two new coverage metrics that automatically approximate it. The idea behind both metrics is the observation that designers tend to modify the value of signals only when there is a reason to do so. We demonstrate the advantages of both metrics and describe algorithms for calculating them.

AB - Over the last decade, extensive research has been conducted on coverage metrics for model checking. The most common coverage metrics are based on mutations, where one examines the effect of small modifications of the system on the satisfaction of the specification. While it is commonly accepted that mutation-based coverage provides adequate means for assessing the exhaustiveness of the model-checking procedure, the incorporation of coverage checks in industrial model checking tools is still very partial. One reason for this is the typically overwhelming number of non-covered mutations, which requires the user to somehow filter those that are most likely to point to real errors or overlooked behaviors. We address this problem and propose to filter mutations according to the attention the designer has paid to the mutated components in the model. We formalize the attention intuition using a multi-valued setting, where the truth values of the signals in the model describe their level of importance. Non-covered mutations of signals of high importance are then more alarming than non-covered mutations of signals with low intention. Given that such "importance information" is usually not available in practice, we suggest two new coverage metrics that automatically approximate it. The idea behind both metrics is the observation that designers tend to modify the value of signals only when there is a reason to do so. We demonstrate the advantages of both metrics and describe algorithms for calculating them.

UR - http://www.scopus.com/inward/record.url?scp=84891858168&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-03077-7_16

DO - 10.1007/978-3-319-03077-7_16

M3 - Conference paper

AN - SCOPUS:84891858168

SN - 9783319030760

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 230

EP - 245

BT - Hardware and Software: Verification and Testing

A2 - Bertacco, Valeria

A2 - Legay, Axel

PB - Springer International Publishing

T2 - 9th Haifa Verification Conference, HVC 2013

Y2 - 5 November 2013 through 7 November 2013

ER -