Conference paper

MATOUŠEK Petr. Tools for Parametric Verification: A Comparison on a Case Study. In: Proceedings of the 5th Joint Workshop on FSCBS. Stirling: University of Stirling, 2004, pp. 45-55. ISBN 1-85769-197-0.
Publication language:english
Original title:Tools for Parametric Verification. A Comparison on A Case Study (extended abstract).
Title (cs):Nástroje pro parametrickou verifikaci: srovnávací studie.
Proceedings:Proceedings of the 5th Joint Workshop on FSCBS
Conference:IEEE TC-ECBS and IFIP WG10.1 Joint Workshop on Formal Specifications of Computer-Based Systems
Place:Stirling, GB
Publisher:University of Stirling
protocol, parametric verification, timed system, tools
Protocol analysis involve several parameters in model specification, for instance, transmission delay or the length of the transmitting window. Verification of the model  with parameters is semi-decision process that depends on number of clocks, parameters and counters in  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 parameters 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.
   author = {Petr Matou{\v{s}}ek},
   title = {Tools for Parametric Verification. A Comparison on A Case
	Study (extended abstract).},
   pages = {45--55},
   booktitle = {Proceedings of the 5th Joint Workshop on FSCBS},
   year = {2004},
   location = {Stirling, GB},
   publisher = {University of Stirling},
   ISBN = {1-85769-197-0},
   language = {english},
   url = {}

Your IPv4 address:
Switch to IPv6 connection

DNSSEC [dnssec]