From Safety Critical Java Programs to Timed Process Models

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

4 Citationer (Scopus)

Resumé

The idea of analysing real programs by process algebraic
methods probably goes back to the Occam language using the CSP
process algebra [43]. In [16,24] Degano et al. followed in that tradition
by analysing Mobile Agent Programs written in the Higher Order Functional,
Concurrent and Distributed, programming language Facile [47],
by equipping Facile with a process algebraic semantics based on true concurrency.
This semantics facilitated analysis of programs revealing subtle
bugs that would otherwise be very hard to find. Inspired by the idea of
translating real programs into process algebraic frameworks, we have in
recent years pursued an agenda of translating hard-real-time embedded
safety critical programs written in the Safety Critical Java Profile [33]
into networks of timed automata [4] and subjecting those to automated
analysis using the UPPAAL model checker [10]. Several tools have been
built and the tools have been used to analyse a number of systems for
properties such as worst case execution time, schedulability and energy
optimization [12–14,19,34,36,38]. In this paper we will elaborate on the
theoretical underpinning of the translation from Java programs to timed
automata models and briefly summarize some of the results based on this
translation. Furthermore, we discuss future work, especially relations to
the work in [16,24] as Java recently has adopted first class higher order
functions in the form of lambda abstractions.
OriginalsprogEngelsk
TitelProgramming Languages with Applications to Biology and Security : Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday
RedaktørerChiara Bodei, Gian-Luigi Ferrari , Corrado Priami
Antal sider20
ForlagSpringer
Publikationsdato2015
Sider319-338
ISBN (Trykt)978-3-319-25526-2
ISBN (Elektronisk)978-3-319-25527-9
DOI
StatusUdgivet - 2015
NavnLecture Notes in Computer Science
Nummer9465
ISSN0302-9743

Fingerprint

Semantics
Mobile agents
Computer programming languages
Algebra

Citer dette

Thomsen, B., Luckow, K. S., Thomsen, L. L., & Bøgholm, T. (2015). From Safety Critical Java Programs to Timed Process Models. I C. Bodei, G-L. Ferrari , & C. Priami (red.), Programming Languages with Applications to Biology and Security: Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday (s. 319-338). Springer. Lecture Notes in Computer Science, Nr. 9465 https://doi.org/10.1007/978-3-319-25527-9_21
Thomsen, Bent ; Luckow, Kasper Søe ; Thomsen, Lone Leth ; Bøgholm, Thomas. / From Safety Critical Java Programs to Timed Process Models. Programming Languages with Applications to Biology and Security: Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday. red. / Chiara Bodei ; Gian-Luigi Ferrari ; Corrado Priami. Springer, 2015. s. 319-338 (Lecture Notes in Computer Science; Nr. 9465).
@inproceedings{00989cc968fe43b9bbc08191856b0532,
title = "From Safety Critical Java Programs to Timed Process Models",
abstract = "The idea of analysing real programs by process algebraicmethods probably goes back to the Occam language using the CSPprocess algebra [43]. In [16,24] Degano et al. followed in that traditionby analysing Mobile Agent Programs written in the Higher Order Functional,Concurrent and Distributed, programming language Facile [47],by equipping Facile with a process algebraic semantics based on true concurrency.This semantics facilitated analysis of programs revealing subtlebugs that would otherwise be very hard to find. Inspired by the idea oftranslating real programs into process algebraic frameworks, we have inrecent years pursued an agenda of translating hard-real-time embeddedsafety critical programs written in the Safety Critical Java Profile [33]into networks of timed automata [4] and subjecting those to automatedanalysis using the UPPAAL model checker [10]. Several tools have beenbuilt and the tools have been used to analyse a number of systems forproperties such as worst case execution time, schedulability and energyoptimization [12–14,19,34,36,38]. In this paper we will elaborate on thetheoretical underpinning of the translation from Java programs to timedautomata models and briefly summarize some of the results based on thistranslation. Furthermore, we discuss future work, especially relations tothe work in [16,24] as Java recently has adopted first class higher orderfunctions in the form of lambda abstractions.",
author = "Bent Thomsen and Luckow, {Kasper S{\o}e} and Thomsen, {Lone Leth} and Thomas B{\o}gholm",
year = "2015",
doi = "10.1007/978-3-319-25527-9_21",
language = "English",
isbn = "978-3-319-25526-2",
pages = "319--338",
editor = "Chiara Bodei and {Ferrari }, Gian-Luigi and Corrado Priami",
booktitle = "Programming Languages with Applications to Biology and Security",
publisher = "Springer",
address = "Germany",

}

