Verifikace pomoci casovanych automatu v distribuovanych systemech
Popis výsledku
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. K porovnani s tradicnimi metodami je nase metoda preciznejsi.
Klíčová slova
Controller Area NetworkDistributed Control SystemModel-checkingTimed Automata
Identifikátory výsledku
Kód výsledku v IS VaVaI
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 Verification of Distributed Systems
Popis výsledku v původním jazyce
The goal of the article is verification of real time distributed system focusing on CAN model by timed automata and specification of verified properties by temporal logic. Such system consists of an application SW running under real-time operating systemand using broadcast communications based on the CAN. The approach is based on the modelling the discrete event system by Timed Automata and on verification by model checking tool. In contrast to classical approaches dealing either with shared bus or shared processor, our approach deals with both kinds of resources.
Název v anglickém jazyce
Timed Automata Approach to Verification of Distributed Systems
Popis výsledku anglicky
The goal of the article is verification of real time distributed system focusing on CAN model by timed automata and specification of verified properties by temporal logic. Such system consists of an application SW running under real-time operating systemand using broadcast communications based on the CAN. The approach is based on the modelling the discrete event system by Timed Automata and on verification by model checking tool. In contrast to classical approaches dealing either with shared bus or shared processor, our approach deals with both kinds of resources.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
JC - Počítačový hardware a software
OECD FORD obor
—
Návaznosti výsledku
Projekt
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
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
Název statě ve sborníku
8th International Student Conference on Electrical Engineering, POSTER 2004, May 20 2004, Prague
ISBN
—
ISSN
—
e-ISSN
—
Počet stran výsledku
4
Strana od-do
—
Název nakladatele
ČVUT v Praze, FEL
Místo vydání
Praha
Místo konání akce
Prague
Datum konání akce
20. 5. 2004
Typ akce podle státní příslušnosti
EUR - Evropská akce
Kód UT WoS článku
—
Druh výsledku
D - Stať ve sborníku
CEP
JC - Počítačový hardware a software
Rok uplatnění
2004