Visualisation of reduced abstracted behaviour as a design tool

Presents a user-friendly formal method for obtaining comprehensive feedback from the behaviour of a design of a distributed system. The method consists of abstracting and reducing the behaviour and showing the result in a graphical form on a computer screen. Deadlocks, livelocks, incorrect actions and many other kinds of design errors can often be easily discovered from the graphical representation. The method differs from animation, simulation and testing in that it analyses all possible behaviours simultaneously. For instance, if the graphical representation does not contain a deadlock, then the system is guaranteed to be free from deadlocks. The method is illustrated by using it in the development of a well-known communication protocol. This article concentrates on the use of the method rather than the underlying theory and computer tools