Publication 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

conference paper

Language

en

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

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

Keywords

formal verification, PVS, communication protocol

Released

01.01.2001

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

Documents

BibTex


@inproceedings{BUT5438,
  author="Petr {Matoušek}",
  title="Protocol Proving Using PVS: A Case Study",
  annote="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.",
  booktitle="Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01",
  chapter="5438",
  year="2001",
  month="january",
  pages="67--73",
  type="conference paper"
}