All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

Timed Automata Approach to Real Time Distributed System Verification

The result's identifiers

  • Result code in IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F04%3A03100263" target="_blank" >RIV/68407700:21230/04:03100263 - isvavai.cz</a>

  • Result on the web

  • DOI - Digital Object Identifier

Alternative languages

  • Result language

    angličtina

  • Original language name

    Timed Automata Approach to Real Time Distributed System Verification

  • Original language description

    This article deals with a distributed real-time application modelling by timed automata. The application under consideration consists of several processors communicating via Controller Area Network (CAN); each processor executes an application that consists of tasks running under an operating system (e.g. OSEK) and using inter-task synchronization primitives. For such system, model checking algorithm implemented in a model checking tool (e.g. UPAALL) can be used to verify complex time and logical properties of the proposed model (e.g. end-to-end response time, state reachability, deadlock freeness). Since the proposed timed automata model contains more crucial details of the system behavior with respect to classical approaches to the response time analysis, the model checking approach provides less pessimistic results in many cases.

  • Czech name

    Verifikace distribuovanych systemu realneho casu casovanymi automaty.

  • Czech description

    Tato prace popisuje jak verifikovat rozprostrene systemy realneho casu pomoci casovanych automatu. Zamnerujeme se na systemy pouzivajici Controller Area Network (CAN) jako sbernici a predpokladame ze na kazdem CPU bezi operacni system realneho casu. Pomoci casovanych jsme schopni verifikovat nejen logicke vlastnosti, ale tez casove (uvaznuti atd.). K porovnani s tradicnimi metodami je nase metoda preciznejsi.

Classification

  • Type

    D - Article in proceedings

  • CEP classification

    JD - Use of computers, robotics and its application

  • OECD FORD branch

Result continuities

  • Project

    <a href="/en/project/FD-K3%2F082" target="_blank" >FD-K3/082: *Advance control system designer.</a><br>

  • Continuities

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

Others

  • Publication year

    2004

  • Confidentiality

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

Data specific for result type

  • Article name in the collection

    Proceedings of 2004 IEEE International Workshop on Factory Communication Systems

  • ISBN

    0-7803-8734-1

  • ISSN

  • e-ISSN

  • Number of pages

    4

  • Pages from-to

    407-410

  • Publisher name

    IEEE Industrial Electronic Society

  • Place of publication

    Vienna

  • Event location

    Vienna

  • Event date

    Sep 22, 2004

  • Type of event by nationality

    WRD - Celosvětová akce

  • UT code for WoS article