A Finite State Analysis of Time-Triggered CAN (TTCAN) Protocol Using Spin

The paper presents a case study of the use of model checking for the analysis of an industrial protocol, a time triggered version of the CAN protocol (TTCAN). Our analysis of this protocol was carried out using the model checker Spin. The original CAN protocol can easily be modeled in Spin, but specifying TTCAN requires the provision of explicitly using time in the modeling language. With a view to express time triggered properties we use a discrete time version of Spin (DT-Spin). This extension allows one to quantify discrete time elapse between events by specifying the time slice in which they occur. Using DT-Spin we have been able to model TTCAN, and subsequently, verify a few of its time-triggered properties. This experience shows that it is possible to largely model TDMA-based protocols using discrete time