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%3A03113392" target="_blank" >RIV/68407700:21230/05:03113392 - 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 Distributed and Fault Tolerant System Verification
Popis výsledku v původním jazyce
The aim of this work 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. The flexibility of the proposed approach is demonstrated on the model of distributed systems based on CAN bus and model of fault tolerant SW method based on recovery blocks.
Název v anglickém jazyce
Timed Automata Approach to Distributed and Fault Tolerant System Verification
Popis výsledku anglicky
The aim of this work 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. The flexibility of the proposed approach is demonstrated on the model of distributed systems based on CAN bus and model of fault tolerant SW method based on recovery blocks.
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/1M0567" target="_blank" >1M0567: Centrum aplikované kybernetiky</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
—
Místo vydání
Praha
Název nakladatele resp. objednatele
—
Verze
—
Identifikační číslo nosiče
neuvedeno