We present the test case generation method and tool KeYTestGen in the context of
real-time Java applications and libraries. The generated tests feature strong
coverage criteria, like the Modified Condition/Decision Criterion, by
construction. This is achieved by basing the test generation on formal
verification techniques, namely the KeY system for Java source code
verification. Moreover, we present formal specifications for the classes and
methods in the real-time Java API. These specifications are used for symbolic
execution when generating tests for real-time Java applications, and for oracle
construction when generating tests for real-time Java library
implementations. The latter application exhibited a mismatch between a
commercial library implementation and the official RTSJ documentation. Even if
there is a rationale behind this particular inconsistency, it demonstrates the
effectiveness of our method on production code.