W. Peng and S. Purushothaman

Data Flow Analysis of Communicating Finite State Machines

in ACM Transactions on Programming Languages and Systems

Abstract:

Let (P1, P2, ..., Pn) 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 specified reception). We set up flow equations to compute the set of pending messages in the queue 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 progress errors. We conclude with a number of example protocols that our algorithm certifies to be free of nonprogress errors. Included in the examples is a specification of X25 call establishment/clear protocol.

Please contact the author for a copy of the paper.