Sciweavers

Share
JTRES
2010
ACM

Static checking of safety critical Java annotations

9 years 8 months ago
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.
Daniel Tang, Ales Plsek, Jan Vitek
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where JTRES
Authors Daniel Tang, Ales Plsek, Jan Vitek
Comments (0)
books