Towards a test automation framework for alloy

Allison Sullivan, Razieh Nokhbeh Zaeem, Sarfraz Khurshid, Darko Marinov

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

Abstract

Writing declarative models of software designs and analyzing them to detect defects is an effective methodology for developing more dependable software systems. However, writing such models correctly can be challenging for practitioners who may not be proficient in declarative programming, and their models themselves may be buggy. We introduce the foundations of a novel test automation framework, A Unit, which we envision for testing declarative models written in Alloy-a first-order, relational language that is supported by its SAT-based analyzer. We take inspiration from the success of the family of x Unit frameworks that are used widely in practice for test automation, albeit for imperative or object-oriented programs. The key novelty of our work is to define a basis for unit testing for Alloy, specifically, to define the concepts of test case and coverage, and cover-age criteria for declarative models. We reduce the problems of declarative test execution and coverage computation to evaluation without requiring SAT solving. Our vision is to blend how developers write unit tests in commonly used programming languages with how Alloy users formulate their models in Alloy, thereby facilitating the development and testing of Alloy models for both new Alloy users as well as experts. We illustrate our ideas using a small but complex Alloy model. While we focus on Alloy, our ideas generalize to other declarative languages (such as Z, B, ASM).

Original languageEnglish (US)
Title of host publication2014 International SPIN Symposium on Model Checking of Software, SPIN 2014 - Proceedings
PublisherAssociation for Computing Machinery, Inc
Pages113-116
Number of pages4
ISBN (Electronic)9781450324526
DOIs
StatePublished - Jul 21 2014
Event21st International Symposium on Model Checking of Software, SPIN 2014 - San Jose, United States
Duration: Jul 21 2014Jul 23 2014

Publication series

Name2014 International SPIN Symposium on Model Checking of Software, SPIN 2014 - Proceedings

Other

Other21st International Symposium on Model Checking of Software, SPIN 2014
CountryUnited States
CitySan Jose
Period7/21/147/23/14

Keywords

  • Alloy
  • Code coverage
  • Coverage criteria
  • J Unit
  • Test case

ASJC Scopus subject areas

  • Artificial Intelligence
  • Computer Science Applications
  • Software

Fingerprint Dive into the research topics of 'Towards a test automation framework for alloy'. Together they form a unique fingerprint.

Cite this