Static checking of safety critical Java annotations

The Safety Critical Java Specification intends to support the development of programs that must be certified. The specification includes a number of annotations used to constrain the behavior of programs written against it. This paper describes and motivates the design of these annotations and the rules used to check statically that programs respect their intended semantics. We report on a prototype implementation with the Java Checker Framework and initial experiments annotating a 24KLoc application. Categories and Subject Descriptors D.3.4 [Programming Languages]: Processors--run-time environments; D.3.3 [Programming Languages]: Language Constructs and Features--classes and objects; D.4.7 [Operating Systems]: Organization and Design--real-time systems and embedded systems. General Terms Languages, Experimentation. Keywords Safety Critical Systems, Verification, Annotations, Memory Safety.

• Type: Conference
• Year: 2010
• Where: JTRES
• Authors: Daniel Tang, Ales Plsek, Jan Vitek
• Keywords: Annotations, Embedded Systems, JTRES 2010, Safety Critical, Safety Critical Java