Publication Details

Protocol Proving and Model-Checking: A First-Look Experience

MATOUŠEK Petr, RÁB Jaroslav and VÝŠEK Pavel. Protocol Proving and Model Checking: A First-Look Experience. In: IEEE ECBS - Joint Workshop on Formal Specifications of Computer-Based Systems. Edinburgh: unknown, 2000, pp. 71-75. ISBN 1-85-769121-0.
Type
conference paper
Language
english
Authors
Matoušek Petr, Ing. (DCSE FEECS BUT)
Ráb Jaroslav, Ing. (DCSE FEECS BUT)
Výšek Pavel, Ing. (FEECS BUT)
URL
Keywords

protocol, verification, model checking, formal methods

Annotation

This paper presents a comparative study of practical experience applying current tools on protocol verification. The goal of the study is to inform about different verification tools and their practical usage. Our test is focused on Spin - a popular model checker; futhermore on theorem prover systems - PVS and Isabelle. Model checking and theorem proving introduce two different verification approaches. The paper brings practical experience with installation and utilization of these systems for protocol verification. The comparative study is demonstrated on a simplified communication protocol that is formally specified and its features are checked by the verification system. The first part of the paper describes verification system used, and lessons learned during downloading, installation, and execution. The second part of the document introduces a case study applied on those three tested systems. A simplified model of LDAP protocol is selected for this task. The last part compares the results achieved.

Published
2000
Pages
71-75
Proceedings
IEEE ECBS - Joint Workshop on Formal Specifications of Computer-Based Systems
Conference
7th IEEE International Conference and Workshop ECBS'2000, Napier University, Edinburgh, Scotland, GB
ISBN
1-85-769121-0
Place
Edinburgh, GB
BibTeX 
@INPROCEEDINGS{FITPUB6140,
   author = "Petr Matou\v{s}ek and Jaroslav R\'{a}b and Pavel V\'{y}\v{s}ek",
   title = "Protocol Proving and Model-Checking: A First-Look Experience",
   pages = "71--75",
   booktitle = "IEEE ECBS - Joint Workshop on Formal Specifications of Computer-Based Systems",
   year = 2000,
   location = "Edinburgh, GB",
   ISBN = "1-85-769121-0",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/6140"
}
Back to top