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

Autor:	Thomas Bøgholm, Bent Thomsen, Anders P. Ravn, Kasper Søe Luckow, Lone Leth
Přispěvatelé:	Aceto, Luca, Bacci, Giorgio, Bacci, Giovanni, Ingólfsdóttir, Anna, Legay, Axel, Mardare, Radu
Rok vydání:	2017
Předmět:	Model checking Java Computer science business.industry Real-time computing Overshoot (signal) ComputerSystemsOrganization_SPECIAL-PURPOSEANDAPPLICATION-BASEDSYSTEMS Extension (predicate logic) Software engineering business computer Statistical model checking computer.programming_language
Zdroj:	Lecture Notes in Computer Science ISBN: 9783319631202 Models, Algorithms, Logics and Tools 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 . 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
DOI:	10.1007/978-3-319-63121-9_14
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a05dae028bf571ad58363bcb7841389d https://doi.org/10.1007/978-3-319-63121-9_14 Zobrazit plný text záznamu