Over-approximate Model of Multitasking Application Based on Timed Automata Using Only One Clock

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F05%3A03110427" target="_blank" >RIV/68407700:21230/05:03110427 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Over-approximate Model of Multitasking Application Based on Timed Automata Using Only One Clock

Original language description

The aim of this article 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.

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

<a href="/en/project/1ET400750406" target="_blank" >1ET400750406: Participation in the evolution of the standardization for embedded software for automotive industry</a><br>

Continuities

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

Publication year

2005

Confidentiality

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

ISBN

0-7695-2312-9

Place of publication

Los Alamitos

Publisher/client name

—

Version

—

Carrier ID

neuvedeno