The author has used Milner’s Calculus of Communicating Systems (CCS) [1] to specify and verify the behavior of switching nodes in a telephone network. Starting from a behavior of the terminal nodes (source and destination) of a network, and the view of the rest of the network provided to each terminal node, the author has systematically derived a specification of the protocol between the two nodes. The powerful expansion theorem and the reduction laws of CCS are used to prove that a network of switching nodes may be regarded as a single node.

The paper presents a good design method for designers of distributed systems. The combination algorithm which is used to derive the total behavior of the network (from its individual behavior to the source and destination nodes) is an original contribution of the author. Being primarily a design application of CCS to a real life situation, the paper contains a bewildering array of equations which may seem forbidding to a lay reader, but by a judicious use of finite-state diagrams the equations become comprehensible. Section 3 and Appendix A contain the necessary theory needed for understanding the rest of the paper.

However, the author does not mention that initial efforts at specifying telephone networks were made by Shields [2] and Milner [1] himself, though they did not come close to specifying such a protocol.