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.

English Title

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

Type

conference paper

Language

en

Original Abstract

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.

English abstract

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.

Keywords

protocol, parametric verification, timed system, tools

RIV year

2004

Released

28.05.2004

Publisher

University of Stirling

Location

Stirling

ISBN

1-85769-197-0

Book

Proceedings of the 5th Joint Workshop on FSCBS

Pages from

45

Pages to

55

Pages count

10

URL

Documents

BibTex


@inproceedings{BUT17127,
  author="Petr {Matoušek}",
  title="Tools for Parametric Verification: A Comparison on a Case Study.",
  annote="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. 
", address="University of Stirling", booktitle="Proceedings of the 5th Joint Workshop on FSCBS", chapter="17127", institution="University of Stirling", year="2004", month="may", pages="45--55", publisher="University of Stirling", type="conference paper" }