A test suite for safety-critical Java using JML
Anders Peter Ravn, Hans Søndergaard · 2013
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.