Open AccessModeling and Verification of CAN Bus with Application Layer using UPPAAL
Author(s) -
Can Pan,
Jian Guo,
Longfei Zhu,
Jianqi Shi,
Huibiao Zhu,
Xinyun Zhou
Publication year - 2014
Publication title -
electronic notes in theoretical computer science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.242
H-Index - 60
ISSN - 1571-0661
DOI - 10.1016/j.entcs.2014.12.004
Subject(s) - computer science , can bus , embedded system , bus network , protocol (science) , control bus , model checking , process (computing) , layer (electronics) , application layer , scheduling (production processes) , system bus , formal verification , distributed computing , real time computing , computer network , computer hardware , algorithm , operating system , medicine , chemistry , operations management , alternative medicine , organic chemistry , pathology , software deployment , economics
Controller Area Network (CAN) is a high-speed serial bus system with real-time capability. In this paper, we present a formal model of the CAN bus protocol, mainly focusing on the arbitration process, transmission process, and fault confinement mechanism. Moreover, 11 important properties are formalized in terms of the protocol. Based on the verification tool UPPAAL, we describe the system model and properties for performing verification work of the CAN bus protocol. The verification results indicate that some properties are not satisfied in CAN bus system, most of which are caused by the starvation and bus-off nodes. On this basis, the dynamic priority scheduling algorithm and bus-off recovery mechanism are applied, which indicates that some problems can be solved on the application layer
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom