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%3A03096842" target="_blank" >RIV/68407700:21230/04:03096842 - 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
Analysis of OSEK/VDX Based Automotive Applications
Popis výsledku v původním jazyce
The aim of this article is to show, how an automotive real-time software application running under real-time operating system compliant with OSEK/VDX standard can be modelled by timed automata. The application under consideration consists of several basic or extended tasks, it includes resource sharing and synchronisation by events. For such system, model checking theory based on timed automata and implemented in model checking tools can be used for verifying complex time and logical properties of proposed model. Use of this methodology is demonstrated on the automotive case study. The automated transmission system and its control software running under OSEK compliant operating system are modelled and properties necessary for its proper function are verified by model checker UPPAAL.
Název v anglickém jazyce
Analysis of OSEK/VDX Based Automotive Applications
Popis výsledku anglicky
The aim of this article is to show, how an automotive real-time software application running under real-time operating system compliant with OSEK/VDX standard can be modelled by timed automata. The application under consideration consists of several basic or extended tasks, it includes resource sharing and synchronisation by events. For such system, model checking theory based on timed automata and implemented in model checking tools can be used for verifying complex time and logical properties of proposed model. Use of this methodology is demonstrated on the automotive case study. The automated transmission system and its control software running under OSEK compliant operating system are modelled and properties necessary for its proper function are verified by model checker UPPAAL.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
JC - Počítačový hardware a software
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/LN00B096" target="_blank" >LN00B096: Výzkumné centrum aplikované kybernetiky</a><br>
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
Proceedings of IFAC Symposium on "Advances in Automotive Control"
ISBN
—
ISSN
—
e-ISSN
—
Počet stran výsledku
6
Strana od-do
212-217
Název nakladatele
Elsevier
Místo vydání
Oxford
Místo konání akce
Salerno
Datum konání akce
19. 4. 2004
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—