Fault localization for declarative models in alloy

Kaiyuan Wang, Allison Sullivan, Darko Marinov, Sarfraz Khurshid

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Fault localization is a popular research topic and many techniques have been proposed to locate faults in imperative code, e.g. C and Java. In this paper, we focus on the problem of fault localization for declarative models in Alloy - a first order relational logic with transitive closure. We introduce AlloyFLhy, the first fault localization technique for faulty Alloy models which leverages multiple test formulas. AlloyFLhy brings the traditional spectrum-based and mutation-based fault localization techniques to Alloy and combines both techniques to locate faults. To measure the effectiveness of AlloyFLhy, we define three distance metrics and use both distance-based and top-k metrics to measure the effectiveness of AlloyFLhy on 90 real faulty models. The results show that AlloyFLhy is substantially more effective than Alloy's built-in unsat core.

Original languageEnglish (US)
Title of host publicationProceedings - 2020 IEEE 31st International Symposium on Software Reliability Engineering, ISSRE 2020
EditorsMarco Vieira, Henrique Madeira, Nuno Antunes, Zheng Zheng
PublisherIEEE Computer Society
Pages391-402
Number of pages12
ISBN (Electronic)9781728198705
DOIs
StatePublished - Oct 2020
Event31st IEEE International Symposium on Software Reliability Engineering, ISSRE 2020 - Virtual, Coimbra, Portugal
Duration: Oct 12 2020Oct 15 2020

Publication series

NameProceedings - International Symposium on Software Reliability Engineering, ISSRE
Volume2020-October
ISSN (Print)1071-9458

Conference

Conference31st IEEE International Symposium on Software Reliability Engineering, ISSRE 2020
CountryPortugal
CityVirtual, Coimbra
Period10/12/2010/15/20

Keywords

  • Alloy
  • AlloyFLHy
  • Fault localization

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Cite this