Model Checking-Enhanced Spectrum-Based Fault Localization

Software debugging is crucial in software development, encompassing fault detection, localization, and correction. This article proposes an innovative approach integrating model checking and testing to enhance fault localization accuracy. Our method combines model checking, model checker-based fault localization (MCFL), and spectrum-based fault localization (SBFL), prioritizing program instructions based on suspicion level. Experiments with the TCAS benchmark from Siemens demonstrate the superiority of our integrated approach over traditional spectrum-based methods, especially in challenging versions. Ochiai consistently outperforms Tarantula, and the introduction of the Enhanced Weighted Suspiciousness Ratio (EWSR) spectral metric addresses challenges in specific versions. The primary outcome is a refined fault localization approach significantly improving accuracy compared to traditional methods. Our approach achieves an average $65.47\%$ improvement in fault localization accuracy across TCAS benchmark versions. This integrated fault localization approach represents a significant advancement in software debugging, offering developers an effective method for identifying problematic instructions in faulty programs.

1. Model Checking-Enhanced Spectrum-Based Fault
Localization
Mohammed BEKKOUCHE
´
Ecole Sup´erieure en Informatique, Sidi Bel Abb`es, Algeria
LabRI-SBA Laboratory
[email protected]
CSA 2024
April 23-24, 2024
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

2. Presentation Outline
1
Introduction
2
State of the Art
3
Motivating Example
4
Approach
5
Results
6
Conclusion
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

3. Introduction
Introduction
Debugging software is time-consuming, especially when it comes to
pinpointing faulty instructions.
Accelerating fault localization
quality.
Research focuses on :
for fault localization.
Proposal:
This presentation introduces a novel approach that
checking
Idea:
Our approach uses model checking
each failing test, reducing non-faulty statement coverage.
The core idea is
spectrum-based fault localization.
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

4. State of the Art
State of the Art
Model Checking-Based Fault Localization
→Model checking evaluates program adherence to a specification by
traversing states.
Techniques :Explain, BugAssist, SNIPER, LocFaults, ...
Spectrum-Based Fault Localization
→Spectrum-based approaches employ ranking metrics to assess program
elements’ suspicion levels.
Techniques :Tarantula, Ochiai, FLCN, ConsilientSFL, ...
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

5. Motivating Example
Motivating Example
Listing
1 {
2∗@
3 \r e s u l t \max \min \min \max
4∗/
5 {
6
7 m=c ;
8 <c ){
9 <b )
10 m=b ;
11 <c )
12 m=b ;
13}
14 {
15 >b )
16 m=b ;
17 >c )
18 m=a ;
19}
20
21}}
Duringthe model checking phase, five suspicious instructions were identified:
{8,12,15,17,20}from the counterexample(a= 2,b= 1,c= 3)
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

6. Motivating Example
Motivating Example
Duringthe testing phase:
Table
Statement
(3,3,5)(3,2,1)(5,5,5)(5,4,3)(2,1,3)(4,5,3)efepnfnpOchiaiRankTarantulaRank
8 11111115000.41 4 0.5 4
12 10001011040.71 1 0.83 1
15 01111114010.45 3 0.55 3
17 00101112030.58 2 0.71 2
20 11111115000.41 4 0.5 4
Result000010
Table
Ochiai
ef
p
(ef+nf)·(ef+ep)
Tarantula
ef
ef+nf
ef
ef+nf
+
ep
ep+np
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

7. Motivating Example
Motivating Example
Utilizingtraditional Spectrum-Based Fault Localizationtechniques :
Table
Spectrum-Based Fault Localization
LineCode efepnfnpOchiaiTarantulaRank
7m=c; 1500 0.41 0.5 3
8if 1500 0.41 0.5 3
9if 11040.71 0.83 1
10m=b; 0015 0 0 7
11else 11040.71 0.83 1
12m=b; 11040.71 0.83 1
15if 0011 0 0 7
16m=b; 0012 0 0 7
17else 0013 0 0 7
18m=a; 0014 0 0 7
20return 1500 0.41 0.5 3
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

8. Approach
Approach
Our approach encompasses three principal steps :Model Checking,Model
Checker-based Fault Localization (MCFL), andSpectrum-based Fault
Localization (SBFL).
Model Checking:
CPBPV/CBMC
Input:Faulty program,
specification
Output:Counterexamples,
successful test cases
MCFL:
LocFaults/BugAssist
Input:Faulty program,
postcondition,
failed test cases
Output:Suspicious
instructions
SBFL:
Ochiai/Tarantula/EWSR
Input:Faulty program,
suspicious instructions,
successful test cases
Output:Ranked instructions
Generate counterexamples
and successful test cases
Locate suspicious
instructions using
MCFL tools
Rank suspicious instructions
using SBFL and spectral
metrics
Figure
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

9. Approach
Approach
Our approach encompasses three principal steps :Model Checking,Model
Checker-based Fault Localization (MCFL), andSpectrum-based Fault
Localization (SBFL).
Model Checking:
CPBPV/CBMC
Input:Faulty program,
specification
Output:Counterexamples,
successful test cases
MCFL:
LocFaults/BugAssist
Input:Faulty program,
postcondition,
failed test cases
Output:Suspicious
instructions
SBFL:
Ochiai/Tarantula/EWSR
Input:Faulty program,
suspicious instructions,
successful test cases
Output:Ranked instructions
Generate counterexamples
and successful test cases
Locate suspicious
instructions using
MCFL tools
Rank suspicious instructions
using SBFL and spectral
metrics
Figure
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

10. Approach
Approach
Weighted Suspiciousness Ratio (WSR)
Novel spectral metric
Equation (refer to Eq. 1)
Higher execution frequency in failed tests
WSR=
ef×np+nf×ep
ef×np+nf×ep+ef×ep+nf×np
(1)
Enhanced Weighted Suspiciousness Ratio (EWSR)
Advancement over WSR
Equation (refer to Eq. 2)
Normalization
EWSR=WSR×
1
p
(ef+ep)×(nf+np)
(2)
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

11. Results
Results
Introduction to TCAS Benchmark and Experiment Setup
Experiments conducted using the
benchmark suite provided by Siemens.
TCAS task simulates an aircraft collision avoidance system with
code
Certain versions excluded due to
Benchmark includes
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

12. Results
Results
Methodology Overview and Comparison
BugAssist
faulty program.
→using a single counterexample
Instructions classified using successful test cases and
Results compared with solely testing-based implementation using
Tarantula
Average position of erroneous instruction calculated using Equation 3 to
address.
MID=S+
`
E−1
2
´
(3)
Srepresents the starting position of the tie, andEdenotes the tie size.
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

