Evaluating state modeling techniques in alloy

Allison Sullivan, Kaiyuan Wang, Sarfraz Khurshid, Darko Marinov

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

Abstract

Software models help develop higher quality systems. The declarative language Alloy and its accompanying automatic analyzer embody a method for developing software models. Our focus in this paper is Alloy models of systems where different operations may mutate the system state, e.g., addition of an element to a sorted container. Researchers have previously used two techniques for modeling state and state mutation in Alloy, but these techniques have not been compared to each other. We propose a third technique and evaluate all these three techniques that embody conceptually different modeling approaches. We use four core subjects, which we model using each technique. Our primary goal is to quantitatively evaluate the techniques by considering the runtime for solving the ensuing SAT formulas. We also discuss practical tradeoffs among the techniques.

Original languageEnglish (US)
Title of host publicationSQAMIA 2017 - Proceedings of the 6th Workshop on Software Quality Analysis, Monitoring, Improvement, and Applications
EditorsZoran Budimac
PublisherCEUR-WS
ISBN (Electronic)9788670313552
StatePublished - Jan 1 2017
Event6th Workshop on Software Quality Analysis, Monitoring, Improvement, and Applications, SQAMIA 2017 - Belgrade, Serbia
Duration: Sep 11 2017Sep 13 2017

Publication series

NameCEUR Workshop Proceedings
Volume1938
ISSN (Print)1613-0073

Other

Other6th Workshop on Software Quality Analysis, Monitoring, Improvement, and Applications, SQAMIA 2017
CountrySerbia
CityBelgrade
Period9/11/179/13/17

Keywords

  • Alloy
  • Empirical evaluation
  • Predicate parameterization
  • SAT solving
  • State modeling

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Evaluating state modeling techniques in alloy'. Together they form a unique fingerprint.

Cite this