@inproceedings{0a984aa0c02c4827b4836ae71b16322f,
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.",
keywords = "Modeling, PAT, TTCAN protocol, Timed CSP, Verification",
author = "Qinwen Ran and Xi Wu and Xin Li and Jianqi Shi and Jian Guo and Huibiao Zhu",
note = "Publisher Copyright: Copyright {\textcopyright} 2014 by The Institute of Electrical and Electronics Engineers, Inc.; 8th International Symposium on Theoretical Aspects of Software Engineering, TASE 2014 ; Conference date: 01-09-2014 Through 03-09-2014",
year = "2014",
month = dec,
day = "4",
doi = "10.1109/TASE.2014.8",
language = "英语",
series = "Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "90--97",
booktitle = "Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014",
address = "美国",
}