DocumentCode
1146899
Title
A Theory for Protocol Validation
Author
Holzmann, Gerard J.
Author_Institution
Department of Electrical Engineering, Delft University of Technology
Issue
8
fYear
1982
Firstpage
730
Lastpage
738
Abstract
This paper introduces a simple algebra for the validation of communication protocols in message passing systems. The behavior of each process participating in a communication is first modeled in a finite state machine. The symbol sequences that can be accepted by these machines are then expressed in "protocol expressions," which are defined as regular expressions extended with two new operators: division and multiplication. The interactions of the machines can be analyzed by combining protocol expressions via multiplication and algebraically manipulating the terms.
Keywords
Deadlock detection; distributed systems; message passing; protocol analysis; regular expressions; validation algebra; verification; Algebra; Automata; Central Processing Unit; Computer networks; Distributed computing; Message passing; Performance analysis; Protocols; Space exploration; State-space methods; Deadlock detection; distributed systems; message passing; protocol analysis; regular expressions; validation algebra; verification;
fLanguage
English
Journal_Title
Computers, IEEE Transactions on
Publisher
ieee
ISSN
0018-9340
Type
jour
DOI
10.1109/TC.1982.1676079
Filename
1676079
Link To Document