面向CAN總線健壯性的形式化建模與驗證

摘要： 為評估控制器局域網絡(Controller Area Network, CAN)攻擊者入侵風險的影響，增強CAN總線設計的健壯性，提出了一種基于UPPAAL SMC的CAN總線健壯性驗證方案。該方案首先針對嵌入式軟件系統(tǒng)需求對CAN總線數據鏈路層與應用層進行形式化建模，采用模型檢測技術對總線控制、收發(fā)、仲裁、應用層等功能進行仿真；其次使用攻擊報文對CAN總線系統(tǒng)抗攻擊性能進行驗...