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

journal article - other

Language

en

Original 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

English 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

Keywords

parametric verification, protocol, timed model-checking

RIV year

2004

Released

23.11.2004

ISBN

0948-6968

Periodical

Journal of Universal Computer Science

Year of study

10

Number

10

State

AT

Pages from

1469

Pages to

1495

Pages count

26

URL

Documents

BibTex


@article{BUT45735,
  author="Petr {Matoušek}",
  title="Tools for Parametric Verification. A Comparison on a Case Study",
  annote="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",
  chapter="45735",
  journal="Journal of Universal Computer Science",
  number="10",
  volume="10",
  year="2004",
  month="november",
  pages="1469--1495",
  type="journal article - other"
}