Graduation Semester and Year
Fall 2024
Language
English
Document Type
Dissertation
Degree Name
Doctor of Philosophy in Computer Science
Department
Computer Science and Engineering
First Advisor
Allison Sullivan
Second Advisor
Dave Levine
Third Advisor
Dajiang Zhu
Fourth Advisor
Jiang Ming
Abstract
Writing correct software models is important in today’s society. Unfortunately, software development is an error-prone task that frequently leads to buggy software. That is why users, both novices and experts, make use of additional techniques and tools to make software more reliable and correct. One of the languages that proposes a solution to this is Alloy. Alloy is a declarative language based on first order logic. Its main advantage is the ability to describe complex systems using concise formal logic. To verify the model and its properties, Alloy uses the Alloy Analyzer, an SAT-based verification tool that supports fully automatic analysis of Alloy models. For a given Alloy model, the Analyzer employs an SAT solver to check if the given properties are satisfied or refuted, and if not, it produces scenarios that demonstrate those cases.
To gain the many benefits that arise from using a software model, the model itself needs to be correct. Our thesis aims to address ways in which we can help improve the accuracy of the model, so that we can, in turn, ensure the underlying system’s correctness is guaranteed against the right behavior. To this end, our thesis first presents an extension to the Analyzer, Reach, that incorporates staged generation of scenarios up to the user-provided scope, allowing the users to inspect scenarios of interest semi-orderly, going from the smallest to the largest given scope. Due to this more organized enumeration, it is easier for users to identify key scenarios and turn around and utilize them to help validate their models and their system.
After Reach, the Alloy language was extended to support temporal logic. This new support means that previously existing validation efforts for software models also need to be updated to remain relevant. Following this trajectory, our thesis presents an update to the current mutation testing tool, μAlloy, facilitating testing, and validation of complex Alloy temporal models. We have updated μAlloy’s test generation capability to build temporal Alloy models, and automatically perform mutation testing for the detection of faulty Alloy models. In addition, we present a case study where we corrected mutants in various parts, correcting them in signatures, in facts, or in predicates to highlight that certain mutations can guide debugging efforts.
Additionally, our thesis presents an empirical study on common practices and mistakes that novice users make while writing Alloy models using the Alloy4Fun benchmark [6]. We have identified commonalities between the way the users tend to write correct solutions as well as incorrect ones, resulting in a series of guidelines for future research to refactor correct formulas to be more efficient in analyzing and debugging faulty formulas. Utilizing these findings, we have developed two benchmarks beneficial to future software modeling. Firstly, we introduce a collection of faulty Alloy models broken by type of fault. Secondly, we introduce submission history trees, visual representations of incremental changes made by users’ model refining. These benchmarks can be used to improve writing software models, to improve incremental analysis techniques, to explore refinements that users tend to make in real-world scenarios, as well as for educational purposes.
Finally, we have used the insights from the empirical study to refine our mutation testing tool to reflect common mistakes. First, we update our current mutation operators broadening their respective scopes, additionally, we introduce new first or- der mutant operators. Finally, we present a case study on the effectiveness versus scalability of second order mutation.
Keywords
Alloy, Mutation testing, Refinement, Staged scenario generation, First order mutants, Second order mutants
Disciplines
Software Engineering
License
This work is licensed under a Creative Commons Attribution 4.0 International License.
Recommended Citation
Jovanovic, Ana, "Improving the Accuracy of Software Models using Refinement and Mutation Testing" (2024). Computer Science and Engineering Dissertations. 399.
https://mavmatrix.uta.edu/cse_dissertations/399