ModelJUnit extends JUnit to support model-based testing, with the models being written as Java classes. Model-based testing allows you to automatically generate test suites from a model of a system under test.
Switching from Spec Explorer, I found ModelJUnit a very good MBT tool for Java users. Advantages: simple, easy to use, fast-but-efficient exploration algorithms. Disadvantages: no test data generation and data coverage report, no depth-first-search exploration. In general, this is a very good MBT tool among the ones I tried. Will post some improvement requests/bug report in the Bug Tracker.