文档名：面向CAN总线健壮性的形式化建模与验证
摘要：为评估控制器局域网络(ControllerAreaNetwork,CAN)攻击者入侵风险的影响,增强CAN总线设计的健壮性,提出了一种基于UPPAALSMC的CAN总线健壮性验证方案.该方案首先针对嵌入式软件系统需求对CAN总线数据链路层与应用层进行形式化建模,采用模型检测技术对总线控制、收发、仲裁、应用层等功能进行仿真;其次使用攻击报文对CAN总线系统抗攻击性能进行验证与分析,开发人员可根据验证结果改进软件需求参数指标.实验结果表明,参数优化后,在总线被攻击情况下节点传输的准确率保持在75%以上,应答正确率可提升12.4%,加强了总线抗攻击能力.该方法为嵌入式软件通信总线系统设计的合理性提供了理论指导,规避开发后期的风险,可广泛应用于通信总线安全性能验证领域.
作者：王一华 周晴 胡婉如 杜家昊 Author：WANGYihua ZHOUQing HUWanru DUJiahao
作者单位：中国科学院国家空间科学中心,北京100190;中国科学院大学,北京100049中国科学院国家空间科学中心,北京100190
刊名：电讯技术 ISTICPKU
Journal：TelecommunicationEngineering
年，卷(期)：2023, 63(9)
分类号：TP391
关键词：CAN总线 健壮性验证 需求建模 模型检测 时间自动机
Keywords：controllerareanetwork(CAN)bus robustnessverification requirementsmodeling modelchecking timedautomata
机标分类号：TP311TP27TN915.04
在线出版日期：2023年10月7日
基金项目：民用航天技术预先研究项目面向CAN总线健壮性的形式化建模与验证[
期刊论文] 电讯技术--2023, 63(9)王一华 周晴 胡婉如 杜家昊为评估控制器局域网络(ControllerAreaNetwork,CAN)攻击者入侵风险的影响,增强CAN总线设计的健壮性,提出了一种基于UPPAALSMC的CAN总线健壮性验证方案.该方案首先针对嵌入式软件系统需求对CAN总线数据链路层与应用层...参考文献和引证文献
参考文献
引证文献
本文读者也读过
相似文献
相关博文
面向CAN总线健壮性的形式化建模与验证 Robustness Verification Technology of CAN Bus Based on Formalization
面向CAN总线健壮性的形式化建模与验证.pdf
- 文件大小:
- 3.8 MB
- 下载次数:
- 60
-
高速下载
|
|
