Formalization and Verification of the Powerlink Protocol using CSP

Happing Pang, Ju Li, Yijia Ruan, Yanhong Huang, Jianqi Shi, Shengchao Qin

Research output: Contribution to conferencePaperpeer-review


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.
Original languageEnglish
Publication statusPublished - 6 Dec 2016
Event23rd Asia-Pacific Software Engineering Conference - Hamilton, New Zealand
Duration: 6 Dec 20169 Dec 2016


Conference23rd Asia-Pacific Software Engineering Conference
Country/TerritoryNew Zealand


Dive into the research topics of 'Formalization and Verification of the Powerlink Protocol using CSP'. Together they form a unique fingerprint.

Cite this