@inproceedings{27b0f09510d547388f565100186ce043,
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.",
keywords = "Analysis, Modelling, Powerlink Protocol, Simulation, Verification",
author = "Haiping Pang and Ju Li and Yijia Ruan and Yanhong Huang and Jianqi Shi and Shengchao Qin",
note = "Publisher Copyright: {\textcopyright} 2016 IEEE.; 23rd Asia-Pacific Software Engineering Conference, APSEC 2016 ; Conference date: 06-12-2016 Through 09-12-2016",
year = "2016",
month = jul,
day = "2",
doi = "10.1109/APSEC.2016.052",
language = "英语",
series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",
publisher = "IEEE Computer Society",
pages = "321--328",
editor = "Alex Potanin and Murphy, \{Gail C.\} and Steve Reeves and Jens Dietrich",
booktitle = "Proceedings - 23rd Asia-Pacific Software Engineering Conference, APSEC 2016",
address = "美国",
}