Conference paper

 
Matoušek, P.: Protocol Proving Using PVS: A Case Study, In: Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01, Hradec n/M, CZ, MARQ, 2001, p. 67-73, ISBN 80-85988-57-7
Publication language:english
Original title:Protocol Proving Using PVS: A Case Study
Title (cs):Dokazování protokolů pomocí PVS: případová studie
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)
Place:Hradec n/M, CZ
Year:2001
URL:http://www.fee.vutbr.cz/~matousp/doc/2001/mosis01.html
ISBN:80-85988-57-7
Publisher:
URL:http://www.fit.vutbr.cz/~matousp/doc/2001/mosis01.html [HTML]
URL:http://www.fit.vutbr.cz/~matousp/doc/2001/mosis01.ps [PS]
Keywords
formal verification, PVS, communication protocol
Annotation
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.
BibTeX:
@INPROCEEDINGS{
   author = {Petr Matouš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},
   publisher = {},
   ISBN = {80-85988-57-7},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=6143}
}