Publication Details

Tools for Parametric Verification. A Comparison on a Case Study

MATOUŠEK Petr. Tools for Parametric Verification. A Comparison on a Case Study. Journal of Universal Computer Science, vol. 10, no. 10, 2004, pp. 1469-1495. ISSN 0948-6968.
Czech title
Nástroje pro parametrickou verifikaci: srovnávací studie.
Type
journal article
Language
english
Authors
Matoušek Petr, doc. Ing., Ph.D., M.A. (DIFS FIT BUT)
URL
Keywords

parametric verification, protocol, timed model-checking

Abstract

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 HyTech, TReX and UPPaal we are able to find relation between parameters satisfying desired property. The paper gives a report 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 Sighireanu1 from LIAFA, Paris

Published
2004
Pages
1469-1495
Journal
Journal of Universal Computer Science, vol. 10, no. 10, ISSN 0948-6968
Publisher
Springer Verlag
BibTeX 
@ARTICLE{FITPUB7629,
   author = "Petr Matou\v{s}ek",
   title = "Tools for Parametric Verification. A Comparison on a Case Study",
   pages = "1469--1495",
   journal = "Journal of Universal Computer Science",
   volume = 10,
   number = 10,
   year = 2004,
   ISSN = "0948-6968",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7629"
}
Back to top