Publication Details

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.
Czech title
Dokazování protokolů pomocí PVS: případová studie
Type
conference paper
Language
English
Authors
Matoušek Petr, doc. Ing., Ph.D., M.A. (DIFS)
URL
Keywords

formal verification, PVS, communication protocol

Abstract

Prototype Verification System (PVS) is a popular verification tool forwriting formal specification and checking formal proofs. It consists ofa specification language integrated with support tools and a theoremprover. This paper shows its application on the class of high-levelcommunication protocols. Case study is demonstrated on a simpleprotocol for user database access. The paper discusses problems offormal specification of communication protocols, its representationusing PVS language and a set of properties to be proved.

Published
2001
Pages
67–73
Proceedings
Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01
Conference
35th Spring International Conference Modelling and Simulation of Systems (MOSIS 2001), Hradec nad Moravicí, CZ
ISBN
80-85988-57-7
Place
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"
}
Back to top