Publication result detail

Protocol Proving Using PVS: A Case Study

MATOUŠEK, P.

Original Title

Protocol Proving Using PVS: A Case Study

English Title

Protocol Proving Using PVS: A Case Study

Type

Paper in proceedings outside WoS and Scopus

Original 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.

English 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.

Keywords

formal verification, PVS, communication protocol

Key words in English

formal verification, PVS, communication protocol

Authors

MATOUŠEK, P.

RIV year

2011

Released

01.01.2001

Publisher

Marq software s.r.o.

Location

Hradec n/M

ISBN

80-85988-57-7

Book

Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01

Pages from

67

Pages to

73

Pages count

7

URL

http://www.fee.vutbr.cz/~matousp/doc/2001/mosis01.html

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",
  publisher="Marq software s.r.o.",
  address="Hradec n/M",
  isbn="80-85988-57-7",
  url="http://www.fee.vutbr.cz/~matousp/doc/2001/mosis01.html"
}