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.