Title
Formalization and Verification of the Powerlink Protocol Using CSP.
Abstract
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.
Year
DOI
Venue
2016
10.1109/APSEC.2016.11
Asia-Pacific Software Engineering Conference
Keywords
Field
DocType
Powerlink Protocol,Modelling,Simulation,Analysis,Verification
Data modeling,Model checking,Computer science,Scheduling (computing),Communicating sequential processes,Deadlock,Automation,Real-time computing,Ethernet,Ethernet Powerlink,Distributed computing,Embedded system
Conference
ISSN
Citations 
PageRank 
1530-1362
0
0.34
References 
Authors
0
6
Name
Order
Citations
PageRank
Haiping Pang100.68
Ju Li200.34
Yijia Ruan300.34
Yanhong Huang44910.56
Jianqi Shi55712.50
Shengchao Qin671162.81