Abstract—It is inevitable that the response time of a message is delayed in a CAN network where multiple ECUs share a single bus. However, delays of response time should be minimized for messages related to the safety of a driver or a vehicle. If the response time exceeds the deadline, the safety of the driver and the whole of the vehicle system may be impaired. Therefore, it is essential to verify the CAN database in advance so that the response time of a message does not exceed the deadline. In this paper, we propose a framework composed of UPPAAL and a DBC2XML component, which automatically generates a UPPAAL model from a CAN database and show how to verify the CAN database using this framework.
Index Terms—Controller area network, DBC, formal verification, UPPAAL.
Beomyeon Cho and Taewook Kim are with the Department of Automotive Convergence, Korea University, Seoul, Korea (e-mail: bycho@ formal.korea.ac.kr, twkim@formal.korea.ac.kr).
Jin-Young Choi is with Graduate School of Information Security, Korea University, Seoul, Korea (e-mail: choi@formal.korea.ac.kr).
[PDF]
Cite:Beomyeon Cho, Taewook Kim, and Jin-Young Choi , "CAN Database Verification Framework Using UPPAAL," International Journal of Computer Theory and Engineering vol. 9, no. 6, pp. 438-442, 2017.
