@inproceedings{558e58a3f76f49308974af2d3bdc5ee3,
title = "Finite-state analysis of the CAN bus protocol",
abstract = "We formally specify the data link layer of the Controller Area Network (CAN), a high-speed serial bus system with real-time capabilities, widely used in embedded systems. CAN's primary application domain is automotive, and the physical and data link layers of the CAN architecture were the subject of the ISO 11898 international standard. We checked our specification against 12 important properties of CAN, eight of which are gleaned from the ISO standard; the other four are desirable properties not directly mentioned in the standard. Our results indicate that not all properties can be expected to hold of a CAN implementation and we discuss the implications of these findings. Moreover, we have conducted a number of experiments aimed at determining how the size of the protocol's state space is affected by the introduction of various features of the data link layer, the number of nodes in the network the number of distinct message types, and other parameters.",
keywords = "Application software, Automotive engineering, Computer science, Control systems, Embedded system, Error correction, ISO standards, Manufacturing, Protocols, State-space methods",
author = "\{Van Osch\}, Michiel and Smolka, \{Scott A.\}",
note = "Publisher Copyright: {\textcopyright} 2001 IEEE.; 6th IEEE International Symposium on High Assurance Systems Engineering, HASE 2001 ; Conference date: 22-10-2001 Through 24-10-2001",
year = "2001",
doi = "10.1109/HASE.2001.966806",
language = "English",
series = "Proceedings of IEEE International Symposium on High Assurance Systems Engineering",
publisher = "IEEE Computer Society",
pages = "42--52",
booktitle = "6th IEEE International Symposium on High Assurance Systems Engineering - Special Topic",
}