White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

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

Marriott, Chris (2014) Checking Memory Safety of Level 1 Safety-Critical Java Programs using Static-Analysis without Annotations. PhD thesis, University of York.

Text (PhD Thesis)
Chris Marriott PhD Thesis.pdf
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (2685Kb) | Preview


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.

Item Type: Thesis (PhD)
Academic Units: The University of York > Computer Science (York)
Identification Number/EthosID: uk.bl.ethos.634372
Depositing User: Dr Chris Marriott
Date Deposited: 28 Jan 2015 12:13
Last Modified: 08 Sep 2016 13:32
URI: http://etheses.whiterose.ac.uk/id/eprint/7758

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)