Checking Java implementation of a naming architecture using TestEra

Sarfraz Khurshid, Darko Marinov

Research output: Contribution to journalConference articlepeer-review


TestEra is a novel framework for automated testing of Java programs. We have built TestEra upon Alloy, a lightweight first-order relational language, and the Alloy Analyzer, a fully automatic simulation and checking tool. Checking a Java program with TestEra involves modeling the correctness criteria for the program in Alloy and specifying abstraction and concretization translations between instances of Alloy models and Java data structures. TestEra automatically generates all non-isomorphic test cases within a given input size and verifies the correctness. We present our initial evaluation of TestEra performed by checking the Java implementation of a naming architecture for resource discovery in dynamic networked environments. Our study delineates the use of TestEra in testing methods for manipulating complex data structures.

Original languageEnglish (US)
Pages (from-to)322-342
Number of pages21
JournalElectronic Notes in Theoretical Computer Science
Issue number3
StatePublished - Oct 2001
Externally publishedYes
EventWorkshop on Software Model Checking (in Connection with CAV '01) - Paris, France
Duration: Jul 23 2001Jul 23 2001

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Checking Java implementation of a naming architecture using TestEra'. Together they form a unique fingerprint.

Cite this