On the Complexity of Error Explanation

When a system fails to satisfy its specification, the model checker produces an error trace (or counter-example) that demonstrates an undesirable behavior, which is then used in debugging the system. Error explanation is the task of discovering errors in the system or the reasons why the system exhibits the error trace. While there has been considerable recent interest in automating this task and developing tools based on different heuristics, there has been very little effort in characterizing the computational complexity of the problem of error explanation. In this paper, we study the complexity of two popular heuristics used in error explanation. The first approach tries to compute the smallest number of system changes that need to be made in order to ensure that the given counter-example is no longer exhibited, with the intuition being that these changes are the errors that need fixing. The second approach relies on the observation that differences between correct and faulty ...

• Type: Conference
• Year: 2005
• Where: VMCAI
• Authors: Nirman Kumar, Viraj Kumar, Mahesh Viswanathan
• Keywords: Error Explanation, Error Trace, Software Engineering, VMCAI 2005, first Approach