Abstract
| Original language | Undefined |
|---|---|
| Place of Publication | Amsterdam |
| Publisher | Centrum voor Wiskunde en Informatica |
| Number of pages | 24 |
| Publication status | Published - Dec 2007 |
Publication series
| Name | Report 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
}
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/Report › Report › Professional
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 -