Verifikace distribuovanych systemu realneho casu casovanymi automaty.

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Timed Automata Approach to Real Time Distributed System Verification

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Timed Automata Approach to Real Time Distributed System Verification

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

JD - Využití počítačů, robotika a její aplikace

OECD FORD obor

—

Projekt

<a href="/cs/project/FD-K3%2F082" target="_blank" >FD-K3/082: *Návrhář pokročilých řídicích systémů.</a><br>

Návaznosti

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

Rok uplatnění

2004

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ů

Název statě ve sborníku

Proceedings of 2004 IEEE International Workshop on Factory Communication Systems

ISBN

0-7803-8734-1

ISSN

—

e-ISSN

—

Počet stran výsledku

4

Strana od-do

407-410

Název nakladatele

IEEE Industrial Electronic Society

Místo vydání

Vienna

Místo konání akce

Vienna

Datum konání akce

22. 9. 2004

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

WRD - Celosvětová akce

Kód UT WoS článku

—