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 conferencePaper

Abstract

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

Conference

Conference23rd Asia-Pacific Software Engineering Conference
CountryNew Zealand
CityHamilton
Period6/12/169/12/16

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

  • Cite this

    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.