TY - GEN
T1 - Automatic generation of potentially pathological instances for validating alloy models
AU - Saeki, Takaya
AU - Ishikawa, Fuyuki
AU - Honiden, Shinichi
PY - 2016/1/1
Y1 - 2016/1/1
N2 - Alloy is a formal specification language that is widely used to verify software systems. However, while users can verify the properties of a specification with Alloy, it is not so easy for them to validate the specification, that is, to check that the specification is written just as the users intended. Alloy Analyzer, a tool supporting Alloy, has a feature to show concrete instances satisfying specifications that can be help in validation, but it does not control the order in which the instances are shown. Many studies have been conducted on ordering to help users explore instances in structured ways. However, not much prior research has focused on proper ways to explore instances for validating specifications. In this paper, we propose a method to assist users in validating specifications by displaying a set of instances that tend to include problems when their specifications have defects. In particular, the method applies pairwise testing to relations of Alloy specifications. We show effectiveness of the method in experiments using mutation analysis.
AB - Alloy is a formal specification language that is widely used to verify software systems. However, while users can verify the properties of a specification with Alloy, it is not so easy for them to validate the specification, that is, to check that the specification is written just as the users intended. Alloy Analyzer, a tool supporting Alloy, has a feature to show concrete instances satisfying specifications that can be help in validation, but it does not control the order in which the instances are shown. Many studies have been conducted on ordering to help users explore instances in structured ways. However, not much prior research has focused on proper ways to explore instances for validating specifications. In this paper, we propose a method to assist users in validating specifications by displaying a set of instances that tend to include problems when their specifications have defects. In particular, the method applies pairwise testing to relations of Alloy specifications. We show effectiveness of the method in experiments using mutation analysis.
UR - http://www.scopus.com/inward/record.url?scp=84995426613&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84995426613&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-47846-3_4
DO - 10.1007/978-3-319-47846-3_4
M3 - Conference contribution
AN - SCOPUS:84995426613
SN - 9783319478456
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 41
EP - 56
BT - Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Proceedings
PB - Springer-Verlag
T2 - 18th International Conference on Formal Engineering Methods, ICFEM 2016
Y2 - 14 November 2016 through 18 November 2016
ER -