Interactive specification mining for debugging embedded software systems
Specification mining techniques are typically used to extract the specification of a software in the absence of (up-to-date) specification documents. Several research projects have targeted the problem in the past. However, very limited application of such techniques is observed in industry, due to challenges related to accuracy and practicality of those techniques. Such specifications are useful for program comprehension, testing, and anomaly detection. However, specification mining can also be used for debugging, where a faulty behavior is abstracted to give developers a context about the bug and help them locate it. In this thesis, I proposed, developed, and evaluated an interactive semi-automated specification mining approach that not only helps generating targeted and correct specifications of a system but can also be used specifically for debugging. The tool users can select relevant state fields and functions, per issue, interactively, and run the tool on a reported faulty scenario. The tool generates a state machine that represents the faulty behavior, abstracted with respect to the users' inputs. These models are then used to locate the fault's root cause for debugging. I have applied the technique and tool on an AutoPilot software system for UAVs, from Micropilot Inc. I evaluated the approach and tool in a set of experiments, based on Micropilot's actual reported issues. I interviewed Micropilot developers after they used the tool in an experimental setup for debugging different real issues and collected their feedback. The results have shown that the approach is feasible, and brings advantages over only using code-level debugging tools.