Treffer: Mutation testing for temporal alloy models (extended version).

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 and 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. [ABSTRACT FROM AUTHOR]