Issue No. 08 - August (1982 vol. 31)
G.J. Holzmann , Department of Electrical Engineering, Delft University of Technology
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.
verification, Deadlock detection, distributed systems, message passing, protocol analysis, regular expressions, validation algebra
G.J. Holzmann, "A Theory for Protocol Validation", IEEE Transactions on Computers, vol. 31, no. , pp. 730-738, August 1982, doi:10.1109/TC.1982.1676079