Using Uppaal for Verification of Priority Assignment in Real-Time Databases

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F11%3A86080823" target="_blank" >RIV/61989100:27240/11:86080823 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-22410-2_34" target="_blank" >http://dx.doi.org/10.1007/978-3-642-22410-2_34</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-22410-2_34" target="_blank" >10.1007/978-3-642-22410-2_34</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Using Uppaal for Verification of Priority Assignment in Real-Time Databases

Popis výsledku v původním jazyce

Model checking, as one area of formal verification, is recently subject of an intensive research. Many verification tools intended to check properties of models of systems were developed, mainly at universities. Many researches are also interested in real-time database management systems (RTDBMS). This article is focused on some possibilities of using a verification tool Uppaal on some variants of priority assignment algorithms used in RTDBMS. In the article are presented some possible models of such algorithms expressed as nets of timed automata, which are a modeling language of Uppaal and then some simulation and verification possibilities of Uppaal on those models.

Název v anglickém jazyce

Using Uppaal for Verification of Priority Assignment in Real-Time Databases

Popis výsledku anglicky

Model checking, as one area of formal verification, is recently subject of an intensive research. Many verification tools intended to check properties of models of systems were developed, mainly at universities. Many researches are also interested in real-time database management systems (RTDBMS). This article is focused on some possibilities of using a verification tool Uppaal on some variants of priority assignment algorithms used in RTDBMS. In the article are presented some possible models of such algorithms expressed as nets of timed automata, which are a modeling language of Uppaal and then some simulation and verification possibilities of Uppaal on those models.

Druh

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

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)

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 periodika

Communications in Computer and Information Science

ISSN

1865-0929

e-ISSN

—

Svazek periodika

189

Číslo periodika v rámci svazku

—

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

15

Strana od-do

385-399

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—