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

Ahead-of-Time Algebraic Compilation for Safety-Critical Java

Baxter, James (2018) Ahead-of-Time Algebraic Compilation for Safety-Critical Java. PhD thesis, University of York.

This is the latest version of this item.

thesis.pdf - Examined Thesis (PDF)
Available under License Creative Commons Attribution 2.0 UK: England & Wales.

Download (1587Kb) | Preview


In recent years Java has been increasingly considered as a language for safety-critical embedded systems. However, some features of Java are unsuitable for such systems. This has resulted in the creation of Safety-Critical Java (SCJ), which facilitates the development of certifiable real-time and embedded Java programs. SCJ uses different scheduling and memory management models to standard Java, so it requires a specialised virtual machine (SCJVM). A common approach is to compile Java bytecode program to a native language, usually C, ahead-of-time for greater performance on low-resource embedded systems. Given the safety-critical nature of the applications, it must be ensured that the virtual machine is correct. However, so far, formal verification has not been applied to any SCJVM. This thesis contributes to the formal verification of SCJVMs that utilise ahead-of-time compilation by presenting a verification of compilation from Java bytecode to C. The approach we adopt is an adaptation of the algebraic approach developed by Sampaio and Hoare. We start with a formal specification of an SCJVM executing the bytecodes of a program, and transform it, through the application of proven compilation rules, to a representation of the target C code. Thus, our contributions are a formal specification of an SCJVM, a set of compilation rules with proofs, and a strategy for applying those compilation rules. Our compilation strategy can be used as the basis for an implementation of an ahead-of-time compiling SCJVM, or verification of an existing implementation. Additionally, our formal model of an SCJVM may be used as a specification for creating an interpreting SCJVM. To ensure the applicability of our results, we base our work on icecap, the only currently available SCJVM that is open source and up-to-date with the SCJ standard.

Item Type: Thesis (PhD)
Related URLs:
Academic Units: The University of York > Computer Science (York)
Identification Number/EthosID: uk.bl.ethos.766595
Depositing User: James Baxter
Date Deposited: 04 Feb 2019 14:17
Last Modified: 19 Feb 2020 13:07
URI: http://etheses.whiterose.ac.uk/id/eprint/22698

Available Versions of this Item

  • Ahead-of-Time Algebraic Compilation for Safety-Critical Java. (deposited 04 Feb 2019 14:17) [Currently Displayed]

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)