Model-based schedulability analysis of safety critical hard real-time Java programs

In this paper, we present a novel approach to schedulability

analysis of Safety Critical Hard Real-Time Java programs.

The approach is based on a translation of programs, written

in the Safety Critical Java profile introduced in [21] for the

Java Optimized Processor [18], to timed automata models

verifiable by the Uppaal model checker [23]. Schedulability

analysis is reduced to a simple reachability question, checking

for deadlock freedom. Model-based schedulability analysis

has been developed by Amnell et al. [2], but has so

far only been applied to high level specifications, not actual

implementations in a programming language. Experiments

show that model-based schedulability analysis can result in

a more accurate analysis than possible with traditional approaches,

thus systems deemed non-schedulable by traditional

approaches may in fact be schedulable, as detected

by our analysis.

Our approach has been implemented in a tool, named

SARTS, successfully used to verify the schedulability of a

real-time sorting machine consisting of two periodic and two

sporadic tasks. SARTS has also been applied on a number of

smaller examples to investigate properties of our approach.