A Formal Model of the Safety-Critical Java Level 2 Paradigm

TL;DR

This paper introduces the first formal semantics for Safety-Critical Java Level 2, enabling rigorous reasoning about complex, concurrent, multi-processor applications for certification purposes.

Contribution

It provides a formal model of SCJ Level 2, capturing its state and behavior, which supports verification and reasoning techniques for safety-critical Java applications.

Findings

First formal semantics of SCJ Level 2

Model can be used to prove properties of SCJ programs

Supports refinement-based reasoning techniques

Abstract

Safety-Critical Java (SCJ) introduces a new programming paradigm for applications that must be certified. The SCJ specification (JSR 302) is an Open Group Standard, but it does not include verification techniques. Previous work has addressed verification for SCJ Level~1 programs. We support the much more complex SCJ Level~2 programs, which allows the programming of highly concurrent multi-processor applications with Java threads, and wait and notify mechanisms. We present a formal model of SCJ Level~2 that captures the state and behaviour of both SCJ programs and the SCJ API. This is the first formal semantics of the SCJ Level~2 paradigm and is an essential ingredient in the development of refinement-based reasoning techniques for SCJ Level~2 programs. We show how our models can be used to prove properties of the SCJ API and applications.