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

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