作者: 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.