Deadlock prevention for flexible manufacturing system
Gang XU
Zhiming WU
摘要：Deadlock must be prevented via the shop controller during the flexible manufacturing system (FMS) performing.Various models have been tried for the analysis and design of shop controller. Petri net is suitable to describe the dynamic behavior of the discrete event system, such as concurrency, conflict and deadlock, however, the verification of the system behavior needs structure analysis with complex theoretical proof method. Temporal logic model checking has important advantages over traditional theorem prover. It is fully automatic and can produce possible counter-example which is particularly important in finding subtle error in complex transition systems. In this paper,a new method for the deadlock prevention based on Petri net and Temporal Logic model checking is presented. The specification in the Temporal Logic is expressed according to some result of structure analysis of the Petri net. The model checking is employed to execute the formal verification, which will conduct an exhaustive exploration of all possible behaviors. Finally, an example is presented to demonstrate how the method works.
机标关键词：Temporal Logicmodel checkingstructure analysisflexible manufacturing systemPetri netdiscrete event systemformal verificationdeadlock prevention
分类号：TP3(计算技术、计算机技术)
论文发表日期：2005-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：6( 377-382 )
英文信息