Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 10 / Issue 10

available in:   PDF (253 kB) PS (237 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-010-10-1469


Tools for Parametric Verification. A Comparison on a Case Study

Petr Matoušek (Brno University of Technology, Czech Republic)

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 Sighireanu (Mihaela.Sighireanu@liafa.jussieu.fr) from LIAFA, Paris.

Keywords: parametric verification, protocol, timed model-checking

Categories: C.2.2, F.4.3, I.6.3