Detail publikace

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

MATOUŠEK Petr. Tools for Parametric Verification. A Comparison on A Case Study (extended abstract). In: Proceedings of the 5th Joint Workshop on FSCBS. Stirling: University of Stirling, 2004, s. 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
angličtina
Autoři
URL
Abstrakt

Při analýze komunikačních protokolů využíváme při specifikaci modelu parametry, 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ých verifikačních nástrojů pro časované modely (HyTech, TReX, Uppaal), můžeme zjistit, pro jaké parametry jsou definované vlastnosti protokolu splněné (tzn. syntéza parametrů). Tento článek popisuje syntézu parametrů protokolu PGM (RFC 3208). Nejprve vytvoříme formální model protokolu postavený na rozšířených časovaných automatech s parametry a pak 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 ve spoluprá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
Konference
IEEE TC-ECBS and IFIP WG10.1 Joint Workshop on Formal Specifications of Computer-Based Systems, Brno, CZ
ISBN
1-85769-197-0
Vydavatel
University of Stirling
Místo
Stirling, GB
BibTeX
@INPROCEEDINGS{FITPUB7478,
   author = "Petr Matou\v{s}ek",
   title = "Tools for Parametric Verification. A Comparison on A Case Study (extended abstract).",
   pages = "45--55",
   booktitle = "Proceedings of the 5th Joint Workshop on FSCBS",
   year = 2004,
   location = "Stirling, GB",
   publisher = "University of Stirling",
   ISBN = "1-85769-197-0",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7478"
}
Nahoru