Using Circus to Verify Safety-Critical Java Level 2 Programs

10^th May 2018, 14:00
Matthew Luckcuck

Abstract

Safety-Critical Java (SCJ) is a Java-based programming language designed for real-time and safety-critical programs. It has been developed from the Real-Time Specification for Java. SCJ provides a strict memory- and programming- model. SCJ is organised into three ascending levels of complexity from Level 0 (the simplest) to Level 2 (the most complex).

This work makes three contributions to the state of the art on veri?cation of SCJ Level 2 programs. Firstly, I model the SCJ Level 2 paradigm using the state-rich process algebra Circus. My model can be used to identify potential errors in the programs that it represents. Secondly, because I model the API separately from the program-speci?c behaviour, my model can be used to show that the SCJ API does not introduce undesirable behaviour, such as deadlock or livelock. Finally, my model enables several options for verifying SCJ Level 2 programs.