Nástroje pro parametrickou verifikaci: srovnávací studie.

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F04%3APU49280" target="_blank" >RIV/00216305:26230/04:PU49280 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Tools for Parametric Verification. A Comparison on a Case Study

Popis výsledku v původním jazyce

Protocol analysis involves several parameters in model specification, for instance, transmission delay or the length of the transmitting window. Verification of the model with parameters is a semi-decision process that depends on the number of clocks, parameters and counters in the model. Using combination of different verification tools for timed models as <tt>HyTech</tt>, <tt>TReX</tt> and <tt>UPPaal</tt> we are able to find relation between parameters satisfying desired property. The paper gives a reeport on the synthesis of parameters of PGM protocol. We built a formal model based on extended time automata with parameters and verified the reliability property. Our results automatically obtained from the model are consistent with previous results derived manually. The paper describes our experience with parametric verification of multicast protocol PGM. Results mentioned in the work were made with collaboration with Mihaela Sighireanu<a href="http://www.liafa.jussieu.fr/%7Esighirea"

Název v anglickém jazyce

Tools for Parametric Verification. A Comparison on a Case Study

Popis výsledku anglicky

Protocol analysis involves several parameters in model specification, for instance, transmission delay or the length of the transmitting window. Verification of the model with parameters is a semi-decision process that depends on the number of clocks, parameters and counters in the model. Using combination of different verification tools for timed models as <tt>HyTech</tt>, <tt>TReX</tt> and <tt>UPPaal</tt> we are able to find relation between parameters satisfying desired property. The paper gives a reeport on the synthesis of parameters of PGM protocol. We built a formal model based on extended time automata with parameters and verified the reliability property. Our results automatically obtained from the model are consistent with previous results derived manually. The paper describes our experience with parametric verification of multicast protocol PGM. Results mentioned in the work were made with collaboration with Mihaela Sighireanu<a href="http://www.liafa.jussieu.fr/%7Esighirea"

Druh

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

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2004

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

Journal of Universal Computer Science

ISSN

0948-6968

e-ISSN

—

Svazek periodika

10

Číslo periodika v rámci svazku

10

Stát vydavatele periodika

AT - Rakouská republika

Počet stran výsledku

26

Strana od-do

1469-1494

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—