Deadlock Analysis in Networks of Communicating Processes

We use the failures model of Communicating Sequential Processes to describe the behaviour of a simple class of networks of communicating processes. This model is well suited to reasoning about the deadlock behaviour of processes, and we demonstrate this fact by proving some results which help in the analysis of deadlock in networks. In particular, we formulate some simple theorems which characterise the states in which deadlock can occur, and use them to prove some theorems on the absence of global deadlock in certain classes of systems. Some examples are given to show the utility of these results.