This Article 
 Bibliographic References 
 Add to: 
A Theory for Protocol Validation
August 1982 (vol. 31 no. 8)
pp. 730-738
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.
Index 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. 8, pp. 730-738, Aug. 1982, doi:10.1109/TC.1982.1676079
Usage of this product signifies your acceptance of the Terms of Use.