BANASZAK Z A，KROGH B H. Deadlock avoidance in flexible manufacturing systems with concurrently competing process flows[J]. IEEE Transactions on Robotics and Automation,1990,6（6）：724-734.
[2]
ABDALLAH I B，EIMARAGHY H. Deadlock prevention and avoidance in FMS:a Petri net-based approach[J]. International Journal of Advanced Manufacturing Technology, 1998，16（1）： 1793-1798.
[3]
WU Naiqi，ZHOU Mengchu. Avoiding deadlock and reducing starvation and blocking in automated manufacturing systems[J]. IEEE Transactions on Robotics and Automation, 2001，17（5）：658-669.
[4]
VISWANADHAM N，NARAHARI Y，JOHNSON T L. Deadlock prevention and deadlock avoidance in flexible manufacturing systems using Petri net models[J]. IEEE Transactions on Robotics and Automation, 1990，6（6）： 713-723.
[5]
HOARE C A R. Communicating sequential processes[M]. Prentice-Hall, 1985.
[6]
HOLZMANN G J. The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997，23（5）：279-295.
[7]
HAVELUND K，LOWRY M，PENIX J. Formal analysis of a space-craft controller using SPIN[J]. IEEE Transactions on Software Engineering, 2001，27（8）：749 -765.
[8]
MORTEL-FRONCZAK van de J M ，ROODA J E. A case study in the design of control systems for flexible production cells[A]. KOPACEK P, Proceedings of MIM97[C].1997.243-248.
[9]
MORTEL-FRONCZAK J M van de，ROODA J E，NIEUWELAAR van den N J M. Specification of a flexible manufacturing system using concurrent programming[J]. The International Journal of Concurrent Engineering: Research & Applications, 1995，3（3）：187-194.
[10]
BOS V，KLEIJN J J T. Automatic verification of a manufacturing system[J]. Robotics and Computer Integrated Manufacturing, 2001, 17(3):185-198.
