面向AltaRica模型的系統(tǒng)安全性設(shè)計(jì)驗(yàn)證方法研究.pdf

1、隨著計(jì)算機(jī)技術(shù)的迅速發(fā)展，嵌入式系統(tǒng)在醫(yī)療、交通、通信、航空航天等安全關(guān)鍵領(lǐng)域已得到廣泛運(yùn)用。如何提高系統(tǒng)的安全性，防止災(zāi)難性事故發(fā)生，已經(jīng)成為當(dāng)前軟件工程領(lǐng)域重要的研究課題。AltaRica語言是一種描述正常情況下系統(tǒng)功能行為，同時描述系統(tǒng)存在的失效行為的建模語言，面向AltaRica模型的系統(tǒng)安全性分析是當(dāng)前的研究熱點(diǎn)之一。目前已有相應(yīng)的一些工具利用AltaRica模型進(jìn)行系統(tǒng)安全性分析，而支持AltaRica模型的窮舉分析和時序?qū)?/p>

2、性方面的驗(yàn)證工具還很缺少，成熟的模型檢測工具SPIN對模型的窮舉分析和線性時序邏輯驗(yàn)證有很大優(yōu)勢，但SPIN工具并不能直接對AltaRica模型進(jìn)行驗(yàn)證。
　　針對以上問題，本文首先將AltaRica模型轉(zhuǎn)換到Promela模型，對安全需求使用線性時序邏輯進(jìn)行規(guī)約；然后將Promela模型導(dǎo)入模型檢測工具SPIN進(jìn)行驗(yàn)證和分析；最后結(jié)合驗(yàn)證結(jié)果和可追蹤性信息模型，追蹤AltaRica模型存在的設(shè)計(jì)缺陷。本文的主要研究內(nèi)容如下：

3、r>　　第一，通過對AltaRica模型和Promela模型的語義分析，提出了AltaRica模型到Promela模型的轉(zhuǎn)換規(guī)則，并對兩模型語義的等價性進(jìn)行證明。使用線性時序邏輯對安全性需求進(jìn)行規(guī)約并結(jié)合轉(zhuǎn)換得到的Promela模型導(dǎo)入模型檢測工具進(jìn)行形式化驗(yàn)證。在此基礎(chǔ)上，提出一種面向AltaRica模型的系統(tǒng)安全性設(shè)計(jì)驗(yàn)證方法。
　　第二，針對模型檢測的驗(yàn)證結(jié)果，給出了根據(jù)驗(yàn)證結(jié)果的反例路徑追蹤到AltaRica模型設(shè)計(jì)缺陷的

4、可追蹤性信息模型。通過對驗(yàn)證結(jié)果和AltaRica模型的分析，首先給出驗(yàn)證結(jié)果可追蹤性信息模型的元模型；然后根據(jù)具體的追蹤目標(biāo)實(shí)例化元模型，得到可追蹤性信息模型；最后基于可追蹤性信息模型設(shè)計(jì)追蹤算法，實(shí)現(xiàn)根據(jù)驗(yàn)證結(jié)果的反例路徑追蹤查找AltaRica模型的設(shè)計(jì)缺陷甚至系統(tǒng)組件存在的安全性問題。
　　第三，針對本文提出的面向AltaRica模型的系統(tǒng)安全性設(shè)計(jì)驗(yàn)證方法，設(shè)計(jì)并實(shí)現(xiàn)相應(yīng)的原型工具A2STool，對A2STool的功能模