ABSTRACTThis paper introduces an automatic debuggingframework that relies on model–based reasoning techniquesto locate faults in programs. In particular, model–based diagnosis, together with an abstract interpretationbased conﬂict detection mechanism is used to derive diagnoses, which correspond to possible faults in pro-grams. Design information and partial speciﬁcations are applied to guide a model revision process, whichallows for automatic detection and correction of structural faults. KEYWORDS : Model–based Debugging, Diagnosis, Abstract Interpretation, Program Analysis 1 Introduction Detecting a faulty behavior within a program, locating the cause of the fault, and ﬁxing the faultby means of changing the program, continues to be a crucial and challenging task in software de-velopment. Many papers have been published so far in the domain of detecting faults in software,e.g., testing or formal veriﬁcation [CDH + 00], and locating them, e.g., program slicing [Wei84] andautomatic program debugging [Llo87]. More recently model–based diagnosis [Rei87] has been usedfor locating faults in software [CFD93, MSWW02a].This paper extends previous research in several directions: Firstly, a parameterized debuggingframework is introduced, which integrates dynamic and static properties, as well as design infor-mation of programs. The framework is based on results derived in the ﬁeld of abstract interpreta-tion [CC77], and can therefore be parameterized with different lattices and context selection strate-gies.Secondly, the one–to–one correspondence between model components and program statementsis replaced by a hierarchy of components, which provides means for more efﬁcient reasoning proce-dures, as well as more ﬂexibility when focusing on interesting parts of a program.This work is organized as follows. In Section 2, we give an introduction to model-based debug-ging. Section 3 describes mapping from source code to model components and the (approximate)computation of program effects in the style of [CC77] and [Bou93]. The next section discusses themodeling of programs and the reasoning framework. In Section 5, we provide an example whichputs together the different models and demonstrates the debugging capabilities of our approach.
Recently, model checking approaches have been extended to attempt fault localization in counterexample traces. @cite_40 extended a model checking algorithm that is able to pinpoint transitions in traces responsible for a faulty behavior. @cite_39 presents another approach, which explores the neighborhood of counterexamples to determine causes of faulty behavior. These techniques mostly consider deviations in control flow and do not take data dependencies into account. Also, the derivation of the abstract model from the concrete program usually is non--trivial and is difficult to automate.
@cite_40 @cite_39
1523041988 2158870716 1511405608 2218365969
A traditional counterexample to a linear-time safety property shows the values of all signals at all times prior to the error. However, some signals may not be critical to causing the failure. A succinct explanation may help human understanding as well as speed up algorithms that have to analyze many such traces. In Bounded Model Checking (BMC), a counterexample is constructed from a satisfying assignment to a Boolean formula, typically in CNF. Modern SAT solvers usually assign values to all variables when the input formula is satisfiable. Deriving minimal satisfying assignments from such complete assignments does not lead to concise explanations of counterexamples because of how CNF formulae are derived from the models. Hence, we formulate the extraction of a succinct counterexample as the problem of finding a minimal assignment that, together with the Boolean formula describing the model, implies an objective. We present a two-stage algorithm for this problem, such that the result of each stage contributes to identify the “interesting” events that cause the failure. We demonstrate the effectiveness of our approach with an example and with experimental results. There is significant room for improving users' experiences with model checking tools. An error trace produced by a model checker can be lengthy and is indicative of a symptom of an error. As a result, users can spend considerable time examining an error trace in order to understand the cause of the error. Moreover, even state-of-the-art model checkers provide an experience akin to that provided by parsers before syntactic error recovery was invented: they report a single error trace per run. The user has to fix the error and run the model checker again to find more error traces.We present an algorithm that exploits the existence of correct traces in order to localize the error cause in an error trace, report a single error trace per error cause, and generate multiple error traces having independent causes. We have implemented this algorithm in the context of slam , a software model checker that automatically verifies temporal safety properties of C programs, and report on our experience using it to find and localize errors in device drivers. The algorithm typically narrows the location of a cause down to a few lines, even in traces consisting of hundreds of statements. One of the chief advantages of model checking is the production of counterexamples demonstrating that a system does not satisfy a specification. However, it may require a great deal of human effort to extract the essence of an error from even a detailed source-level trace of a failing run. We use an automated method for finding multiple versions of an error (and similar executions that do not produce an error), and analyze these executions to produce a more succinct description of the key elements of the error. The description produced includes identification of portions of the source code crucial to distinguishing failing and succeeding runs, differences in invariants between failing and nonfailing runs, and information on the necessary changes in scheduling and environmental actions needed to cause successful runs to fail. Many software model checkers only detect counterexamples with deep loops after exploring numerous spurious and increasingly longer counterexamples. We propose a technique that aims at eliminating this weakness by constructing auxiliary paths that represent the effect of a range of loop iterations. Unlike acceleration, which captures the exact effect of arbitrarily many loop iterations, these auxiliary paths may under-approximate the behaviour of the loops. In return, the approximation is sound with respect to the bit-vector semantics of programs. Our approach supports arbitrary conditions and assignments to arrays in the loop body, but may as a result introduce quantified conditionals. To reduce the resulting performance penalty, we present two quantifier elimination techniques specially geared towards our application. Loop under-approximation can be combined with a broad range of verification techniques. We paired our techniques with lazy abstraction and bounded model checking, and evaluated the resulting tool on a number of buffer overflow benchmarks, demonstrating its ability to efficiently detect deep counterexamples in C programs that manipulate arrays.