This paper proposes the first mutation-based technique for the repair of Alloy 6 first-order temporal logic specifications. This technique was developed with the educational context in mind, in particular, to repair submissions for specification challenges, as allowed, for example, in the Alloy4Fun web-platform. Given an oracle and an incorrect submission, the proposed technique searches for syntactic mutations that lead to a correct specification, using previous counterexamples to quickly prune the search space, thus enabling timely feedback to students. Evaluation shows that, not only is the technique feasible for repairing temporal logic specifications, but also outperforms existing techniques for non-temporal Alloy specifications in the context of educational challenges.
CITATION STYLE
Cerqueira, J., Cunha, A., & Macedo, N. (2022). Timely Specification Repair for Alloy 6. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13550 LNCS, pp. 288–303). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-17108-6_18
Mendeley helps you to discover research relevant for your work.