Detail publikace

Tools for Parametric Verification. A Comparison on A Case Study (extended abstract).

MATOUŠEK, P. Tools for Parametric Verification. A Comparison on A Case Study (extended abstract). Proceedings of the 5th Joint Workshop on FSCBS. Stirling: University of Stirling, 2004. p. 45-55. ISBN: 1-85769-197-0.
Název česky
Nástroje pro parametrickou verifikaci: srovnávací studie.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Matoušek Petr, doc. Ing., Ph.D., M.A. (UIFS)
URL
Klíčová slova

protocol, parametric verification, timed system, tools

Abstrakt

Při analýze komunikačních protokolů využíváme při specifikaci modeluparametry, např. zpoždění přenosu, délka odesílacího okna apod.Verifikace modelu s parametry je semi-rozhodnutelný problém , kterýzávisí na počtu hodin, parametrů a čítačů v modulu. Kombinací různýchverifikačních nástrojů pro časované modely (HyTech, TReX, Uppaal),můžeme zjistit, pro jaké parametry jsou definované vlastnosti protokolusplněné (tzn. syntéza parametrů). Tento článek popisuje syntézuparametrů protokolu PGM (RFC 3208). Nejprve vytvoříme formální modelprotokolu postavený na rozšířených časovaných automatech s parametry apak verifikujeme vlastnosti typu bezpečnost. Výsledky získanéautomatickou verifikací odpovídají ručně vypočítaným vztahům. Tentočlánek popisuje naše zkušenosti s parametrickou verifikacímulticastového protokolu PGM. Dosažené výsledky byly vytvořeny vespolupráci s Mihaelou Sighireanu z institutu LIAFA v Paříži.

Rok
2004
Strany
45–55
Sborník
Proceedings of the 5th Joint Workshop on FSCBS
ISBN
1-85769-197-0
Vydavatel
University of Stirling
Místo
Stirling
BibTeX 
@inproceedings{BUT17127,
  author="Petr {Matoušek}",
  title="Tools for Parametric Verification. A Comparison on A Case Study (extended abstract).",
  booktitle="Proceedings of the 5th Joint Workshop on FSCBS",
  year="2004",
  pages="45--55",
  publisher="University of Stirling",
  address="Stirling",
  isbn="1-85769-197-0",
  url="http://www.fit.vutbr.cz/~matousp/doc/2004/fscbs04.pdf"
}
Nahoru