基于CAN的信息物理系統(tǒng)的形式化驗(yàn)證方法研究.pdf

1、信息物理系統(tǒng)被廣泛應(yīng)用于交通、醫(yī)療、能源等多個(gè)重要發(fā)展領(lǐng)域?？刂破骶钟蚓W(wǎng)（CAN）是一種現(xiàn)場(chǎng)總線，該總線可應(yīng)用于車載信息物理系統(tǒng)。在上述基于CAN的信息物理系統(tǒng)中，保證系統(tǒng)的安全性和可靠性是非常重要的。但是當(dāng)前對(duì)于該系統(tǒng)的驗(yàn)證方法存在驗(yàn)證過(guò)程不規(guī)范、系統(tǒng)分析驗(yàn)證時(shí)對(duì)性能方面分析不足以及可驗(yàn)證的系統(tǒng)規(guī)模較小等問(wèn)題。
　　為對(duì)基于CAN的信息物理系統(tǒng)進(jìn)行有效驗(yàn)證，提高人們對(duì)系統(tǒng)可靠性的可信度，本文首先提出了一種信息物理系統(tǒng)的形式化驗(yàn)證

2、框架，通過(guò)對(duì)系統(tǒng)的各部分組件分別建模并根據(jù)它們的交互關(guān)系形成整個(gè)系統(tǒng)的形式化邏輯模型，從而對(duì)系統(tǒng)進(jìn)行功能正確性驗(yàn)證和運(yùn)行性能評(píng)估；然后針對(duì)基于CAN的信息物理系統(tǒng)，提供了一種構(gòu)建時(shí)間自動(dòng)機(jī)的方法流程，構(gòu)建了系統(tǒng)各個(gè)基本模塊的時(shí)間自動(dòng)機(jī)模型，并對(duì)各個(gè)模型進(jìn)行了形式化描述；最后，基于所提出的驗(yàn)證框架以及時(shí)間自動(dòng)機(jī)模型，利用模型檢驗(yàn)工具UPPAAL對(duì)基于CAN的車載信息物理系統(tǒng)進(jìn)行了詳細(xì)建模，并對(duì)不同環(huán)境配置下的系統(tǒng)進(jìn)行了功能正確性驗(yàn)證以及性