MuAlloy : an automated mutation system for alloy

Mutation is a powerful technique that researchers have studied for several decades in the context of imperative code. For example, mutation testing is commonly considered a '"gold standard"' for test suite quality. Mutation in the context of declarative languages is a less studied problem. This thesis introduces a foundation for mutation-driven analyses for Alloy, a first-order, declarative language based on relations. Specifically, we introduce a family of mutation operators for Alloy models and define algorithms for applying the operators on different parts of the models. We embody these operators and algorithms in our prototype tool MuAlloy that provides a GUI-based front-end for customizing the application of mutation operators. To demonstrate the potential of our approach, we illustrate the use of MuAlloy in two application scenarios: (1) mutation testing for Alloy (in the spirit of traditional mutation testing for imperative languages); and (2) program repair for Alloy using mutation.

Name thesis:degree_name

Master of Science in Engineering

Level thesis:degree_level

Masters

Discipline thesis:degree_discipline

Electrical and Computer Engineering

Grantor

The University of Texas at Austin

Year dc:date.issued

2015

Author dc:creator

• Wang, Kaiyuan

Advisor dc:contributor.advisor

• Khurshid, Sarfraz

Committee member dc:contributor.committeemember

• Perry, Dewayne E.

• MuAlloy
• Mutation
• Alloy
• Mutation testing
• Repair

Language dc:language.iso

en

Identifier

doi:10.15781/T2S31M

OAI identifier oai:identifier

oai:repositories.lib.utexas.edu:2152/31865