Modeling and Verification of Starvation-Free Bitwise Arbitration Technique for Controller Area Network Using SPIN Promela

Abstract

The Controller Area Network (CAN) is a message based communication service working over high-speed serial bus systems, and mostly used in the automotive industries and real-time communication systems. The CAN bus connects several independent CAN modules and allows them to communicate and work together asynchronously and/or synchronously. All nodes can simultaneously transmit data to the CAN bus, and the collision of multiple messages on the bus is resolved by a bitwise arbitration technique that operates by assigning a node with a low-priority message to switch to a “listening” mode while a node with a high-priority message remains in a “transmitting” mode. This arbitration mechanism results in the starvation problem that lower-priority messages continuously lose arbitration to higher-priority ones. This starvation is seen as a critical section problem with priority scheduling, where a synchronization technique is required at the entry and exit of the bus. The techniques of non-starvation critical section with general semaphore and barrier synchronization are applied to enable the CAN bus to proceed without starvation. In this paper, we present a formal model of a starvation-free bitwise CAN arbitration protocol applying barrier synchronization and starvation-free mutual exclusion. Based on SPIN Promela, we provide that the proposed CAN starvation-free CAN bus model works correctly.