Title :
A Theory for Protocol Validation
Author :
Holzmann, Gerard J.
Author_Institution :
Department of Electrical Engineering, Delft University of Technology
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;
Journal_Title :
Computers, IEEE Transactions on
DOI :
10.1109/TC.1982.1676079
