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