Abstract: Good formal design of control architecture for distributed manufacturing scheduling is the basis to the consistency and efficiency of the next developed system.This paper studies the formal specification problem of Agent or Holon-based control architecture for manufacturing scheduling.Based on the comparisons of existing formal specification methods，this paper proposes a first-order polyadic π-calculus based formal design and analysis method.Then，a case of Holon-based control architecture for manufacturing scheduling in flexible shop floor is investigated.Especially，its communication and negotiation mechanism is modeled with first-order polyadic π-calculus and its deadlock is analyzed correspondingly.The results show that the first-order polyadic π-calculus is an easier and effective way for formal specification of Agent or Holon-based control architecture for distributed manufacturing scheduling.

Key words: distributed manufacturing scheduling, control architecture, formal specification, first-order polyadic π-calculus, Agent, Holon

摘要： 分布式制造调度控制体系结构的良好形式化设计是确保后续开发系统一致性和高效性的基础。以Agent（Holon）的制造调度控制体系结构模型为对象，在比较现有形式化方法优劣的基础上，提出基于一阶多元π-演算的体系结构形式化建模和分析方法，并以一种基于Holon的柔性制造车间生产调度控制体系结构为实例，重点对各个实体的通信协调机制进行了形式化分析，并借助计算机工具进行了相应的死锁分析。结果表明了基于一阶多元π-演算在形式化建模和分析方面的有效性。

关键词: 分布式制造调度, 控制体系结构, 形式化规范, 一阶多元π-演算, Agent, Holon