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

Kasper Søe Luckow; Thomas Bøgholm; Bent Thomsen; Kim Guldstrand Larsen

doi:10.1145/2512989.2512992

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

Kasper Søe Luckow, Thomas Bøgholm, Bent Thomsen, Kim Guldstrand Larsen

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

6 Citations (Scopus)

Abstract

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 language	English
Title of host publication	Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems
Number of pages	10
Publisher	Association for Computing Machinery (ACM)
Publication date	2013
Edition	11
Pages	11-20
ISBN (Print)	978-1-4503-2166-2
DOIs	https://doi.org/10.1145/2512989.2512992
Publication status	Published - 2013
Event	The 11th International Workshop on Java Technologies for Real-Time and Embedded Systems - Karlsruhe, Germany Duration: 9 Oct 2013 → 10 Oct 2013 Conference number: 11

Workshop

Workshop	The 11th International Workshop on Java Technologies for Real-Time and Embedded Systems
Number	11
Country/Territory	Germany
City	Karlsruhe
Period	09/10/2013 → 10/10/2013

Series	Proceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems
ISSN	2154-056X

Access to Document

10.1145/2512989.2512992

AUB Link

Search for the material in Aalborg University Library's search engine

6 Citations
1 PhD thesis

Platforms and Model-Based Analyses for Real-Time Java
Luckow, K. S., 2014, Department of Computer Science, Aalborg University.
Research output: PhD thesis

Cite this

Luckow, Kasper Søe ; Bøgholm, Thomas ; Thomsen, Bent et al. / TetaSARTS : A tool for modular timing analysis of safety critical Java systems. Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems. 11. ed. Association for Computing Machinery (ACM), 2013. pp. 11-20 (Proceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems).

@inproceedings{cc68b9760e2e4004981925ff3b1259a5,

title = "TetaSARTS: A tool for modular timing analysis of safety critical Java systems",

abstract = "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.",

keywords = "model checking, uppaal, real-time, java, program analysis, timing analysis",

author = "Luckow, {Kasper S{\o}e} and Thomas B{\o}gholm and Bent Thomsen and Larsen, {Kim Guldstrand}",

year = "2013",

doi = "10.1145/2512989.2512992",

language = "English",

isbn = "978-1-4503-2166-2",

series = "Proceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems",

pages = "11--20",

booktitle = "Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems",

publisher = "Association for Computing Machinery (ACM)",

address = "United States",

edition = "11",

note = "The 11th International Workshop on Java Technologies for Real-Time and Embedded Systems ; Conference date: 09-10-2013 Through 10-10-2013",

}

Luckow, KS, Bøgholm, T, Thomsen, B & Larsen, KG 2013, TetaSARTS: A tool for modular timing analysis of safety critical Java systems. in Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems. 11 edn, Association for Computing Machinery (ACM), Proceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems, pp. 11-20, The 11th International Workshop on Java Technologies for Real-Time and Embedded Systems, Karlsruhe, Germany, 09/10/2013. https://doi.org/10.1145/2512989.2512992

TetaSARTS: A tool for modular timing analysis of safety critical Java systems. / Luckow, Kasper Søe; Bøgholm, Thomas; Thomsen, Bent et al.
Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems. 11. ed. Association for Computing Machinery (ACM), 2013. p. 11-20 (Proceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

T1 - TetaSARTS

T2 - The 11th International Workshop on Java Technologies for Real-Time and Embedded Systems

AU - Luckow, Kasper Søe

AU - Bøgholm, Thomas

AU - Thomsen, Bent

AU - Larsen, Kim Guldstrand

N1 - Conference code: 11

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

KW - model checking

KW - uppaal

KW - real-time

KW - java

KW - program analysis

KW - timing analysis

U2 - 10.1145/2512989.2512992

DO - 10.1145/2512989.2512992

M3 - Article in proceeding

SN - 978-1-4503-2166-2

T3 - Proceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems

SP - 11

EP - 20

BT - Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems

PB - Association for Computing Machinery (ACM)

Y2 - 9 October 2013 through 10 October 2013

ER -

Luckow KS, Bøgholm T, Thomsen B , Larsen KG. TetaSARTS: A tool for modular timing analysis of safety critical Java systems. In Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems. 11 ed. Association for Computing Machinery (ACM). 2013. p. 11-20. (Proceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems). doi: 10.1145/2512989.2512992

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

Abstract

Workshop

Access to Document

AUB Link

Research output

Platforms and Model-Based Analyses for Real-Time Java

Cite this