Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking

Anders P. Ravn, Bent Thomsen, Kasper Søe Luckow, Lone Leth Thomsen, Thomas Bøgholm

Publikation: Bidrag til bog/antologi/rapport/konference proceedingBidrag til bog/antologiForskningpeer review

Resumé

In cyber-physical applications many programs have hard real-time constraints that have to be stringently validated. In some applications, there are programs that have hard deadlines, which must not be violated. Other programs have soft deadlines where the value of the response decreases when the deadline is passed although it is still a valid response. In between, there are programs with firm deadlines. Here the response may be occasionally delayed; but this should not happen too often or with too large an overshoot. This paper presents an extension to an existing approach and tool for checking hard deadline constraints to the case of firm deadlines for application programs written in Safety-Critical Java (SCJ). The existing approach uses models and model checking with the Uppaal toolset; the extension uses the statistical model checking features of Uppaal-smc to provide a hold on firm deadlines and performance in the case of soft deadlines. The extended approach is illustrated with examples from applications.
OriginalsprogEngelsk
TitelModels, Algorithms, Logics and Tools : Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday
RedaktørerLuca Aceto, Giorgio Bacci, Giovanni Bacci, Anna Ingólfsdóttir, Axel Legay, Radu Mardare
Antal sider20
Udgivelses stedCham
ForlagSpringer
Publikationsdato2017
Sider269-288
ISBN (Trykt)978-3-319-63121-9
DOI
StatusUdgivet - 2017
BegivenhedEssays Dedicated to Kim Guldstrand Larsen
on the Occasion of His 60th Birthday
-
Varighed: 25 jul. 2017 → …
https://link.springer.com/chapter/10.1007%2F978-3-319-63121-9_28

Andet

AndetEssays Dedicated to Kim Guldstrand Larsen
on the Occasion of His 60th Birthday
Periode25/07/2017 → …
Internetadresse
NavnLecture Notes in Computer Science
Vol/bind10460
ISSN0302-9743

Citer dette

Ravn, A. P., Thomsen, B., Søe Luckow, K., Thomsen, L. L., & Bøgholm, T. (2017). Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking. I L. Aceto, G. Bacci, G. Bacci, A. Ingólfsdóttir, A. Legay, & R. Mardare (red.), Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday (s. 269-288). Cham: Springer. Lecture Notes in Computer Science, Bind. 10460 https://doi.org/10.1007/978-3-319-63121-9_14
Ravn, Anders P. ; Thomsen, Bent ; Søe Luckow, Kasper ; Thomsen, Lone Leth ; Bøgholm, Thomas. / Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking. Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. red. / Luca Aceto ; Giorgio Bacci ; Giovanni Bacci ; Anna Ingólfsdóttir ; Axel Legay ; Radu Mardare. Cham : Springer, 2017. s. 269-288 (Lecture Notes in Computer Science, Bind 10460).
@inbook{33428f93e1534f3cbb2a016c204f758e,
title = "Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking",
abstract = "In cyber-physical applications many programs have hard real-time constraints that have to be stringently validated. In some applications, there are programs that have hard deadlines, which must not be violated. Other programs have soft deadlines where the value of the response decreases when the deadline is passed although it is still a valid response. In between, there are programs with firm deadlines. Here the response may be occasionally delayed; but this should not happen too often or with too large an overshoot. This paper presents an extension to an existing approach and tool for checking hard deadline constraints to the case of firm deadlines for application programs written in Safety-Critical Java (SCJ). The existing approach uses models and model checking with the Uppaal toolset; the extension uses the statistical model checking features of Uppaal-smc to provide a hold on firm deadlines and performance in the case of soft deadlines. The extended approach is illustrated with examples from applications.",
author = "Ravn, {Anders P.} and Bent Thomsen and {S{\o}e Luckow}, Kasper and Thomsen, {Lone Leth} and Thomas B{\o}gholm",
year = "2017",
doi = "10.1007/978-3-319-63121-9_14",
language = "English",
isbn = "978-3-319-63121-9",
pages = "269--288",
editor = "Luca Aceto and Giorgio Bacci and Giovanni Bacci and Anna Ing{\'o}lfsd{\'o}ttir and Axel Legay and Radu Mardare",
booktitle = "Models, Algorithms, Logics and Tools",
publisher = "Springer",
address = "Germany",

}

