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%2F04%3A03098675" target="_blank" >RIV/68407700:21230/04:03098675 - 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
Timed Automata Approach to CAN Verification
Popis výsledku v původním jazyce
This article deals with verification of real time distributed system focusing on CAN model by timed automata and specification of verified properties by temporal logic. Such system, based on several CPUs, consists of an application SW running under real-time operating system (e.g. OSEK) and using standard broadcast communications based on the Controller Area Network (CAN). The crucial problem is to verify both, the time properties (e.g. message response time) and logic properties (e.g. deadlock) of suchcomplex applications. The approach presented in this article is based on the modeling the discrete event system by Timed Automata and on verification by model checking tool (e.g. UPPAAL). In contrast to classical approaches dealing either with shared bus (guarantee message latencies approached by Tindell and Burns) or shared processor (rate monotonic analysis), our approach deals with both kinds of resources.
Název v anglickém jazyce
Timed Automata Approach to CAN Verification
Popis výsledku anglicky
This article deals with verification of real time distributed system focusing on CAN model by timed automata and specification of verified properties by temporal logic. Such system, based on several CPUs, consists of an application SW running under real-time operating system (e.g. OSEK) and using standard broadcast communications based on the Controller Area Network (CAN). The crucial problem is to verify both, the time properties (e.g. message response time) and logic properties (e.g. deadlock) of suchcomplex applications. The approach presented in this article is based on the modeling the discrete event system by Timed Automata and on verification by model checking tool (e.g. UPPAAL). In contrast to classical approaches dealing either with shared bus (guarantee message latencies approached by Tindell and Burns) or shared processor (rate monotonic analysis), our approach deals with both kinds of resources.
Klasifikace
Druh
A - Audiovizuální tvorba
CEP obor
JC - Počítačový hardware a software
OECD FORD obor
—
Návaznosti výsledku
Projekt
—
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
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ů
Údaje specifické pro druh výsledku
ISBN
—
Místo vydání
Laxenburg
Název nakladatele resp. objednatele
—
Verze
—
Identifikační číslo nosiče
neuvedeno