该文利用模型验证(Model-Checking)方法的强大运算能力,这篇文章给出一个新的制造系统的结构化控制器,该控制器利用符合模型验证(Symbolic Model Checking)方法来验证系统行为的正确性.一种名为Petri网的离散事件系统模型被用来描述系统动态行为.系统的资源用库所表示,系统可以执行的任务往往需要一系列的资源被依次分配给它,这一过程用一组库所、变迁依次交替的Petri网来表达,并且这些变迁与系统资源库所交互.结构化控制器希望控制的系统性质,采用时态逻辑描述.作为一个示例,一个符合模型验证工具SMV被用来作为结构化控制器的运算工具.每当系统进入一个新状态,该控制器检测所有可行的变迁,一个变迁被触发,仅当其发生后的系统状态满足期望的时态逻辑公式.一些已有的死锁避免算法被纳入这个结构化控制器框架.这些控制算法被时态逻辑重新表示,并且,模型验证方法使得其运算更为有效.此外,文中还讨论了对于不可靠资源情形下的死锁避免问题.通过一些例子,展示了这个结构化控制器的工作过程.对于一组系统仿真运行的结果,给出了这个控制器的运算性能.