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

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