Document Type
Article
Abstract
Declarative models help improve the reliability of software systems: models can be used to convey requirements, analyze system designs and verify implementation properties. Alloy is a commonly used modeling language. A key strength of Alloy is the Analyzer, Alloy’s integrated development environment (IDE), which allows users to write and execute models by leveraging a fully automatic SAT based analysis engine. Unfortunately, writing correct constraints of complex properties is difficult.To help users identify fault locations, AlloyFL is a fault localization technique that takes as input a faulty Alloy model and a fault-revealing test suite. As output, AlloyFL returns a ranked list of locations from most to least suspicious. This paper describes our Java implementation of AlloyFL as an extension to the Analyzer. Our experimental results show AlloyFL is capable of detecting the location of real world faults and works in the presence of multiple faulty locations.
Publication Date
8-23-2021
Language
English
License
This work is licensed under a Creative Commons Attribution 4.0 International License.
Recommended Citation
Khan, Tanvir Ahmed; Wang, Kaiyun; and Sullivan, Allison, "AlloyFL: A Fault Localization Framework for Alloy" (2021). Association of Computing Machinery Open Access Agreement Publications. 32.
https://mavmatrix.uta.edu/utalibraries_acmoapubs/32