Publication Details

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, 2001, pp. 67-73. ISBN 80-85988-57-7. Available from: http://www.fee.vutbr.cz/~matousp/doc/2001/mosis01.html
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 FIT BUT)
URL
Keywords

formal verification, PVS, communication protocol

Abstract

Prototype Verification System (PVS) is a popular verification tool for writing formal specification and checking formal proofs. It consists of a specification language integrated with support tools and a theorem prover. This paper shows its application on the class of high-level communication protocols. Case study is demonstrated on a simple protocol for user database access. The paper discusses problems of formal specification of communication protocols, its representation using 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, 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"
}
Back to top