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

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.