13. Results
Results
TCAS Benchmark Experiment Results
v1v2v3v4v5v6v7v8v9v10v11v12v13v14v15v16v17v18v19v20010203040502.511.536.52.533.56.536.539.517.56.56.536.536.515.551.536.536.534.536.516.52.512.537.52.541.56.536.539.517.56.56.537.537.515.521.536.536.542.536.516.52.516.542.52.542.56.542.525.517.56.56.542.542.515.57.536.542.542.542.516.519716.54168.58557.56.531.51616.513.5168.5VersionsLine numbersOchiaiTarantulaEWSRMC+TEST
Figure
TCAS Suite from Siemens
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

14. Results
Results
TCAS Benchmark Experiment Results
v21v22v23v24v25v26v27v28v29v30v31v32v34v35v36v37v39v40v4101020304016.517.517.517.51.537.533.511.513.511.54436.511.512.51.5142.516.517.517.517.51.539.541.512.513.512.54437.512.512.51.5142.516.517.517.517.51.542.542.513.518.514.54442.513.512.51.5142.58.56.579178.5979.52266.51219.51VersionsLine numbersOchiaiTarantulaEWSRBMC+TEST
Figure
TCAS Suite from Siemens
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

15. Results
Results
TCAS Benchmark Experiment Results
Outcomes illustrated in histogram showing
instruction.
Comparison between
approach
Ochiai consistently outperforms Tarantula in localizing faults.
EWSR spectral metric demonstrates variability in performance across versions.
Integrated approach consistently achieves, indicating
improved fault localization accuracy.
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

16. Conclusion
Conclusion
Our integrated fault localization approach represents a significant
advancement in software debugging.
The combination of model checking and testing, as demonstrated in the
TCAS benchmark experiments,
methods.
The novel EWSR spectral metric introduces
challenges in certain versions.
This research contributes to automating and improving the fault localization
process, providing developers with
identifying problematic instructions.
Overall, our integrated fault localization approach demonstrates a remarkable
improvement of approximately65.47%in fault localization accuracy
compared to traditional spectrum-based methods.
Future research avenues may explore the applicability of this approach
other benchmarks
testing
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024

17. Conclusion
Thank you for your attention.Questions ?
Mohammed BEKKOUCHE (ESI-SBA) Fault Localization in Programs April 23-24, 2024