Abstract
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.
Original language | English |
---|---|
Title of host publication | Proceedings of the 6th international workshop on Java technologies for real-time and embedded systems |
Volume | 343 |
Publisher | Association for Computing Machinery |
Publication date | 2008 |
Pages | 106-114 |
ISBN (Print) | 978-1-60558-337-2 |
DOIs | |
Publication status | Published - 2008 |
Event | International workshop on Java technologies for real-time and embedded systems - Santa Clara, California, United States Duration: 24 Sept 2008 → 26 Sept 2008 Conference number: 6 |
Conference
Conference | International workshop on Java technologies for real-time and embedded systems |
---|---|
Number | 6 |
Country/Territory | United States |
City | Santa Clara, California |
Period | 24/09/2008 → 26/09/2008 |