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

Safety-Critical Java Level 2: Applications, Modelling, and Verification

Luckcuck, Matthew (2016) Safety-Critical Java Level 2: Applications, Modelling, and Verification. PhD thesis, University of York.

This is the latest version of this item.

Matthew Luckcuck PhD Thesis.pdf - Examined Thesis (PDF)
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (1489Kb) | Preview


Safety-Critical Java (SCJ) introduces a new programming paradigm for applications that must be certified. To aid certification, SCJ is organised into three compliance levels, which increase in complexity from Level 0 to Level 2. The SCJ language specification (JSR 302) is an Open Group Standard, but it does not include verification techniques. Previous work has addressed verification for Level 0 and Level 1 programs. This thesis supports the much more complex SCJ Level 2 programs, which allow for the programming of highly concurrent multi-processor applications with Java threads, and wait and notify mechanisms. The SCJ language specification is clear on what constitutes a Level 2 program but not why it should be used. The utility of Levels 0 and 1 are clear from their features. The scheduling behaviour required by a program is a primary indicator of whether or not Level 0 should be used. However, both Levels 1 and 2 use concurrency and fixed-priority scheduling, so this cannot be used as an indicator to choose between them. This thesis presents the first examination of utility of the unique features of Level 2 and presents use cases that justify the availability of these features. This thesis presents a technique for modelling SCJ Level 2 programs using the state-rich process algebra Circus. The model abstracts away from resources (for example, memory) and scheduling. An SCJ Level 2 program is represented by a combination of a generic model of the SCJ API (the framework model) and an application-specific model (the application model) of that program. The framework model is reused for each modelled program, whereas the application model is generated afresh. This is the first formal semantics of the SCJ Level 2 paradigm and it provides both top-down and bottom-up benefits. Top-down, it is an essential ingredient in the development of refinement-based reasoning techniques for SCJ Level 2 programs. These can be used to develop Level 2 programs that are correct-by-construction. Bottom-up, the technique can be used as a verification tool for Level 2 programs. This is achieved with the Failures Divergences Refinement checker version 3 (FDR3), after translating the model from Circus to the machine readable version of CSP (CSPM). FDR3 allows animation and model checking, which can reveal sources of deadlock, livelock, and divergence. The CSPM version of the model fits the same pattern, with a generic model of the API being combined with an application-specific model of the program. Because the model ignores scheduling, these checks are a worst-case analysis and can give false-negatives.

Item Type: Thesis (PhD)
Academic Units: The University of York > Computer Science (York)
Identification Number/EthosID: uk.bl.ethos.721890
Depositing User: Dr Matthew Luckcuck
Date Deposited: 31 Aug 2017 10:54
Last Modified: 24 Jul 2018 15:22
URI: http://etheses.whiterose.ac.uk/id/eprint/17743

Available Versions of this Item

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)