Bug Hunting with False Negatives Revisited

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

    Research output: Book/ReportReportProfessional

    13 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.