
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.
Safety Critical Java, Analysis Tools, Temporal correctness, Real-time Java, Real-time, model checking
Safety Critical Java, Analysis Tools, Temporal correctness, Real-time Java, Real-time, model checking
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
