TetaSARTS: A tool for modular timing analysis of safety critical Java systems

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

6 Citations (Scopus)


We describe the design and the capabilities of the static timing analysis tool TetaSARTS that assists in temporal verification of Safety Critical Java (SCJ) systems. The primary functionality of TetaSARTS is schedulability analysis, which takes into account the scheduling policy and task interactions. TetaSARTS also facilitates analysing processor utilisation and idle time, Worst Case Execution Time, Worst Case Response Time, and Worst Case Blocking Time.

In the analyses, TetaSARTS accounts for the execution environment hosting the analysed system; both hardware implementations of the Java Virtual Machine as well as software implementations hosted on common embedded hardware are supported. Several parameters of the execution environment can be adjusted prior to performing the analyses e.g. the clock frequency of the hardware.

The enabling technology for supporting the analyses and for achieving high flexibility is model checking. In a process resembling the stages of an optimising compiler, TetaSARTS translates the SCJ system into a Network of Timed Automata amenable to model checking using the Uppaal model checker.
Original languageEnglish
Title of host publicationProceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems
Number of pages10
PublisherAssociation for Computing Machinery
Publication date2013
ISBN (Print)978-1-4503-2166-2
Publication statusPublished - 2013
EventThe 11th International Workshop on Java Technologies for Real-Time and Embedded Systems - Karlsruhe, Germany
Duration: 9 Oct 201310 Oct 2013
Conference number: 11


WorkshopThe 11th International Workshop on Java Technologies for Real-Time and Embedded Systems
SeriesProceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems

Cite this