The Design of SafeJML, a Specification Language for SCJ With Support for WCET Specification

Safety-Critical Java (SCJ) is a dialect of Java that allows programmers to implement safety-critical systems, such as software to control airplanes, medical devices, and nuclear power plants. SafeJML extends the Java Modeling Language (JML) to allow specification and checking of both functional and timing constraints for SCJ programs. When the authors' design of the SafeJML is implemented, it will help check the correctness of detailed designs, including timing for real-time systems written in SCJ.