MSc dissertation, September 1992, 103pp.
We consider Chang and Maxemchuk's proposal for a reliable protocol over an unreliable broadcast medium. Their description consists of an informal explanation supported by the use of pseudo-code to characterise the operation of the protocol, and to depict communication events within a system of functional and non-functional sites.
The protocol operates between the applications programs and the broadcast network. The protocol guarantees that all the broadcast messages are received at all the operational receivers in a broadcast group, isolating the applications programs from the unreliable characteristics of the communications network.
The language and models of CSP are employed to specify and implement the protocol at an abstract level, and to establish a proof of correctness. The refinement of the CSP process algebra implementation into the programming language Occam2 is documented.