TY - GEN
T1 - Towards a test automation framework for alloy
AU - Sullivan, Allison
AU - Zaeem, Razieh Nokhbeh
AU - Khurshid, Sarfraz
AU - Marinov, Darko
N1 - Publisher Copyright:
Copyright 2014 ACM.
PY - 2014/7/21
Y1 - 2014/7/21
N2 - 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).
AB - 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).
KW - Alloy
KW - Code coverage
KW - Coverage criteria
KW - J Unit
KW - Test case
UR - http://www.scopus.com/inward/record.url?scp=84942324632&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84942324632&partnerID=8YFLogxK
U2 - 10.1145/2632362.2632369
DO - 10.1145/2632362.2632369
M3 - Conference contribution
AN - SCOPUS:84942324632
T3 - 2014 International SPIN Symposium on Model Checking of Software, SPIN 2014 - Proceedings
SP - 113
EP - 116
BT - 2014 International SPIN Symposium on Model Checking of Software, SPIN 2014 - Proceedings
PB - Association for Computing Machinery
T2 - 21st International Symposium on Model Checking of Software, SPIN 2014
Y2 - 21 July 2014 through 23 July 2014
ER -