Publication detail
Tools for Parametric Verification. A Comparison on a Case Study
MATOUŠEK, P.
Original Title
Tools for Parametric Verification. A Comparison on a Case Study
Type
journal article - other
Language
English
Original Abstract
Protocol analysis involves several parameters inmodel specification, for instance, transmission delay or the length ofthe transmitting window. Verification of the model with parameters isa semi-decision process that depends on the number of clocks,parameters and counters in the model. Using combination of differentverification tools for timed models as HyTech, TReX and UPPaal we areable to find relation between parameters satisfying desiredproperty. The paper gives a report on the synthesis of parameters ofPGM protocol. We built a formal model based on extended time automatawith parameters and verified the reliability property. Our resultsautomatically obtained from the model are consistent with previousresults derived manually. The paper describes our experience withparametric verification of multicast protocol PGM. Results mentionedin the work were made with collaboration with MihaelaSighireanu1 from LIAFA, Paris
Keywords
parametric verification, protocol, timedmodel-checking
Authors
MATOUŠEK, P.
RIV year
2004
Released
23. 11. 2004
ISBN
0948-6968
Periodical
Journal of Universal Computer Science
Year of study
10
Number
10
State
Republic of Austria
Pages from
1469
Pages to
1495
Pages count
26
URL
BibTex
@article{BUT45735,
author="Petr {Matoušek}",
title="Tools for Parametric Verification. A Comparison on a Case Study",
journal="Journal of Universal Computer Science",
year="2004",
volume="10",
number="10",
pages="1469--1495",
issn="0948-6968",
url="https://www.fit.vut.cz/research/publication/7629/"
}