Formal Verification of CAN Bus in Cyber Physical System

作者: Rui Wang , Yong Guan , Xiaojuan Li , Rui Zhang

DOI: 10.1109/QRS-C51114.2020.00050

关键词:

摘要: Cyber physical system (CPS) is a multi-dimensional complicated integrating computing, communication and environment. CPS widely used in safety-critical areas such as aerospace, intelligent transportation medical equipment. So ensuring the security reliability of great significance. Formal verification one useful ways. This paper builds timed automata models for process CAN bus CPS. Our research especially analyses gateway process, simulates transmission with different rates between external environment internal unit. The task also takes into account packet priority. model checking tool Uppaal to verify functional real-time properties. results illustrate that established can meet relevant properties, be transmitted an orderly efficient manner.

参考文章(22)
Hafizah Mansor, Konstantinos Markantonakis, Keith Mayes, CAN Bus Risk Analysis Revisit Information Security Theory and Practice. Securing the Internet of Things. pp. 170- 179 ,(2014) , 10.1007/978-3-662-43826-8_13
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar, Symbolic model checking with rich assertional languages Theoretical Computer Science. ,vol. 256, pp. 93- 112 ,(2001) , 10.1016/S0304-3975(00)00103-1
Dai Qiang Wang, ShiYou Gao, Yu Qing Chen, Yi Wang, Qiao Liu, Intelligent Control system based on CAN-bus for car doors and windows international conference on anti counterfeiting security and identification. pp. 242- 245 ,(2009) , 10.1109/ICASID.2009.5276906
Huan-Kai Peng, Youn-Long Lin, An optimal warning-zone-length assignment algorithm for real-time and multiple-QoS on-chip bus arbitration ACM Transactions in Embedded Computing Systems. ,vol. 9, pp. 35- ,(2010) , 10.1145/1721695.1721701
Can Pan, Jian Guo, Longfei Zhu, Jianqi Shi, Huibiao Zhu, Xinyun Zhou, Modeling and Verification of CAN Bus with Application Layer using UPPAAL Electronic Notes in Theoretical Computer Science. ,vol. 309, pp. 31- 49 ,(2014) , 10.1016/J.ENTCS.2014.12.004
Wen Jin, Xi Chen, Hui Qun Zhang, Modified Worst Case Response Time Analysis of CAN Bus Consisting of Nodes with Buffers Applied Mechanics and Materials. pp. 3393- 3396 ,(2014) , 10.4028/WWW.SCIENTIFIC.NET/AMM.513-517.3393
Renjun Li, Chu Liu, Feng Luo, A design for automotive CAN bus monitoring system vehicle power and propulsion conference. pp. 1- 5 ,(2008) , 10.1109/VPPC.2008.4677544
Rajeev Alur, David L. Dill, A theory of timed automata Theoretical Computer Science. ,vol. 126, pp. 183- 235 ,(1994) , 10.1016/0304-3975(94)90010-8
Jung-Yup Kim, Ill-Woo Park, Jungho Lee, Min-Su Kim, Baek-kyu Cho, Jun-Ho Oh, System Design and Dynamic Walking of Humanoid Robot KHR-2 international conference on robotics and automation. pp. 1431- 1436 ,(2005) , 10.1109/ROBOT.2005.1570316
I.F. Akyildiz, Weilian Su, Y. Sankarasubramaniam, E. Cayirci, A survey on sensor networks IEEE Communications Magazine. ,vol. 40, pp. 102- 114 ,(2002) , 10.1109/MCOM.2002.1024422