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

Research output: Contribution to book/anthology/report/conference proceedingBook chapterResearchpeer-review

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.
Original languageEnglish
Title of host publicationModels, Algorithms, Logics and Tools : Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday
EditorsLuca Aceto, Giorgio Bacci, Giovanni Bacci, Anna Ingólfsdóttir, Axel Legay, Radu Mardare
Number of pages20
Place of PublicationCham
PublisherSpringer
Publication date2017
Pages269-288
ISBN (Print)978-3-319-63121-9
DOIs
Publication statusPublished - 2017
EventEssays Dedicated to Kim Guldstrand Larsen
on the Occasion of His 60th Birthday
-
Duration: 25 Jul 2017 → …
https://link.springer.com/chapter/10.1007%2F978-3-319-63121-9_28

Other

OtherEssays Dedicated to Kim Guldstrand Larsen
on the Occasion of His 60th Birthday
Period25/07/2017 → …
Internet address
SeriesLecture Notes in Computer Science
Volume10460
ISSN0302-9743

Cite this

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. In L. Aceto, G. Bacci, G. Bacci, A. Ingólfsdóttir, A. Legay, & R. Mardare (Eds.), Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday (pp. 269-288). Cham: Springer. Lecture Notes in Computer Science, Vol.. 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. editor / Luca Aceto ; Giorgio Bacci ; Giovanni Bacci ; Anna Ingólfsdóttir ; Axel Legay ; Radu Mardare. Cham : Springer, 2017. pp. 269-288 (Lecture Notes in Computer Science, Vol. 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",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
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",
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. in L Aceto, G Bacci, G Bacci, A Ingólfsdóttir, A Legay & R Mardare (eds), 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, vol. 10460, pp. 269-288, Essays Dedicated to Kim Guldstrand Larsen
on the Occasion of His 60th Birthday, 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. ed. / Luca Aceto; Giorgio Bacci; Giovanni Bacci; Anna Ingólfsdóttir; Axel Legay; Radu Mardare. Cham : Springer, 2017. p. 269-288 (Lecture Notes in Computer Science, Vol. 10460).

Research output: Contribution to book/anthology/report/conference proceedingBook chapterResearchpeer-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

T3 - Lecture Notes in Computer Science

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. In Aceto L, Bacci G, Bacci G, Ingólfsdóttir A, Legay A, Mardare R, editors, Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. Cham: Springer. 2017. p. 269-288. (Lecture Notes in Computer Science, Vol. 10460). https://doi.org/10.1007/978-3-319-63121-9_14