Applying formal methods to causal multicast

This thesis provides a layered proof of an algorithm based on the ISIS system that provides causal group multicast. We also examine the role of specification and give some specifications for differing multicast services. We start our verification by showing the sliding window protocol in both unbounded and bounded sequence number versions, when built upon a lossy FIFO link, provides a service which is equivalent to a lossless FIFO link. We prove this by showing both safety and liveness properties for both version. We then build a simple multicast with destination sets on top of a collection of lossless FIFO link, but also introduce process crashes. We describe the effect of crashes on delivery expectations and verify that a simple multicast algorithm provides this service. Finally we show that a causal multicast algorithm based on the simple multicast, performs the task of causal, peer group multicast with delivery atomicity. This specification also illustrates the effect that crashes and crash detection mechanisms have on such a service. All our models are presented using the I/O Automaton and we use variants of the common proof techniques used with the I/O automaton