Vše

Co hledáte?

Vše
Projekty
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

Statistical Model Checking of Processor Systems in Various Interrupt Scenarios

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F18%3APU130708" target="_blank" >RIV/00216305:26230/18:PU130708 - isvavai.cz</a>

  • Výsledek na webu

    <a href="https://link.springer.com/chapter/10.1007%2F978-3-030-03421-4_26" target="_blank" >https://link.springer.com/chapter/10.1007%2F978-3-030-03421-4_26</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1007/978-3-030-03421-4_26" target="_blank" >10.1007/978-3-030-03421-4_26</a>

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    Statistical Model Checking of Processor Systems in Various Interrupt Scenarios

  • Popis výsledku v původním jazyce

    Many practical, especially real-time, systems are expected to be predictable under various sources of unpredictability. To cope with the expectation, a system must be modeled and analyzed precisely for various operating conditions. This represents a problem that  grows with the dynamics of the system and that must be, typically, solved before the system starts to operate.  Due to the general complexity of the problem, this paper focuses just to processor based systems with interruptible executions. Their predictability analysis becomes more difficult especially when interrupts may occur at arbitrary times, suffer from arrival and servicing jitters, are subject to priorities, or may be nested and un/masked at run-time. Such a behavior of interrupts and executions has stochastic aspects and leads to the explosion of the number of situations to be considered.  To cope with such a behavior, we propose a simulation model that relies on a network of stochastic timed automata and involves the above-mentioned behavioral aspects related to  interrupts and executions. For a system, modeled by means of the automata, we show that the problem of analyzing its predictability may be efficiently solved by means of the statistical model checking.

  • Název v anglickém jazyce

    Statistical Model Checking of Processor Systems in Various Interrupt Scenarios

  • Popis výsledku anglicky

    Many practical, especially real-time, systems are expected to be predictable under various sources of unpredictability. To cope with the expectation, a system must be modeled and analyzed precisely for various operating conditions. This represents a problem that  grows with the dynamics of the system and that must be, typically, solved before the system starts to operate.  Due to the general complexity of the problem, this paper focuses just to processor based systems with interruptible executions. Their predictability analysis becomes more difficult especially when interrupts may occur at arbitrary times, suffer from arrival and servicing jitters, are subject to priorities, or may be nested and un/masked at run-time. Such a behavior of interrupts and executions has stochastic aspects and leads to the explosion of the number of situations to be considered.  To cope with such a behavior, we propose a simulation model that relies on a network of stochastic timed automata and involves the above-mentioned behavioral aspects related to  interrupts and executions. For a system, modeled by means of the automata, we show that the problem of analyzing its predictability may be efficiently solved by means of the statistical model checking.

Klasifikace

  • Druh

    D - Stať ve sborníku

  • CEP obor

  • OECD FORD obor

    10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Návaznosti výsledku

  • Projekt

    <a href="/cs/project/LQ1602" target="_blank" >LQ1602: IT4Innovations excellence in science</a><br>

  • Návaznosti

    P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Ostatní

  • Rok uplatnění

    2018

  • Kód důvěrnosti údajů

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

Údaje specifické pro druh výsledku

  • Název statě ve sborníku

    Proceedings of 8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)

  • ISBN

  • ISSN

    0302-9743

  • e-ISSN

  • Počet stran výsledku

    16

  • Strana od-do

    414-429

  • Název nakladatele

    Springer International Publishing

  • Místo vydání

    Cham

  • Místo konání akce

    Limassol

  • Datum konání akce

    5. 11. 2018

  • Typ akce podle státní příslušnosti

    WRD - Celosvětová akce

  • Kód UT WoS článku