TestEra: A tool for testing Java programs using alloy specifications

Shadi Abdul Khalek, Guowei Yang, Lingming Zhang, Darko Marinov, Sarfraz Khurshid

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

Abstract

This tool paper presents an embodiment of TestEra - a framework developed in previous work for specification-based testing of Java programs. To test a Java method, TestEra uses the method's pre-condition specification to generate test inputs and the post-condition to check correctness of outputs. TestEra supports specifications written in Alloy - a first-order, declarative language based on relations - and uses the SAT-based back-end of the Alloy tool-set for systematic generation of test suites. Each test case is a JUnit test method, which performs three key steps: (1) initialization of pre-state, i.e., creation of inputs to the method under test; (2) invocation of the method; and (3) checking the correctness of post-state, i.e., checking the method output. The tool supports visualization of inputs and outputs as object graphs for graphical illustration of method behavior. TestEra is available for download to be used as a library or as an Eclipse plug-in.

Original languageEnglish (US)
Title of host publication2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings
Pages608-611
Number of pages4
DOIs
StatePublished - Dec 1 2011
Event2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011 - Lawrence, KS, United States
Duration: Nov 6 2011Nov 10 2011

Publication series

Name2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings

Other

Other2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011
CountryUnited States
CityLawrence, KS
Period11/6/1111/10/11

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'TestEra: A tool for testing Java programs using alloy specifications'. Together they form a unique fingerprint.

Cite this