Algebraic specification and verification of communication protocols (Q2265806)

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 behaviour of switching nodes. Starting from a specification of the communication behaviour 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 behaviour 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. With these, it is proved that the behaviour of a network of switching nodes is observation equivalent to a single switching node, which proves the consistency of the specification of the communication behaviour of the network as a whole and the combined behaviour of its constituents, the switching nodes.