Ravn, AP, Thomsen, B, Søe Luckow, K, Thomsen, LL & Bøgholm, T 2017, Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking. i L Aceto, G Bacci, G Bacci, A Ingólfsdóttir, A Legay & R Mardare (red), Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. Springer, Cham, Lecture Notes in Computer Science, bind 10460, s. 269-288, 25/07/2017. https://doi.org/10.1007/978-3-319-63121-9_14

Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking. / Ravn, Anders P.; Thomsen, Bent; Søe Luckow, Kasper; Thomsen, Lone Leth; Bøgholm, Thomas.

Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. red. / Luca Aceto; Giorgio Bacci; Giovanni Bacci; Anna Ingólfsdóttir; Axel Legay; Radu Mardare. Cham : Springer, 2017. s. 269-288 (Lecture Notes in Computer Science, Bind 10460).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingBidrag til bog/antologiForskningpeer review

TY - CHAP

T1 - Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking

AU - Ravn, Anders P.

AU - Thomsen, Bent

AU - Søe Luckow, Kasper

AU - Thomsen, Lone Leth

AU - Bøgholm, Thomas

PY - 2017

Y1 - 2017

N2 - In cyber-physical applications many programs have hard real-time constraints that have to be stringently validated. In some applications, there are programs that have hard deadlines, which must not be violated. Other programs have soft deadlines where the value of the response decreases when the deadline is passed although it is still a valid response. In between, there are programs with firm deadlines. Here the response may be occasionally delayed; but this should not happen too often or with too large an overshoot. This paper presents an extension to an existing approach and tool for checking hard deadline constraints to the case of firm deadlines for application programs written in Safety-Critical Java (SCJ). The existing approach uses models and model checking with the Uppaal toolset; the extension uses the statistical model checking features of Uppaal-smc to provide a hold on firm deadlines and performance in the case of soft deadlines. The extended approach is illustrated with examples from applications.

AB - In cyber-physical applications many programs have hard real-time constraints that have to be stringently validated. In some applications, there are programs that have hard deadlines, which must not be violated. Other programs have soft deadlines where the value of the response decreases when the deadline is passed although it is still a valid response. In between, there are programs with firm deadlines. Here the response may be occasionally delayed; but this should not happen too often or with too large an overshoot. This paper presents an extension to an existing approach and tool for checking hard deadline constraints to the case of firm deadlines for application programs written in Safety-Critical Java (SCJ). The existing approach uses models and model checking with the Uppaal toolset; the extension uses the statistical model checking features of Uppaal-smc to provide a hold on firm deadlines and performance in the case of soft deadlines. The extended approach is illustrated with examples from applications.

U2 - 10.1007/978-3-319-63121-9_14

DO - 10.1007/978-3-319-63121-9_14

M3 - Book chapter

SN - 978-3-319-63121-9

SP - 269

EP - 288

BT - Models, Algorithms, Logics and Tools

A2 - Aceto, Luca

A2 - Bacci, Giorgio

A2 - Bacci, Giovanni

A2 - Ingólfsdóttir, Anna

A2 - Legay, Axel

A2 - Mardare, Radu

PB - Springer

CY - Cham

ER -

Ravn AP, Thomsen B, Søe Luckow K, Thomsen LL, Bøgholm T. Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking. I Aceto L, Bacci G, Bacci G, Ingólfsdóttir A, Legay A, Mardare R, red., Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. Cham: Springer. 2017. s. 269-288. (Lecture Notes in Computer Science, Bind 10460). https://doi.org/10.1007/978-3-319-63121-9_14