Mutation Testing for Temporal Alloy Models.

Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties before systems are built, to automated testing and debugging of their implementations after they are built. Alloy is a declarative modeling language that is well-suited for verifying system designs. A key strength of Alloy is its scenario-finding toolset, the Analyzer, which allows users to explore all valid scenarios that adhere to the model’s constraints up to a user-provided scope. Despite the Analyzer, writing correct Alloy models remains a difficult task, partly due to Alloy’s expressive operators, which allow for succinct formulations of complex properties but can be difficult to reason over manually. To further add to the complexity, Alloy’s grammar was recently expanded to support linear temporal logic, increasing both the expressibility of Alloy as well as the burden for accurately expressing properties. To address this, this paper presents μAlloyτ, an extension to Alloy’s mutation testing framework that accounts for the newly introduced temporal logic, including updating μAlloyτ’s test generation capability to produce temporal test cases. Experimental results reveal μAlloyτ is efficient at generating and checking mutations and μAlloyτ’s automatically generated tests are effective at detecting faulty temporal models.