Abstract: Modeling and analysis can help improve the safety of industrial control protocol. This paper summarizes the communicating behaviors of Powerlink and proposes a new modeling method by the modeling language CSP（Communication Sequential Process）. This method simulates the random generation of asynchronous request and the error handling mechanism of losing-frame error. Finally, this paper analyzes the scheduling priority of the requests in PAT（Process Analysis Toolkit）. The results of the experiment show the proposed method can accurately describe the scheduling process in the protocol, which will help the further research of the mechanism of Powerlink.

Key words: Powerlink, Communication Sequential Process（CSP）, modeling, verification, Process Analysis Toolkit（PAT）

摘要： 针对通信协议进行形式化建模与分析，能够很大程度上提高工控协议的安全性。通过分析开源实时以太网Powerlink的同步、异步阶段的不同通信行为，以及在同步阶段的不同通信模式，提出一种利用CSP（Communication Sequential Process）语言对Powerlink协议进行形式化建模的方法。使用该方法能够描述Powerlink在数据链路层上不同节点之间的通信行为，以及描述在随机产生异步请求的情况下，异步阶段的异步请求调度行为。同时，该方法也准确模拟了协议运行过程中，错误处理机制对丢失帧情况的处理过程。最后利用软件PAT（Process Analysis Toolkit）验证了这些异步调度过程是否满足优先级顺序等性质，有助于对协议的运行机制进行深入分析。

关键词: Powerlink, 通信顺序进程（CSP）, 建模, 验证, 流程分析工具箱（PAT）