Timed Automata Approach to CAN Verification

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Timed Automata Approach to CAN Verification

Original language description

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.

Czech name

Není k dispozici

Czech description

Není k dispozici

Type

A - Audiovisual production

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2004

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

ISBN

—

Place of publication

Laxenburg

Publisher/client name

—

Version

—

Carrier ID

neuvedeno