Dokazování protokolů pomocí PVS: případová studie
Identifikátory výsledku
Kód výsledku v 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>
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Protocol Proving Using PVS: A Case Study
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Protocol Proving Using PVS: A Case Study
Popis výsledku anglicky
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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
JC - Počítačový hardware a software
OECD FORD obor
—
Návaznosti výsledku
Projekt
—
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2001
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Proceedings of the 35th Spring Conference: Modelling and Simulation of Systems - MOSIS'01
ISBN
80-85988-57-7
ISSN
—
e-ISSN
—
Počet stran výsledku
7
Strana od-do
67-73
Název nakladatele
NEUVEDEN
Místo vydání
Hradec n/M
Místo konání akce
Hradec nad Moravicí
Datum konání akce
9. 5. 2001
Typ akce podle státní příslušnosti
EUR - Evropská akce
Kód UT WoS článku
—