Bug Hunting with False Negatives Revisited

J.R. Calame, N. Ioustinova, Jan Cornelis van de Pol, N. Sidorova

Research output: Book/ReportReportProfessional

8 Downloads (Pure)

Abstract

Safe data abstractions are widely used for verification purposes. Positive verification results can be transferred from the abstract to the concrete system. When a property is violated in the abstract system, one still has to check whether a concrete violation scenario exists. However, even when the violation scenario is not reproducible in the concrete system (a false negative), it may still contain information on possible sources of bugs. Here, we propose a bug hunting framework based on abstract violation scenarios. We first extract a violation pattern from one abstract violation scenario. The violation pattern represents multiple abstract violation scenarios, increasing the chance that a corresponding concrete violation exists. Then, we look for a concrete violation that corresponds to the violation pattern by using constraint solving techniques. Finally, we define the class of counterexamples that we can handle and argue correctness of the proposed framework. Our method combines two formal techniques, model checking and constraint solving. Through an analysis of contracting and precise abstractions, we are able to integrate overapproximation by abstraction with concrete counterexample generation.
Original languageUndefined
Place of PublicationAmsterdam
PublisherCentrum voor Wiskunde en Informatica
Number of pages24
Publication statusPublished - Dec 2007

Publication series

NameReport Software Engineering
No.7/SEN-R0708
ISSN (Print)1386-369X

Keywords

  • IR-64600
  • METIS-245982
  • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
  • FMT-MC: MODEL CHECKING
  • CR-B.5.3
  • EWI-11824

Cite this

Calame, J. R., Ioustinova, N., van de Pol, J. C., & Sidorova, N. (2007). Bug Hunting with False Negatives Revisited. (Report Software Engineering; No. 7/SEN-R0708). Amsterdam: Centrum voor Wiskunde en Informatica.
Calame, J.R. ; Ioustinova, N. ; van de Pol, Jan Cornelis ; Sidorova, N. / Bug Hunting with False Negatives Revisited. Amsterdam : Centrum voor Wiskunde en Informatica, 2007. 24 p. (Report Software Engineering; 7/SEN-R0708).
@book{f202374bfa4744c198cdfcc5481bde67,
title = "Bug Hunting with False Negatives Revisited",
abstract = "Safe data abstractions are widely used for verification purposes. Positive verification results can be transferred from the abstract to the concrete system. When a property is violated in the abstract system, one still has to check whether a concrete violation scenario exists. However, even when the violation scenario is not reproducible in the concrete system (a false negative), it may still contain information on possible sources of bugs. Here, we propose a bug hunting framework based on abstract violation scenarios. We first extract a violation pattern from one abstract violation scenario. The violation pattern represents multiple abstract violation scenarios, increasing the chance that a corresponding concrete violation exists. Then, we look for a concrete violation that corresponds to the violation pattern by using constraint solving techniques. Finally, we define the class of counterexamples that we can handle and argue correctness of the proposed framework. Our method combines two formal techniques, model checking and constraint solving. Through an analysis of contracting and precise abstractions, we are able to integrate overapproximation by abstraction with concrete counterexample generation.",
keywords = "IR-64600, METIS-245982, FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS, FMT-MC: MODEL CHECKING, CR-B.5.3, EWI-11824",
author = "J.R. Calame and N. Ioustinova and {van de Pol}, {Jan Cornelis} and N. Sidorova",
year = "2007",
month = "12",
language = "Undefined",
series = "Report Software Engineering",
publisher = "Centrum voor Wiskunde en Informatica",
number = "7/SEN-R0708",
address = "Netherlands",

}

Calame, JR, Ioustinova, N, van de Pol, JC & Sidorova, N 2007, Bug Hunting with False Negatives Revisited. Report Software Engineering, no. 7/SEN-R0708, Centrum voor Wiskunde en Informatica, Amsterdam.

Bug Hunting with False Negatives Revisited. / Calame, J.R.; Ioustinova, N.; van de Pol, Jan Cornelis; Sidorova, N.

Amsterdam : Centrum voor Wiskunde en Informatica, 2007. 24 p. (Report Software Engineering; No. 7/SEN-R0708).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Bug Hunting with False Negatives Revisited

AU - Calame, J.R.

AU - Ioustinova, N.

AU - van de Pol, Jan Cornelis

AU - Sidorova, N.

PY - 2007/12

Y1 - 2007/12

N2 - Safe data abstractions are widely used for verification purposes. Positive verification results can be transferred from the abstract to the concrete system. When a property is violated in the abstract system, one still has to check whether a concrete violation scenario exists. However, even when the violation scenario is not reproducible in the concrete system (a false negative), it may still contain information on possible sources of bugs. Here, we propose a bug hunting framework based on abstract violation scenarios. We first extract a violation pattern from one abstract violation scenario. The violation pattern represents multiple abstract violation scenarios, increasing the chance that a corresponding concrete violation exists. Then, we look for a concrete violation that corresponds to the violation pattern by using constraint solving techniques. Finally, we define the class of counterexamples that we can handle and argue correctness of the proposed framework. Our method combines two formal techniques, model checking and constraint solving. Through an analysis of contracting and precise abstractions, we are able to integrate overapproximation by abstraction with concrete counterexample generation.

AB - Safe data abstractions are widely used for verification purposes. Positive verification results can be transferred from the abstract to the concrete system. When a property is violated in the abstract system, one still has to check whether a concrete violation scenario exists. However, even when the violation scenario is not reproducible in the concrete system (a false negative), it may still contain information on possible sources of bugs. Here, we propose a bug hunting framework based on abstract violation scenarios. We first extract a violation pattern from one abstract violation scenario. The violation pattern represents multiple abstract violation scenarios, increasing the chance that a corresponding concrete violation exists. Then, we look for a concrete violation that corresponds to the violation pattern by using constraint solving techniques. Finally, we define the class of counterexamples that we can handle and argue correctness of the proposed framework. Our method combines two formal techniques, model checking and constraint solving. Through an analysis of contracting and precise abstractions, we are able to integrate overapproximation by abstraction with concrete counterexample generation.

KW - IR-64600

KW - METIS-245982

KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

KW - FMT-MC: MODEL CHECKING

KW - CR-B.5.3

KW - EWI-11824

M3 - Report

T3 - Report Software Engineering

BT - Bug Hunting with False Negatives Revisited

PB - Centrum voor Wiskunde en Informatica

CY - Amsterdam

ER -

Calame JR, Ioustinova N, van de Pol JC, Sidorova N. Bug Hunting with False Negatives Revisited. Amsterdam: Centrum voor Wiskunde en Informatica, 2007. 24 p. (Report Software Engineering; 7/SEN-R0708).