［1］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.