Thomsen, B, Luckow, KS, Thomsen, LL & Bøgholm, T 2015, From Safety Critical Java Programs to Timed Process Models. i C Bodei, G-L Ferrari & C Priami (red), Programming Languages with Applications to Biology and Security: Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday. Springer, Lecture Notes in Computer Science, nr. 9465, s. 319-338. https://doi.org/10.1007/978-3-319-25527-9_21

From Safety Critical Java Programs to Timed Process Models. / Thomsen, Bent; Luckow, Kasper Søe; Thomsen, Lone Leth; Bøgholm, Thomas.

Programming Languages with Applications to Biology and Security: Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday. red. / Chiara Bodei; Gian-Luigi Ferrari ; Corrado Priami. Springer, 2015. s. 319-338 (Lecture Notes in Computer Science; Nr. 9465).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - From Safety Critical Java Programs to Timed Process Models

AU - Thomsen, Bent

AU - Luckow, Kasper Søe

AU - Thomsen, Lone Leth

AU - Bøgholm, Thomas

PY - 2015

Y1 - 2015

N2 - The idea of analysing real programs by process algebraicmethods probably goes back to the Occam language using the CSPprocess algebra [43]. In [16,24] Degano et al. followed in that traditionby analysing Mobile Agent Programs written in the Higher Order Functional,Concurrent and Distributed, programming language Facile [47],by equipping Facile with a process algebraic semantics based on true concurrency.This semantics facilitated analysis of programs revealing subtlebugs that would otherwise be very hard to find. Inspired by the idea oftranslating real programs into process algebraic frameworks, we have inrecent years pursued an agenda of translating hard-real-time embeddedsafety critical programs written in the Safety Critical Java Profile [33]into networks of timed automata [4] and subjecting those to automatedanalysis using the UPPAAL model checker [10]. Several tools have beenbuilt and the tools have been used to analyse a number of systems forproperties such as worst case execution time, schedulability and energyoptimization [12–14,19,34,36,38]. In this paper we will elaborate on thetheoretical underpinning of the translation from Java programs to timedautomata models and briefly summarize some of the results based on thistranslation. Furthermore, we discuss future work, especially relations tothe work in [16,24] as Java recently has adopted first class higher orderfunctions in the form of lambda abstractions.

AB - The idea of analysing real programs by process algebraicmethods probably goes back to the Occam language using the CSPprocess algebra [43]. In [16,24] Degano et al. followed in that traditionby analysing Mobile Agent Programs written in the Higher Order Functional,Concurrent and Distributed, programming language Facile [47],by equipping Facile with a process algebraic semantics based on true concurrency.This semantics facilitated analysis of programs revealing subtlebugs that would otherwise be very hard to find. Inspired by the idea oftranslating real programs into process algebraic frameworks, we have inrecent years pursued an agenda of translating hard-real-time embeddedsafety critical programs written in the Safety Critical Java Profile [33]into networks of timed automata [4] and subjecting those to automatedanalysis using the UPPAAL model checker [10]. Several tools have beenbuilt and the tools have been used to analyse a number of systems forproperties such as worst case execution time, schedulability and energyoptimization [12–14,19,34,36,38]. In this paper we will elaborate on thetheoretical underpinning of the translation from Java programs to timedautomata models and briefly summarize some of the results based on thistranslation. Furthermore, we discuss future work, especially relations tothe work in [16,24] as Java recently has adopted first class higher orderfunctions in the form of lambda abstractions.

U2 - 10.1007/978-3-319-25527-9_21

DO - 10.1007/978-3-319-25527-9_21

M3 - Article in proceeding

SN - 978-3-319-25526-2

SP - 319

EP - 338

BT - Programming Languages with Applications to Biology and Security

A2 - Bodei, Chiara

A2 - Ferrari , Gian-Luigi

A2 - Priami, Corrado

PB - Springer

ER -

Thomsen B, Luckow KS, Thomsen LL, Bøgholm T. From Safety Critical Java Programs to Timed Process Models. I Bodei C, Ferrari G-L, Priami C, red., Programming Languages with Applications to Biology and Security: Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday. Springer. 2015. s. 319-338. (Lecture Notes in Computer Science; Nr. 9465). https://doi.org/10.1007/978-3-319-25527-9_21