Experimental Fault Analysis Process Implemented Using Model Extraction and Model Checking

When a software failure is observed during testing or operation, developers traditionally execute the software program again for reproducing the failure to analyze the cause of the failure. However, failures are often hard to reproduce because they depend on factors that are hard to expressly control, such as concurrency and nondeterminism. This paper presents a novel experimental fault analysis process for such "hard-to-reproduce failures". The proposed process consists of three phases: assumption of a hypothesis for the cause of a failure, experiments to examine the hypothesis and confirmation of the experimental results. We formalized the process and implemented it by using model extraction and model checking. Model extraction acts as a bridge between the assumption and experiment. Experiments on failure reproduction are conducted using model checking. The results of the case studies show that the process and tools supporting the process enables developers to detect the cause of hard-to-reproduce failures in industrial software development.