Formalization and Verification of the Powerlink Protocol using CSP

As an integral part of the Ethernet standard IEEE 802.3, Ethernet Powerlink protocol is widely used in the automation industry. It is a software-based solution and achieves some real-time capabilities, and satisfies data transmission demand by guaranteeing communication with very high speed and accuracy. In effort to make implementing Powerlink protocol easier, we built a formal Powerlink model via Communicating Sequential Processes (CSP) and implemented it in the model checker Process Analysis Toolkit (PAT). Based on the model, we simulated Managing Node (MN) and Controlled Node (CN) behaviors in a Powerlink cycle. According to the scheduling case given in the official tutorial, we verify and evaluate the algorithm in it and present an improved algorithm. At last, we verify some properties including deadlock about the Powerlink protocol and whether it exists any imperfect problems when it is operating.