Formalization and Verification of the Powerlink Protocol Using CSP

摘要

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