Detail publikačního výsledku

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

Peer-reviewed article not indexed in WoS or Scopus

Original Abstract

Protocol analysis involves several parameters inmodel specification, for instance, transmission delay or the length ofthe transmitting window. Verification of the model with parameters isa semi-decision process that depends on the number of clocks,parameters and counters in the model. Using combination of differentverification tools for timed models as HyTech, TReX and UPPaal we areable to find relation between parameters satisfying desiredproperty. The paper gives a report on the synthesis of parameters ofPGM protocol. We built a formal model based on extended time automatawith parameters and verified the reliability property. Our resultsautomatically obtained from the model are consistent with previousresults derived manually. The paper describes our experience withparametric verification of multicast protocol PGM. Results mentionedin the work were made with collaboration with MihaelaSighireanu1 from LIAFA, Paris

English abstract

Protocol analysis involves several parameters inmodel specification, for instance, transmission delay or the length ofthe transmitting window. Verification of the model with parameters isa semi-decision process that depends on the number of clocks,parameters and counters in the model. Using combination of differentverification tools for timed models as HyTech, TReX and UPPaal we areable to find relation between parameters satisfying desiredproperty. The paper gives a report on the synthesis of parameters ofPGM protocol. We built a formal model based on extended time automatawith parameters and verified the reliability property. Our resultsautomatically obtained from the model are consistent with previousresults derived manually. The paper describes our experience withparametric verification of multicast protocol PGM. Results mentionedin the work were made with collaboration with MihaelaSighireanu1 from LIAFA, Paris

Keywords

parametric verification, protocol, timedmodel-checking

Key words in English

parametric verification, protocol, timedmodel-checking

Authors

MATOUŠEK, P.

RIV year

2011

Released

23.11.2004

ISBN

0948-6968

Periodical

JOURNAL OF UNIVERSAL COMPUTER SCIENCE

Volume

10

Number

10

State

Republic of Austria

Pages from

1469

Pages to

1495

Pages count

26

URL

https://www.fit.vut.cz/research/publication/7629/

Full text in the Digital Library

http://hdl.handle.net/

BibTex

@article{BUT45735,
  author="Petr {Matoušek}",
  title="Tools for Parametric Verification. A Comparison on a Case Study",
  journal="JOURNAL OF UNIVERSAL COMPUTER SCIENCE",
  year="2004",
  volume="10",
  number="10",
  pages="1469--1495",
  issn="0948-695X",
  url="https://www.fit.vut.cz/research/publication/7629/"
}