An Empirical Assessment of Formal Models and Static Analysis Alarms in the Context of Defect Detection

Software developers work with different programming languages and tools in their careers. Software maintenance is one of the essential parts of a developer\u27s job. It includes locating and correcting defects in software systems. Understanding how developers comprehend programs and their process of finding and fixing bugs is essential for creating better tools to improve their productivity and workflow. It also gives us insight into their cognitive processes while working on these tasks, which can help build theories for teaching and learning programming. This dissertation presents three studies on assessing formal models and static analysis alarms in the context of defect detection. The first is an online empirical study on the effects of experience on bug fixing tasks in the Alloy specification language, a lightweight formal language with accompanying software that performs bounded model checking to facilitate verifying properties of software models. The study found that non-novices performed 54% better on the Alloy tasks compared to novices, and participants performed better on syntactic tasks compared to semantic tasks. Insights from the participants\u27 problem solving patterns are presented. The second and third studies investigate the effects of repositioning and merging static analysis alarms used to detect software defects on task accuracy and developers\u27 visual effort. The data for the first study was collected through an online survey, and in the second study, eye tracking was used to collect the participants\u27 gazes while working on the tasks. Each study was done independently, with no overlap between participants. Both studies\u27 results indicate that the repositioning and merging treatment do not affect accuracy. However, the eye tracking study results indicate that there is a significant difference in visual effort with the repositioning and merging of alarms as it draws the focus and attention of the developers to the most important parts of the program to solve tasks. The impact of these results on languages and tools to assist developers in defect detection is discussed