CFaults: Model-Based Diagnosis for Fault Localization in C Programs with Multiple Test Cases

要約

デバッグは、ソフトウェア開発において最も時間と費用がかかるタスクの 1 つです。
数式ベースの障害位置特定 (FBFL) 方法がいくつか提案されていますが、失敗したすべてのテストにわたって一連の診断を保証できなかったり、特に複数の障害があるプログラムの場合、サブセット最小ではない冗長な診断が生成される可能性があります。
この論文では、複数の障害を持つ C プログラムに対する新しい障害位置特定アプローチを紹介します。
CFaults は、複数の観察によるモデルベースの診断 (MBD) を活用し、失敗したすべてのテスト ケースを統合された MaxSAT 式に集約します。
その結果、私たちの方法は観測全体にわたる一貫性を保証し、障害位置特定手順を簡素化します。
C プログラムの 2 つのベンチマーク セット、TCAS と C-Pack-IPA での実験結果は、CFaults が BugAssist や SNIPER などの他の FBFL アプローチよりも高速であることを示しています。
さらに、CFaults は、欠陥のあるステートメントのサブセット最小限の診断のみを生成しますが、他のアプローチでは冗長な診断が列挙される傾向があります。

要約(オリジナル)

Debugging is one of the most time-consuming and expensive tasks in software development. Several formula-based fault localization (FBFL) methods have been proposed, but they fail to guarantee a set of diagnoses across all failing tests or may produce redundant diagnoses that are not subset-minimal, particularly for programs with multiple faults. This paper introduces a novel fault localization approach for C programs with multiple faults. CFaults leverages Model-Based Diagnosis (MBD) with multiple observations and aggregates all failing test cases into a unified MaxSAT formula. Consequently, our method guarantees consistency across observations and simplifies the fault localization procedure. Experimental results on two benchmark sets of C programs, TCAS and C-Pack-IPAs, show that CFaults is faster than other FBFL approaches like BugAssist and SNIPER. Moreover, CFaults only generates subset-minimal diagnoses of faulty statements, whereas the other approaches tend to enumerate redundant diagnoses.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google