Deadlock avoidance policies for automated manufacturing cells

This paper suggests a framework for developing provably correct and scalable avoidance policies for the automated manufacturing cell (AMC) model. We provide a formal description of the AMC operation and establish its correspondence to a finite state automaton (FSA). The AMC model´s deadlock characteristics are studied with the aid of the FSA state transition diagram. We provide a new characterization of AMC state safety which serves as the basis of a new framework for systematic development of avoidance policies. We provide two examples of the framework functionality. First, the framework is used to formally prove the correctness of the resource upstream neighborhood (RUN) avoidance policy (Gaarder, 1993). Then, it is used to provide an alternative proof for the correctness of B-K deadlock avoidance algorithm (BKDAA) (Banaszak et al., 1990). Furthermore, an interesting relationship existing between RUN and BKDAA policies is brought out. Finally, the results are summarized, conclusions drawn, and possible extensions and generalizations of the underlying ideas discussed