Automatic generation of potentially pathological instances for validating alloy models

Takaya Saeki*, Fuyuki Ishikawa, Shinichi Honiden

*この研究の対応する著者

研究成果: Conference contribution

1 被引用数 (Scopus)

抄録

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.

本文言語English
ホスト出版物のタイトルFormal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Proceedings
出版社Springer-Verlag
ページ41-56
ページ数16
ISBN(印刷版)9783319478456
DOI
出版ステータスPublished - 2016 1 1
外部発表はい
イベント18th International Conference on Formal Engineering Methods, ICFEM 2016 - Tokyo, Japan
継続期間: 2016 11 142016 11 18

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
10009 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Other

Other18th International Conference on Formal Engineering Methods, ICFEM 2016
国/地域Japan
CityTokyo
Period16/11/1416/11/18

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Automatic generation of potentially pathological instances for validating alloy models」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル