Abstract This paper defines a new denotational semantics for the language of Communicating Sequential Processes (CSP). The semantics lies between the existing traces and failures models of CSP, providing a treatment of non-determinism in terms of singleton failures . Although the semantics does not represent a congruence upon the full language, it is adequate for sequential tests of non-deterministic processes. This semantics corresponds exactly to a commonly used notion of data refinement in Z and Object-Z: an abstract data type is refined when the corresponding process is refined in terms of singleton failures. The semantics is used to explore the relationship between data refinement and process refinement, and to derive a rule for data refinement that is both sound and complete.

The reverse path forwarding algorithm is a protocol for distributing messages throughout networks. The intention is to preserve correctness - messages sent will eventually be received by all nodes in the originator's connected component - whilst minimising the number of propagations of each message. We use a variety of analysis techniques to identify necessary additional constraints, and to prove correctness under these conditions. In particular we present counter examples found by the model-checkers FDR and the Alloy Analyzer, illustrating that the protocol is incorrect if the cost of links is dependent upon the node using that link. We then consider the case where the cost of links is independent of the node using that link; we use a special-purpose network sampling program to increase confidence in the correctness of this stricter protocol, and then perform a hand-proof to verify correctness. We conclude with a discussion of the suitability of these techniques for reasoning about protocols of this complexity.