Paper Info
Title
Modeling and Verifying the TTCAN Protocol Using Timed CSP
Abstract
As one of the most practical protocols, Time-Triggered CAN protocol (TTCAN), which is time triggered to ensure the real-time capability required by embedded systems, has been widely used in the automotive electric system development. In this paper, we present a formal model of the TTCAN protocol using Timed Communicating Sequential Processes (Timed CSP). All the components in the protocol are abstracted as CSP processes, thus the basic transmission in TTCAN is converted into the communication between different CSP processes. Besides, an error handling model is also proposed to capture the exception in the protocol. Finally, we use model checker Process Analysis Toolkit (PAT) to verify whether we can achieve model caters for some properties, which are specified using Linear Temporal Logic (LTL) formulas. Based on the verification results, our TTCAN model turns out to match the specification.
Year
DOI
Venue
2014
10.1109/TASE.2014.8
TASE
Keywords
Field
DocType
real-time capability,error handling model,protocols,communicating sequential processes,timed communicating sequential process,error handling,model caters,controller area networks,timed csp,csp process,time-triggered can protocol,ttcan protocol, timed csp, pat, modeling, verification,verification,automotive electric system development,linear temporal logic formula,ttcan protocol,pat,embedded system,temporal logic,ltl formula,model checker process analysis toolkit,embedded systems,modeling,formal specification,formal verification,formal model,software engineering
CAN bus,Model checking,Computer science,Communicating sequential processes,Linear temporal logic,Process analysis,Real-time computing,System development,Automotive industry,Distributed computing,Embedded system
Conference
Citations 
PageRank 
References 
1
0.37
3
Authors
6
Name
Order
Citations
PageRank
Qinwen Ran110.37
Xi Wu2379.97
Xin Li332.84
Jianqi Shi45712.50
Jian Guo551.90
Huibiao Zhu658386.68