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.
|Publication status||Published - 6 Dec 2016|
|Event||23rd Asia-Pacific Software Engineering Conference - Hamilton, New Zealand|
Duration: 6 Dec 2016 → 9 Dec 2016
|Conference||23rd Asia-Pacific Software Engineering Conference|
|Period||6/12/16 → 9/12/16|
Pang, H., Li, J., Ruan, Y., Huang, Y., Shi, J., & Qin, S. (2016). Formalization and Verification of the Powerlink Protocol using CSP. Paper presented at 23rd Asia-Pacific Software Engineering Conference, Hamilton, New Zealand.