FLACK: Counterexample-Guided Fault Localization for Alloy Models
Alloy is a specification language that has been used in a wide range of applications, such as program verification, test case generation, IoT and Android security, etc. Unlike imperative languages, such as C or Java, Alloy is declarative, which describes the logic of a computation without describing...
| Autores principales: | , , , , , , |
|---|---|
| Formato: | Objeto de conferencia Resumen |
| Lenguaje: | Inglés |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/140263 http://50jaiio.sadio.org.ar/pdfs/asse/ASSE-04.pdf |
| Aporte de: |
| id |
I19-R120-10915-140263 |
|---|---|
| record_format |
dspace |
| institution |
Universidad Nacional de La Plata |
| institution_str |
I-19 |
| repository_str |
R-120 |
| collection |
SEDICI (UNLP) |
| language |
Inglés |
| topic |
Ciencias Informáticas Alloy Alloy buggy expressions |
| spellingShingle |
Ciencias Informáticas Alloy Alloy buggy expressions Zheng, Guolong Nguyen, ThanhVu Gutiérrez Brida, Simón Regis, Germán Frias, Marcelo F. Aguirre, Nazareno Matías Bagheri, Hamid FLACK: Counterexample-Guided Fault Localization for Alloy Models |
| topic_facet |
Ciencias Informáticas Alloy Alloy buggy expressions |
| description |
Alloy is a specification language that has been used in a wide range of applications, such as program verification, test case generation, IoT and Android security, etc. Unlike imperative languages, such as C or Java, Alloy is declarative, which describes the logic of a computation without describing its control flow and does not generate traces during the execution. Thus, traditional fault localization techniques developed for imperative programs based on analyzing the control flows of passing and failing tests do not directly apply to Alloy. To aid developers in debugging Alloy models, we develop FLACK, a tool to automatically localize Alloy buggy expressions.
Given an Alloy model with violated assertions, FLACK automatically outputs a ranking list of expressions based on their spaciousness to the assertions violations. For each assertion, FLACK first queries the Alloy analyzer for counterexamples, i.e. instances of the model that violate the asserted property. FLACK then uses a Partial Max-SAT (PMAXSAT) solver to find instances that satisfy the asserted property and are most similar to the counterexamples. FLACK then identifies the relations and atoms that are different between the counterexamples and the satisfying instances. The differences illustrate how the counterexamples violate the assertion. The PMAXSAT solver guarantees that these differences are “minimal”, containing only essential information related to the assertion violation. By finding expressions most related to these differences, FLACK identifies the potential expressions causing the assertion violation.
FLACK is different than the state of the art on Alloy fault localization in that it does not rely on unit tests which are not commonly found accompanying Alloy models. Instead, FLACK relies on assertions and constraint solvers to obtain counterexamples and satisfying instances, which are the main underlying technology in Alloy and commonly used by the Alloy developers. |
| format |
Objeto de conferencia Resumen |
| author |
Zheng, Guolong Nguyen, ThanhVu Gutiérrez Brida, Simón Regis, Germán Frias, Marcelo F. Aguirre, Nazareno Matías Bagheri, Hamid |
| author_facet |
Zheng, Guolong Nguyen, ThanhVu Gutiérrez Brida, Simón Regis, Germán Frias, Marcelo F. Aguirre, Nazareno Matías Bagheri, Hamid |
| author_sort |
Zheng, Guolong |
| title |
FLACK: Counterexample-Guided Fault Localization for Alloy Models |
| title_short |
FLACK: Counterexample-Guided Fault Localization for Alloy Models |
| title_full |
FLACK: Counterexample-Guided Fault Localization for Alloy Models |
| title_fullStr |
FLACK: Counterexample-Guided Fault Localization for Alloy Models |
| title_full_unstemmed |
FLACK: Counterexample-Guided Fault Localization for Alloy Models |
| title_sort |
flack: counterexample-guided fault localization for alloy models |
| publishDate |
2021 |
| url |
http://sedici.unlp.edu.ar/handle/10915/140263 http://50jaiio.sadio.org.ar/pdfs/asse/ASSE-04.pdf |
| work_keys_str_mv |
AT zhengguolong flackcounterexampleguidedfaultlocalizationforalloymodels AT nguyenthanhvu flackcounterexampleguidedfaultlocalizationforalloymodels AT gutierrezbridasimon flackcounterexampleguidedfaultlocalizationforalloymodels AT regisgerman flackcounterexampleguidedfaultlocalizationforalloymodels AT friasmarcelof flackcounterexampleguidedfaultlocalizationforalloymodels AT aguirrenazarenomatias flackcounterexampleguidedfaultlocalizationforalloymodels AT bagherihamid flackcounterexampleguidedfaultlocalizationforalloymodels |
| bdutipo_str |
Repositorios |
| _version_ |
1764820458496065536 |