A Novel Approach to Modechart Verification of Real-Time systems

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F11%3APU96140" target="_blank" >RIV/00216305:26230/11:PU96140 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

A Novel Approach to Modechart Verification of Real-Time systems

Popis výsledku v původním jazyce

Because real-time systems are often time-critical applications and their failure can have fatal consequences, it is important to ensure their correct behaviour. There exist many approaches for verification of real-time systems. Some use graphical formalisms, other various kinds of logics, to describe the system being verified. While graphical description can be significantly easier to use, it disallows to utilise many powerful methods for analysis and verification. In this paper, we propose a new approach for verification of real-time systems described by the Modechart graphical formalism by transforming the computation of the system onto a set of restricted real-time logic (RRTL) formulae. Moreover, if the verified property is known in advance, we areable to reduce the number of resulting RRTL formulae.

Název v anglickém jazyce

A Novel Approach to Modechart Verification of Real-Time systems

Popis výsledku anglicky

Because real-time systems are often time-critical applications and their failure can have fatal consequences, it is important to ensure their correct behaviour. There exist many approaches for verification of real-time systems. Some use graphical formalisms, other various kinds of logics, to describe the system being verified. While graphical description can be significantly easier to use, it disallows to utilise many powerful methods for analysis and verification. In this paper, we propose a new approach for verification of real-time systems described by the Modechart graphical formalism by transforming the computation of the system onto a set of restricted real-time logic (RRTL) formulae. Moreover, if the verified property is known in advance, we areable to reduce the number of resulting RRTL formulae.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2011

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 statě ve sborníku

Proceedings of the 13th International Conference on Computer Aided Systems Theory

ISBN

978-84-693-9560-8

ISSN

—

e-ISSN

—

Počet stran výsledku

2

Strana od-do

338-339

Název nakladatele

The Universidad de Las Palmas de Gran Canaria

Místo vydání

Universidad de Las Palmas de Canaria

Místo konání akce

Las Palmas de Gran Canaria, Canary Islands

Datum konání akce

6. 2. 2011

Typ akce podle státní příslušnosti

EUR - Evropská akce

Kód UT WoS článku

—