面向CAN总线健壮性的形式化建模与验证

摘要： 为评估控制器局域网络(Controller Area Network, CAN)攻击者入侵风险的影响，增强CAN总线设计的健壮性，提出了一种基于UPPAAL SMC的CAN总线健壮性验证方案。该方案首先针对嵌入式软件系统需求对CAN总线数据链路层与应用层进行形式化建模，采用模型检测技术对总线控制、收发、仲裁、应用层等功能进行仿真；其次使用攻击报文对CAN总线系统抗攻击性能进行验... （共8页）