Using Statistical Model Checker for Schedulability Analysis of Real-Time Systems Under Uncertainty

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F26%3A0198918" target="_blank" >RIV/00216305:26230/26:0198918 - isvavai.cz</a>

Result on the web

<a href="https://link.springer.com/chapter/10.1007/978-3-032-01377-4_13" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-032-01377-4_13</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-032-01377-4_13" target="_blank" >10.1007/978-3-032-01377-4_13</a>

Result language

angličtina

Original language name

Using Statistical Model Checker for Schedulability Analysis of Real-Time Systems Under Uncertainty

Original language description

Schedulability analysis aims to decide whether it is possible to meet the timing constraints of the given subset of real-time tasks that will be scheduled by the given policy and executed on the given platform. For some situations (classes of systems and conditions), a guaranteed/proven schedulability analysis method exists. As such a method may be absent for other situations and there may be a practical need to cope with the schedulability analysis in such problematic (but realistic, burdened with uncertainty) situations, the analysis must rely on alternative means. This paper presents some of the situations (related, e.g., to the drift of a clock and OSTime, event/interrupt management, task design patterns or OS components such as a scheduler and task queues) that represent a problem for guaranteed approaches first. Then, it presents our approach for interruptible CPU-based systems; it builds on a simulation model over a network of stochastic timed automata, an instrument able to cope with such situations. To analyze schedulability, we apply the statistical model-checking technique to our model. The technique has already shown to easily scale to complex dynamic systems as well as to efficiently solve various problems. Our results indicate that the model and the technique are appropriate for schedulability analysis in realistic situations, where the computational complexity and result of the analysis are driven by predefined parameters such as the degree of confidence.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

20205 - Automation and control systems

Project

—

Continuities

S - Specificky vyzkum na vysokych skolach

Publication year

2025

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Lecture Notes in Computer Science, Bridging the Gap Between AI and Reality

ISBN

978-3-032-01376-7

ISSN

—

e-ISSN

—

Number of pages

24

Pages from-to

233-256

Publisher name

Springer Nature Switzerland

Place of publication

Cham

Event location

Crete, Greece

Event date

Oct 30, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—