Automatic generation of potentially pathological instances for validating alloy models

Takaya Saeki, Fuyuki Ishikawa, Shinichi Honiden

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

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationFormal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Proceedings
PublisherSpringer-Verlag
Pages41-56
Number of pages16
ISBN (Print)9783319478456
DOIs
Publication statusPublished - 2016 Jan 1
Externally publishedYes
Event18th International Conference on Formal Engineering Methods, ICFEM 2016 - Tokyo, Japan
Duration: 2016 Nov 142016 Nov 18

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10009 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other18th International Conference on Formal Engineering Methods, ICFEM 2016
CountryJapan
CityTokyo
Period16/11/1416/11/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Automatic generation of potentially pathological instances for validating alloy models'. Together they form a unique fingerprint.

  • Cite this

    Saeki, T., Ishikawa, F., & Honiden, S. (2016). Automatic generation of potentially pathological instances for validating alloy models. In Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Proceedings (pp. 41-56). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10009 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-47846-3_4