Checking Memory Safety of Level 1 Safety-Critical Java Programs using Static-Analysis without Annotations

Safety-Critical Java (SCJ) has been designed specifically to ring performance and reliability to the development of safety-critical Java programs. SCJ introduces a novel programming paradigm based on missions and handlers, and has been designed to ease certification. One of the distinguishing features of SCJ is its memory model, which is defined as a hierarchical structure of scoped-based memory areas. Unlike in Java programs, memory management is an important concern under the control of the programmer in SCJ; it is not sufficient to write a program that conforms to the specification as memory safety may still be broken.
By using static analysis techniques, it is possible to identify errors in programs before they are executed. Analysing at the source-code level allows for a precise analysis that abstracts away from machine details and unnecessary program details. As the SCJ paradigm is different to that of Java, it is not possible to apply existing tools and techniques for Java programs to SCJ.
This thesis describes a new static-checking technique for a comprehensive subset of SCJ programs (comparable to Ravenscar Ada) that automatically checks for memory-safety violations at the source-code level without the need for user-added annotations. An abstract language (SCJ-mSafe) is used to describe the aspects of SCJ programs required to
check memory safety, and a set of inference rules define what it means for each aspect to be memory safe. By using a points-to environment and automatically-generated method
properties, it is possible to produce a model of the execution of an SCJ program that can identify possible memory-safety violations at each point in the execution. The whole process has been automated with tool support and compared against other techniques. A worst-case analysis is performed that can give false negatives.