Data flow analysis of communicating finite state machines

Abstract

Let ( F'l, Pz, . . . . Pm) be a network of n finite state machines, communicating with each other asynchronously using typed messages over unbounded FIFO channels, In this paper we present a data flow approach to analyzing these communicating machines for nonprogress properties (deadlock and unspecified reception). We set up flow equations to compute the set of pending messages in the queues at any given state of such a network, The central technical contribution of this paper is an algorithm to compute approximations to solutions for the ensuing equations We then show how these approximate solutions can be used to check that interactions between the processes are free of nonprogress errors. We conclude with a number of example protocols that our algorithm certifies to be free of nonprog-ess errors. Included in the examples is a specification of X25 call establishment/clear protocol,