Detail publikace

Protocol Proving Using PVS: A Case Study

MATOUŠEK Petr. Protocol Proving Using PVS: A Case Study. In: Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01. Hradec n/M: MARQ, 2001, s. 67-73. ISBN 80-85988-57-7. Dostupné z: http://www.fee.vutbr.cz/~matousp/doc/2001/mosis01.html
Název česky
Dokazování protokolů pomocí PVS: případová studie
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Matoušek Petr, doc. Ing., Ph.D., M.A. (UIFS FIT VUT)
URL
Abstrakt

Systém PVS (Prototype Verification System) je populární verifikační nástroj pro psaní formální specifikace a kontrolu formálních důkazů. PVS tvoří nejen vlastní theorem prover a specifikačním jazykem, ale i další nástroje. Tento článek ukazuje použití PVS při verifikace komunikačních protokolů vyšší úrovně. Studie ukazuje jednoduchý protokol pro přístup do databáze. Ve studii ukazujeme problémy formální specifikace komunikačních protokolů, reprezentace modelu jazykem PVS a množinu dokazovaných vlastností.

Rok
2001
Strany
67-73
Sborník
Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01
Konference
35th Spring International Conference Modelling and Simulation of Systems (MOSIS 2001), Hradec nad Moravicí, CZ
ISBN
80-85988-57-7
Vydavatel
MARQ
Místo
Hradec n/M, CZ
BibTeX 
@INPROCEEDINGS{FITPUB6143,
   author = "Petr Matou\v{s}ek",
   title = "Protocol Proving Using PVS: A Case Study",
   pages = "67--73",
   booktitle = "Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01",
   year = 2001,
   location = "Hradec n/M, CZ",
   ISBN = "80-85988-57-7",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/6143"
}
Nahoru