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”

Není k dispozici

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F05%3A03110427" target="_blank" >RIV/68407700:21230/05:03110427 - isvavai.cz</a>

  • Výsledek na webu

  • DOI - Digital Object Identifier

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    Over-approximate Model of Multitasking Application Based on Timed Automata Using Only One Clock

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

    The aim of this article is to show, how a multitasking application running under real-time operating system compliant with OSEK/VDX standard can be modeled by timed automata. The application under consideration consists of several tasks, it includes resource sharing and synchronization by events. For such system, we use model checking theory based on timed automata and we verify time and logical properties of proposed model by existing model checking tools. Since a complexity of the model-checking verification exponentially grows with the number of clocks used in a model, the proposed model uses only one clock for measuring execution time of all modeled tasks.

  • Název v anglickém jazyce

    Over-approximate Model of Multitasking Application Based on Timed Automata Using Only One Clock

  • Popis výsledku anglicky

    The aim of this article is to show, how a multitasking application running under real-time operating system compliant with OSEK/VDX standard can be modeled by timed automata. The application under consideration consists of several tasks, it includes resource sharing and synchronization by events. For such system, we use model checking theory based on timed automata and we verify time and logical properties of proposed model by existing model checking tools. Since a complexity of the model-checking verification exponentially grows with the number of clocks used in a model, the proposed model uses only one clock for measuring execution time of all modeled tasks.

Klasifikace

  • Druh

    A - Audiovizuální tvorba

  • CEP obor

    JC - Počítačový hardware a software

  • OECD FORD obor

Návaznosti výsledku

  • Projekt

    <a href="/cs/project/1ET400750406" target="_blank" >1ET400750406: Participace na vývoji evropské standardizace vestavného software pro automobilový průmysl</a><br>

  • Návaznosti

    P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Ostatní

  • Rok uplatnění

    2005

  • 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

  • ISBN

    0-7695-2312-9

  • Místo vydání

    Los Alamitos

  • Název nakladatele resp. objednatele

  • Verze

  • Identifikační číslo nosiče

    neuvedeno