Verification of FlexRay Start-up Mechanism by Timed Automata

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F10%3A00171753" target="_blank" >RIV/68407700:21230/10:00171753 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Verification of FlexRay Start-up Mechanism by Timed Automata

Popis výsledku v původním jazyce

Paper deals with the modelling of the mechanism ensuring the start-up of a FlexRay network. The model has been created with the use of timed automata and verified. For this purpose the UPPAAL software tool has been used that allows the modelling of discrete event systems with the use of timed automata, and subsequently the verification of the model with the use of suitable queries compiled in the so called computation tree logic. This model can be used to look for incorrect settings of time parameters of communication nodes in the network that prevent network start-up and subsequently the start of the car. The existence of this model also opens the way for finding possible errors in the standard. On the basis of the model, the work gives a case study of the start-up mechanism behaviour verification in a FlexRay network consisting of three communication nodes.

Název v anglickém jazyce

Verification of FlexRay Start-up Mechanism by Timed Automata

Popis výsledku anglicky

Paper deals with the modelling of the mechanism ensuring the start-up of a FlexRay network. The model has been created with the use of timed automata and verified. For this purpose the UPPAAL software tool has been used that allows the modelling of discrete event systems with the use of timed automata, and subsequently the verification of the model with the use of suitable queries compiled in the so called computation tree logic. This model can be used to look for incorrect settings of time parameters of communication nodes in the network that prevent network start-up and subsequently the start of the car. The existence of this model also opens the way for finding possible errors in the standard. On the basis of the model, the work gives a case study of the start-up mechanism behaviour verification in a FlexRay network consisting of three communication nodes.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/1M0568" target="_blank" >1M0568: Výzkumné centrum spalovacích motorů a automobilů Josefa Božka II</a><br>

Návaznosti

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

Rok uplatnění

2010

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 periodika

Metrology and Measurement Systems

ISSN

0860-8229

e-ISSN

—

Svazek periodika

17

Číslo periodika v rámci svazku

3

Stát vydavatele periodika

PL - Polská republika

Počet stran výsledku

20

Strana od-do

—

Kód UT WoS článku

000285569400013

EID výsledku v databázi Scopus

—