Locating faults in spreadsheets can be difficult. Therefore, tools supporting the localization of faults are needed. Modelbased software debugging (MBSD) is a promising fault localization technique. This paper presents a novel dependencybased model that can be used in MBSD. This model allows improvements of the diagnostic accuracy while keeping the computation times short. In an empirical evaluation, we show that dependency-based models of spreadsheets whose value-based models are often not solvable in an acceptable amount of time can be solved in less than one second. Furthermore, we show that the amount of diagnoses obtained through dependency-based models is reduced by 15 % on average when using the novel model instead of the original dependency-based model. The short computation time and the improved diagnostic accuracy enable the usage of model-based debugging for spreadsheets in practice.
Even for small spreadsheets, the localization of faults can
be time consuming and frustrating. Thus, approaches
supporting fault localization in spreadsheets are needed. Some
fault localization techniques developed for the software
engineering discipline have been adapted to the spreadsheet
domain, for example [
(a) Normal view
(b) Formula view
When using model based debugging, the faulty cell of this
example spreadsheet can be detected independent of the
underlying model. There are however differences with respect
to runtime and solution size. The value-based model and
our novel dependency-based model identify three cells that
1An output cell is a cell that is not referenced by any other cell.
could explain the observed misbehavior, while the original
dependency-based model identifies six cells as possible
explanations. When using the constraint solver Minion [
In the remainder of this paper, we will explain the different types of models and show the model representations for the above described running example (see Section 2). In Section 3, we will empirically compare the different models with respect to efficiency and effectiveness. The novel dependency-based model reduces the number of computed diagnoses by 15 % compared to original dependency-based model. Furthermore, the empirical evaluation shows that the dependency-based models can be solved in less than one second even for those spreadsheets whose value-based models require more than 20 minutes solving time.
In model-based software debugging (MBSD), the cells of a
spreadsheet and the given observations (i.e., the test case2)
are converted into constraints. As the given test case is a
failing test case, this constraint system results in a
contradiction. In order to determine which cells could resolve this
contradiction, MBSD introduces abnormal variables (AB) for
each cell. These abnormal variables represent the “health”
state of the cells. If a cell c is not abnormal, the formula of
the cell must be correct [
Having such a constraint system, we are able to use a
constraint or SMT solver to determine which abnormal variables
have to be set to true to eliminate the contradiction. We
refer the interested reader to [
When using value-based models, the values of the cells are
propagated. A value-based constraint system contains (i) the
input cells and their values, (ii) the output cells and their
expected values, and (iii) all formulas concatenated with their
abnormal variable. The constraint representation handles
the formulas as equations instead of assignments. This
allows to draw conclusions on the input from the output of a
formula. Such a value-based model for spreadsheets is
proposed by Abreu et al. [
When using dependency-based models, only the information about whether the computed values are correct is propagated. Therefore, all cell values are represented as Boolean instead of Integer or Real values. All variables representing input cells are initialized with true. All variables representing correct output cells are also initialized with true. The variables representing erroneous output cells are initialized with false. Instead of using the concrete formulas in the constraints, only the correctness relation is modeled. If the formula of cell c is correct and the input values of a formula are correct then cell c must compute a correct value: AB(cellc) ∨
^
c′∈ρ(c)
c′ → c
(3)
where ρ(c) is the set of all cells that are referenced in c.
Details about this modeling for software written in an
imperative language can be found e.g. in [
B2 == true C2 == true B3 == true . . .
D3 == true B7 == true C7 == true D7 == false
∨ ∨ ∨ ∨ ∨ ∨ . . . ∨ (B2 ∧ C2 → D2) (D2 ∧ D4 → D3) (B2 ∧ B3 → B4) (C2 ∧ C3 → C4) (B4 ∧ C4 → D4) (B5 → D5) (D4 ∧ D6 → D7)
Solving this constraint system leads to six possible solutions: Either cell B4, C4, D4, D5, D6 or D7 must contain the fault. This dependency-based model computes more diagnoses because of the implication. In the value-based model, the cells B4, C4, and D4 can be excluded from the set of possible diagnoses because B4 and C4 are used to compute D4, and D4 is used to compute D3, which is known to compute the correct value. Unfortunately, this information gets lost when using the implication because the implication allows conclusions only from the input to the output but not vice versa. This problem will be solved with the novel dependency-based model that is explained in the following subsection.
In order to eliminate the previously described weakness of dependency-based models, we use bi-implication (equivalence) instead of the implication. The formula constraints for our running example from Figure 1b are as follows: Please note, that this list gives only examples. It is not a complete list, because the size of the list depends on the functions that are supported by the concrete spreadsheet environment (e.g. Microsoft Excel, iWorks’Number, OpenOffice’s Calc). All formulas where coincidental correctness might happen still have to be modeled with the implication instead of the bi-implication.
This section consists of two major parts: the empirical setup
(discussing the prototype implementation, the used
platform, and the evaluated spreadsheet corpora) and the
results showing that dependency-based models are able to
compute diagnoses within a fraction of a second even for
spreadsheets whose value-based models require more than
20 minutes of solving time. In addition, this empirical
evaluation shows that the number of diagnoses obtained by the
novel dependency-based model is reduced by 15 % on
average compared to the original dependency-based model.
We developed a prototype in Java for performing the
empirical evaluation. This prototype uses Minion [
The evaluation was performed on an Intel Core2 Duo processor (2.67 GHz) with 4 GB RAM and Windows 7 as operating system. We used the Minion version 0.15. The computation time is the average time over 10 runs.
We evaluated the models by means of spreadsheets from the
publicly available Integer spreadsheet corpus3 [
Table 1 compares the three types of models with respect to fault localization capabilities and runtimes. The fault localization capabilities are expressed by means of the number of cells that are single fault diagnoses. The runtime is measured by means of Minion’s average solving time in milliseconds. The spreadsheets are divided into two subgroups: spreadsheets whose value-based models are solved by Minion in less then 20 minutes and spreadsheets whose value-based models could not be solved within 20 minutes (i.e. 31 from 94 spreadsheets). For these 31 spreadsheets, the dependency-based models are solved in less than one second. These runtime results indicate that dependency-based models are better suited for debugging large spreadsheets than value-based models. 3https://dl.dropbox.com/u/38372651/Spreadsheets/Integer Spreadsheets.zip Reduction
0 % ]0 %;10 %] ]10 %;20 %] ]20 %;30 %] ]30 %;40 %] ]40 %;50 %] ]50 %;60 %] ]60 %;70 %] ]70 %;80 %] ]80 %;90 %] ]90 %;100 %] For 64 spreadsheets, no reduction in the number of diagnoses was achieved when using the novel dependency-based model instead of the original model. However, for 15 spreadsheets, a reduction of more than 80 % was achieved.
Locating faulty formulas in spreadsheets can be time consuming. This paper addresses the fault localization problem by means of model-based diagnosis. Our most important contribution is the introduction of a novel dependencybased model. This novel dependency-based model improves previous work in two ways: (1) Compared to the original dependency-based model, it reduces the amount of diagnoses that have to be manually investigated by 15 %. (2) Compared to the value-based model, it reduces the required solving time and allows the computation of diagnoses in realtime where the value-based model cannot compute solutions within 20 minutes. The savings in computation time can be explained by the reduction of the domain: The dependencybased model requires only Boolean variables instead of Integers and Real numbers.
The reduction of the domain comes with additional advantages: (1) An arbitrary solver can be used, because all solvers support at least Boolean variables. Even spreadsheets containing Real numbers can be debugged with any solver when using dependency-based models. (2) The user does not need to indicate concrete values for the erroneous output variables. The information that an output cell computes the wrong value is sufficient.
In the description of the model, we listed all types of coincidental correctness occurring in the spreadsheets used in the empirical evaluation. This list is not exhaustive. For using this model in practice, the list has to be extended. We are convinced that the model presented improves the state of the art in model-based diagnosis. Further work includes a user study and the adaptation to other types of programs, e.g. programs written in imperative or objectoriented languages.
The research herein is partially conducted within the competence network Softnet Austria II (www.soft-net.at, COMET K-Projekt) and funded by the Austrian Federal Ministry of Economy, Family and Youth (bmwfj), the province of Styria, the Steirische Wirtschaftsfo¨rderungsgesellschaft mbH. (SFG), and the city of Vienna in terms of the center for innovation and technology (ZIT).