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 our design of the SafeJML is implemented, it will help check the correctness of detailed designs, including timing for real-time systems written in SCJ. Categories and Subject Descriptors C.3 [Special-Purpose and Application-Based Systems]: Realtime and embedded systems; C.4 [Performance of Systems]: Measurement techniques, performance attributes; D.2.1 [Software Engineering]: Requirements/Specifications Languages, tools; D.2.4 [Software Engineering]: Software/Program Verification Assertion checkers,formal methods, programming by contract, validation; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about ProgramsAsser...

• Type: Conference
• Year: 2010
• Where: JTRES
• Authors: Ghaith Haddad, Faraz Hussain, Gary T. Leavens
• Keywords: Embedded Systems, Java Modeling Language, JTRES 2010, Safety-Critical Java, Systems