Detail publikace

Protocol Proving Using PVS: A Case Study

MATOUŠEK, P. Protocol Proving Using PVS: A Case Study. Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01. Hradec n/M: 2001. p. 67-73. ISBN: 80-85988-57-7.
Název česky
Dokazování protokolů pomocí PVS: případová 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

formal verification, PVS, communication protocol

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
ISBN
80-85988-57-7
Místo
Hradec n/M
BibTeX 
@inproceedings{BUT5438,
  author="Petr {Matoušek}",
  title="Protocol Proving Using PVS: A Case Study",
  booktitle="Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01",
  year="2001",
  pages="67--73",
  address="Hradec n/M",
  isbn="80-85988-57-7",
  url="http://www.fee.vutbr.cz/~matousp/doc/2001/mosis01.html"
}
Nahoru