AUnit - a testing framework for alloy

dc.contributor.advisorKhurshid, Sarfraz
dc.creatorSullivan, Allisonen
dc.date.accessioned2014-10-09T21:13:32Zen
dc.date.issued2014-05en
dc.date.submittedMay 2014en
dc.date.updated2014-10-09T21:13:32Zen
dc.descriptiontexten
dc.description.abstractWriting 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, AUnit, 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 xUnit 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 test coverage as well as coverage criteria for declarative models. We reduce the problems of declarative test execution and coverage computation to partial 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).en
dc.description.departmentElectrical and Computer Engineeringen
dc.format.mimetypeapplication/pdfen
dc.identifier.urihttp://hdl.handle.net/2152/26426en
dc.language.isoenen
dc.subjectAlloyen
dc.subjectDeclarative testsen
dc.subjectCoverageen
dc.subjectTest automaton frameworken
dc.subjectUnit testsen
dc.subjectDeclarative modelen
dc.subjectPartial instancesen
dc.subjectDeclarative languagesen
dc.subjectPartial evaluationsen
dc.subjectSATen
dc.titleAUnit - a testing framework for alloyen
dc.typeThesisen
thesis.degree.departmentElectrical and Computer Engineeringen
thesis.degree.disciplineElectrical and Computer Engineeringen
thesis.degree.grantorThe University of Texas at Austinen
thesis.degree.levelMastersen
thesis.degree.nameMaster of Science in Engineeringen

Access full-text files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
SULLIVAN-THESIS-2014.pdf
Size:
656.94 KB
Format:
Adobe Portable Document Format

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
LICENSE.txt
Size:
1.85 KB
Format:
Plain Text
Description: