ALGEBRAIC SPECIFICATION AND VERIFICATION OF COMMUNICATION PROTOCOLS

Assume a communication network, consisting of switching nodes which make connections (like telephone exchanges) and terminal nodes which use these connections (like subscribers, computer terminals, etc. ). The terminal nodes are at the periphery of the network, whereas switching nodes are internal to the network. In this paper it is shown how Milner's calculus of communicating systems (CCS) can be applied to specify and verify the communication behavior of switching nodes. Starting from a specification of the communication behavior of terminal nodes, a specification for the protocol between terminal nodes and the network of switching nodes is systematically derived. In a similar way the communication behavior of switching nodes inside the network is derived. Verification is based on a formal abstraction mechanism which shows the equivalence of a specification and the corresponding design. The expansion theorem of CCS, together with certain laws from CCS, provide such a mechanism.