Protocol Proving Using PVS: A Case Study
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F01%3APU28657" target="_blank" >RIV/00216305:26230/01:PU28657 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Protocol Proving Using PVS: A Case Study
Original language description
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 setof properties to be proved.
Czech name
Dokazování protokolů pomocí PVS: případová studie
Czech description
Systém PVS (Prototype Verification System) je populární verifikační nástroj pro psaní formální specifikace a kontrolu formálních důkazů. PVS tvoří nejen vlastní theorem prover a specifikačním jazykem, ale i další nástroje. Tento článek ukazuje použití PVS při verifikace komunikačních protokolů vyšší úrovně. Studie ukazuje jednoduchý protokol pro přístup do databáze. Ve studii ukazujeme problémy formální specifikace komunikačních protokolů, reprezentace modelu jazykem PVS a množinu dokazovaných vlastnosttí.<br>
Classification
Type
D - Article in proceedings
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
—
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2001
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01
ISBN
80-85988-57-7
ISSN
—
e-ISSN
—
Number of pages
7
Pages from-to
67-73
Publisher name
NEUVEDEN
Place of publication
Hradec n/M
Event location
Hradec nad Moravicí
Event date
May 9, 2001
Type of event by nationality
EUR - Evropská akce
UT code for WoS article
—