Deadlock prevention in flexible manufacturing systems using symbolic model checking

This paper illustrates the use of symbolic model checking in the design of deadlock-free flexible manufacturing systems. Our verification methodology consists of the following stages. First, we extract a state machine model of the system. Second, we write the system specifications using a propositional temporal logic. Finally we use the model checker to check the state machine of the system against its requirements. When a deadlock is identified, a counterexample is automatically generated with a scenario that leads to the deadlock. The counterexample is used to design the proper operational policy that will prevent the corresponding deadlock. This verification approach allows an exhaustive search of all possible behaviors and scenarios. We designed a flexible manufacturing system capable of producing 3 types of parts with 4 machines and 3 robots. It took 8 seconds to find possible deadlocks assuming machine processing capacity of one part at a time and about 36 seconds when we increased the machine processing capacity to two parts at a time. The size of the state space was in the order of 10¹⁸ states