Detail publikačního výsledku

Protocol Proving Using PVS: A Case Study

MATOUŠEK, P.

Originální název

Protocol Proving Using PVS: A Case Study

Anglický název

Protocol Proving Using PVS: A Case Study

Druh

Stať ve sborníku mimo WoS a Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

formal verification, PVS, communication protocol

Klíčová slova v angličtině

formal verification, PVS, communication protocol

Autoři

MATOUŠEK, P.

Rok RIV

2011

Vydáno

01.01.2001

Nakladatel

Marq software s.r.o.

Místo

Hradec n/M

ISBN

80-85988-57-7

Kniha

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

Strany od

67

Strany do

73

Strany počet

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"
}