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 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.

Recommendations

Cited in

(16)

This page was built for publication: Algebraic specification and verification of communication protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2265806)