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

Abstrakt

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
UdgivelsesstedCham
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

Citationsformater