On the Application of Formal Methods for Specifying and Verifying Distributed Protocols

Author

Gelastou, Marina ; Georgiou, Chryssis ; Philippou, Anna

Author_Institution

Dept. of Comput. Sci., Univ. of Cyprus, Nicosia

fYear

2008

fDate

10-12 July 2008

Firstpage

195

Lastpage

204

Abstract

In this paper we consider the frameworks of Process Algebra and I/O Automata and we apply both towards the verification of a distributed leader-election protocol. Based on the two experiences we evaluate the approaches and draw initial conclusions with respect to their relative capabilities, strengths and usability.To the best of our knowledge, this is the first hands-on evaluation of the two models, and we view it as the cornerstone for a wider investigation of the strengths and weaknesses of the two methodologies in specifying and verifying (distributed) protocols.

Keywords

automata theory; distributed processing; formal specification; formal verification; process algebra; distributed leader-election protocol specification; distributed leader-election protocol verification; formal method; input-output automata; process algebra; Algebra; Application software; Automata; Computer applications; Computer networks; Computer science; Distributed computing; Nominations and elections; Protocols; Usability; Applicability; Distributed Protocols; Formal Methods; I/O Automata; Process Algebra; Usability;

fLanguage

English

Publisher

ieee

Conference_Titel

Network Computing and Applications, 2008. NCA '08. Seventh IEEE International Symposium on

Conference_Location

Cambridge, MA

Print_ISBN

978-0-7695-3192-2

Electronic_ISBN

978-0-7695-3192-2

Type

conf

DOI

10.1109/NCA.2008.24

Filename

4579656