A Test Suite for Safety-Critical Java using JML

Development techniques are presented for a test suite for the draft specification of the Java profile for Safety-Critical Systems. Distinguishing features are: specification of conformance constraints in the Java Modeling Language, encoding of infrastructure concepts without implementation bias, and corresponding specifications of implicitly stated behavioral and real-time properties. The test programs are auto-generated from the specification, while concrete values for test parameters are selected manually. The suite is open source and publicly accessible