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

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

6 Citationer (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.

Originalsprog	Engelsk
Titel	Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems
Antal sider	10
Forlag	Association for Computing Machinery
Publikationsdato	2013
Udgave	11
Sider	11-20
ISBN (Trykt)	978-1-4503-2166-2
DOI	https://doi.org/10.1145/2512989.2512992
Status	Udgivet - 2013
Begivenhed	The 11th International Workshop on Java Technologies for Real-Time and Embedded Systems - Karlsruhe, Tyskland Varighed: 9 okt. 2013 → 10 okt. 2013 Konferencens nummer: 11

Workshop

Workshop	The 11th International Workshop on Java Technologies for Real-Time and Embedded Systems
Nummer	11
Land/Område	Tyskland
By	Karlsruhe
Periode	09/10/2013 → 10/10/2013

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

Emneord

model checking
uppaal
real-time
java
program analysis
timing analysis

Adgang til dokumentet

10.1145/2512989.2512992

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

6 Citationer
1 Ph.d.-afhandling

Platforms and Model-Based Analyses for Real-Time Java
Luckow, K. S., 2014, Department of Computer Science, Aalborg University.
Publikation: Ph.d.-afhandling

Citationsformater

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. udg. Association for Computing Machinery, 2013. s. 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",

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. i Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems. 11 udg, Association for Computing Machinery, Proceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems, s. 11-20, The 11th International Workshop on Java Technologies for Real-Time and Embedded Systems, Karlsruhe, Tyskland, 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. udg. Association for Computing Machinery, 2013. s. 11-20 (Proceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems).

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › 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

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. I Proceedings of the 11th International Workshop on Java Technologies for Real-time and Embedded Systems. 11 udg. Association for Computing Machinery. 2013. s. 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

Emneord

Adgang til dokumentet

AUB Link

Publikation

Platforms and Model-Based Analyses for Real-Time Java

Citationsformater