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%3APU49144" target="_blank" >RIV/00216305:26230/04:PU49144 - 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 involve several parameters in model specification, for instance, transmission delay or the length of the transmitting window. Verification of the model&nbsp; with parameters is semi-decision process that depends on number of clocks, parameters and counters in&nbsp; the model. Using combination of different verification tools for timed models as HyTech, TReX and Uppaal we are able to find relation between parameters satisfying desired property. The paper gives a report on synthesis of pparameters of PGM protocol RFC3208. 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 experiences with parametric verification of multicast protocol PGM. Results mentioned in the work were made with collaboration with Mihaela Sighireanu from LIAFA, Paris. <br>

Název v anglickém jazyce

Tools for Parametric Verification: A Comparison on a Case Study.

Popis výsledku anglicky

Protocol analysis involve several parameters in model specification, for instance, transmission delay or the length of the transmitting window. Verification of the model&nbsp; with parameters is semi-decision process that depends on number of clocks, parameters and counters in&nbsp; the model. Using combination of different verification tools for timed models as HyTech, TReX and Uppaal we are able to find relation between parameters satisfying desired property. The paper gives a report on synthesis of pparameters of PGM protocol RFC3208. 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 experiences with parametric verification of multicast protocol PGM. Results mentioned in the work were made with collaboration with Mihaela Sighireanu from LIAFA, Paris. <br>

Druh

D - Stať ve sborníku

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

Proceedings of the 5th Joint Workshop on FSCBS

ISBN

1-85769-1970

ISSN

—

e-ISSN

—

Počet stran výsledku

10

Strana od-do

45-54

Název nakladatele

University of Stirling

Místo vydání

Stirling

Místo konání akce

Brno

Datum konání akce

26. 5. 2004

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

WRD - Celosvětová akce

Kód UT WoS článku

—