Supporting Development of Energy-Optimised Java Real-Time Systems using TetaSARTS

Kasper Søe Luckow, Thomas Bøgholm, Bent Thomsen

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review


This paper presents how the tool TetaSARTS can be used to support the development of embedded hard real-time systems written in Java using the emerging Safety Critical Java (SCJ) profile. TetaSARTS facilitates control-flow sensitive schedulability analysis of a set of real-time tasks, and features a pluggable platform specification allowing analysis of systems including the hosting execution environment. This is achieved by approaching the analysis as a model checking problem by modelling the system using the Timed Automata formalism of the model checking tool Uppaal. The resulting Timed Automata model facilitates easy adjustment of a wide variety of parameters that may be of interest such as processor frequency.

This paper demonstrates that TetaSARTS can be used for tuning processor frequency, for conducting control-flow sensitive Worst Case Response Time analysis, and for conducting processor utilisation and idle time analysis.
TidsskriftWiP Proceedings of the 19th IEEE Real-Time and Embedded Technology and Applications Symposium
Sider (fra-til)41-44
Antal sider4
StatusUdgivet - 2013
Begivenhed19th IEEE Real-Time and Embedded Technology and Applications Symposium - Hyatt Regency Philadelphia at Penn's Landing, Philadelphia, Pennsylvania, USA
Varighed: 10 apr. 201311 apr. 2013
Konferencens nummer: 19


Konference19th IEEE Real-Time and Embedded Technology and Applications Symposium
LokationHyatt Regency Philadelphia at Penn's Landing
ByPhiladelphia, Pennsylvania


  • Real-time
  • Temporal correctness
  • Real-time Java
  • Safety Critical Java
  • model checking
  • Analysis Tools