Formal Verification of Multitasking Applications Based on Timed Automata Model

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F08%3A03139311" target="_blank" >RIV/68407700:21230/08:03139311 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Formal Verification of Multitasking Applications Based on Timed Automata Model

Original language description

The aim of this paper is to show, how a multitasking application running under a real-time operating system compliant with an OSEK/VDX standard can be modeled by timed automata. The application under consideration consists of several non-preemptive tasksand interrupt service routines that can be synchronized by events. A model checking tool is used to verify time and logical properties of the proposed model. Use of this methodology is demonstrated on an automated gearbox case study and the result of the worst-case response time verification is compared with the classical method based on the time-demand analysis. It is shown that the model-checking approach provides less pessimistic results due to a more detailed model and exhaustive state-space exploration

Czech name

Formální verifikace vícevláknových aplikací založená na časovaných automatech

Czech description

Článek ukazuje jak lze pomocí časovaných automatů modelovat vícevláknové aplikace běžící pod operačním systémem reálného času kompatibilního se standardem OSEK-VDX. Uvažovaná aplikace se skládá z několika nepreemptivních úloh a obslužných rutin přerušení, které mohou být synchronizovány pomocí událostí. Nástroj pro Model-Checking je použit k verifikaci časových a logických vlastností navrženého modelu. Použití navržené metodologie je demonstrováno na automatické převodovce a výsledek verifikace nejhoršího reakčního času je je porovnán s klasickými metodami založenými na metodách time-demand analýzy. Je ukázáno, že náš přístup je méně pesimistický díky detailnějšímu modelu a úplnému prohledávání stavového prostoru

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

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

Publication year

2008

Confidentiality

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

Name of the periodical

Real-Time Systems

ISSN

0922-6443

e-ISSN

—

Volume of the periodical

38

Issue of the periodical within the volume

1

Country of publishing house

US - UNITED STATES

Number of pages

27

Pages from-to

—

UT code for WoS article

000251900900002

EID of the result in the Scopus database

—