ASketch: A sketching framework for alloy

Kaiyuan Wang, Allison Sullivan, Darko Marinov, Sarfraz Khurshid

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

Abstract

Alloy is a declarative modeling language that supports first-order logic with transitive closure. Alloy has been used in a variety of domains to model software systems and find design deficiencies. However, it is often challenging to make an Alloy model correct or to debug a faulty Alloy model. ASketch is a sketching/synthesis technique that can help users write correct Alloy models. ASketch allows users to provide a partial Alloy model with holes, a generator that specifies candidate fragments to be considered for each hole, and a set of tests that capture the desired model properties. Then, the tool completes the holes such that all tests for the completed model pass. ASketch uses tests written for the recently introduced AUnit framework, which provides a foundation of testing (unit tests, test execution, and model coverage) for Alloy models in the spirit of traditional unit testing. This paper describes our Java implementation of ASketch, which is a command-line tool, released as an open-source project on GitHub. Our experimental results show that ASketch can handle partial Alloy models with multiple holes and a large search space.

Original languageEnglish (US)
Title of host publicationESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering
EditorsAlessandro Garci, Corina S. Pasareanu, Gary T. Leavens
PublisherAssociation for Computing Machinery, Inc
Pages916-919
Number of pages4
ISBN (Electronic)9781450355735
DOIs
StatePublished - Oct 26 2018
Event26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018 - Lake Buena Vista, United States
Duration: Nov 4 2018Nov 9 2018

Publication series

NameESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Other

Other26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018
CountryUnited States
CityLake Buena Vista
Period11/4/1811/9/18

Keywords

  • ASketch
  • Sketching
  • first-order logic

ASJC Scopus subject areas

  • Software
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'ASketch: A sketching framework for alloy'. Together they form a unique fingerprint.

  • Cite this

    Wang, K., Sullivan, A., Marinov, D., & Khurshid, S. (2018). ASketch: A sketching framework for alloy. In A. Garci, C. S. Pasareanu, & G. T. Leavens (Eds.), ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering (pp. 916-919). (ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering). Association for Computing Machinery, Inc. https://doi.org/10.1145/3236024.3264594