Paper Info
Title
A Finite State Analysis of Time-Triggered CAN (TTCAN) Protocol Using Spin
Abstract
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.
Year
DOI
Venue
2007
10.1109/ICCTA.2007.4
ICCTA
Keywords
Field
DocType
controller area networks,formal specification,formal verification,protocols,discrete time version,finite state analysis,model checking,modeling language,time-triggered controller area network protocol
CAN bus,Model checking,Computer science,Automaton,Modeling language,Real-time computing,Formal specification,Discrete time and continuous time,Time division multiple access,Formal verification
Conference
ISBN
Citations 
PageRank 
0-7695-2770-1
4
0.44
References 
Authors
6
2
Name
Order
Citations
PageRank
Indranil Saha129618.27
Suman Roy2217.25