Bounded Exhaustive Search of Alloy Specification Repairs

TL;DR

This paper introduces BeAFix, an automated repair technique for Alloy models that uses a novel bounded exhaustive search strategy, does not require tests, and effectively repairs thousands of real-world faulty models.

Contribution

BeAFix is the first Alloy repair method employing a scalable, bounded exhaustive search with sound pruning, eliminating the need for unit tests and improving repair effectiveness.

Findings

Successfully repaired thousands of real-world Alloy models.

Outperformed existing Alloy repair techniques.

Did not require unit tests for repairs.

Abstract

The rising popularity of declarative languages and the hard to debug nature thereof have motivated the need for applicable, automated repair techniques for such languages. However, despite significant advances in the program repair of imperative languages, there is a dearth of repair techniques for declarative languages. This paper presents BeAFix, an automated repair technique for faulty models written in Alloy, a declarative language based on first-order relational logic. BeAFix is backed with a novel strategy for bounded exhaustive, yet scalable, exploration of the spaces of fix candidates and a formally rigorous, sound pruning of such spaces. Moreover, different from the state-of-the-art in Alloy automated repair, that relies on the availability of unit tests, BeAFix does not require tests and can work with assertions that are naturally used in formal declarative languages. Our experience with using BeAFix to repair thousands of realworld faulty models, collected by other researchers, corroborates its ability to effectively generate correct repairs and outperform the state-of-the-art.