Reasoning about asynchronous behaviour in distributed systems

When a new component is added to an existing, distributed system, it has to co-operate with existing components in a way that doesn't interfere badly with the original system. Adding new components to an existing system is simplified if their communication is asynchronous. It allows for looser coupling. Unfortunately, the fact that the communication between components is asynchronous adds to the difficulty of reasoning about their behaviour. This paper gives an illustrative example of a simple distributed system with asynchronous behaviour and discusses how its behaviour can be described and reasoned about in terms of goals. This formalises what we believe to be contemporary engineering practice. Experimental support for reasoning, including animation, is particularly appropriate and practical in these circumstances, because the properties which we must reason about are emergent rather than compositional.