Towards harnessing theories through tool support for hard real-time Java programming

Hans Søndergaard; Thomas Bøgholm; Christian Frost; Rene Rydhof Hansen; Casper Svenning Jensen; Kasper Søe Luckow; Anders P. Ravn; Bent Thomsen

Towards harnessing theories through tool support for hard real-time Java programming

Hans Søndergaard
, Thomas Bøgholm
, Christian Frost
, Rene Rydhof Hansen
, Casper Svenning Jensen
, Kasper Søe Luckow
, Anders P. Ravn
, Bent Thomsen

Software Technology Engineering

Aalborg University

Research output: Contribution to journal › Journal article › Research › peer-review

Abstract

We present a rationale for a selection of tools that assist developers of hard real-time applications to verify that programs conform to a Java real-time profile and that platform-specific resource constraints are satisfied. These tools are specialised instances of more generic static analysis and model checking frameworks. The concepts are illustrated by two case studies, and the strengths and the limitations of the tools are discussed.

Original language	English
Journal	Innovations in Systems and Software Engineering
Volume	8
Number of pages	12
ISSN	1614-5046
Publication status	Published - Jun 2012

Keywords

it
Java
Model checking
Real-time systems
Safety-critical
Static analysis

Access to Document

http://link.springer.com/content/pdf/10.1007%2Fs11334-012-0185-4

Cite this

@article{defb0809f3254b7ba7f0ceb1c65a7b5b,

title = "Towards harnessing theories through tool support for hard real-time Java programming",

abstract = "We present a rationale for a selection of tools that assist developers of hard real-time applications to verify that programs conform to a Java real-time profile and that platform-specific resource constraints are satisfied. These tools are specialised instances of more generic static analysis and model checking frameworks. The concepts are illustrated by two case studies, and the strengths and the limitations of the tools are discussed.",

keywords = "it, Java, Model checking, Real-time systems, Safety-critical, Static analysis",

author = "Hans S{\o}ndergaard and Thomas B{\o}gholm and Christian Frost and Hansen, \{Rene Rydhof\} and Jensen, \{Casper Svenning\} and Luckow, \{Kasper S{\o}e\} and Ravn, \{Anders P.\} and Bent Thomsen",

year = "2012",

month = jun,

language = "English",

volume = "8",

journal = "Innovations in Systems and Software Engineering",

issn = "1614-5046",

publisher = "Springer London",

}

TY - JOUR

T1 - Towards harnessing theories through tool support for hard real-time Java programming

AU - Søndergaard, Hans

AU - Bøgholm, Thomas

AU - Frost, Christian

AU - Hansen, Rene Rydhof

AU - Jensen, Casper Svenning

AU - Luckow, Kasper Søe

AU - Ravn, Anders P.

AU - Thomsen, Bent

PY - 2012/6

Y1 - 2012/6

N2 - We present a rationale for a selection of tools that assist developers of hard real-time applications to verify that programs conform to a Java real-time profile and that platform-specific resource constraints are satisfied. These tools are specialised instances of more generic static analysis and model checking frameworks. The concepts are illustrated by two case studies, and the strengths and the limitations of the tools are discussed.

AB - We present a rationale for a selection of tools that assist developers of hard real-time applications to verify that programs conform to a Java real-time profile and that platform-specific resource constraints are satisfied. These tools are specialised instances of more generic static analysis and model checking frameworks. The concepts are illustrated by two case studies, and the strengths and the limitations of the tools are discussed.

KW - it

KW - Java

KW - Model checking

KW - Real-time systems

KW - Safety-critical

KW - Static analysis

M3 - Journal article

SN - 1614-5046

VL - 8

JO - Innovations in Systems and Software Engineering

JF - Innovations in Systems and Software Engineering

ER -

Towards harnessing theories through tool support for hard real-time Java programming

Abstract

Keywords

Access to Document

Fingerprint

Cite this