基于時(shí)序故障樹的實(shí)時(shí)系統(tǒng)安全性驗(yàn)證方法研究.pdf

1、伴隨實(shí)時(shí)系統(tǒng)在信息關(guān)鍵領(lǐng)域的廣泛應(yīng)用，其復(fù)雜度也在不斷增加，如何保證實(shí)時(shí)系統(tǒng)安全性，避免財(cái)產(chǎn)損失甚至人員傷亡等災(zāi)難性事故的發(fā)生，已成為當(dāng)前軟件工程領(lǐng)域的研究重點(diǎn)。目前針對軟件安全性分析的研究工作主要集中在軟件需求規(guī)約和功能設(shè)計(jì)階段，以故障分析及功能建模方法作為主要技術(shù)支持。然而在軟件的實(shí)際開發(fā)過程中，安全需求分析和軟件設(shè)計(jì)過程相對獨(dú)立，研究工作尚未統(tǒng)一，致使一方面安全需求分析結(jié)果難以應(yīng)用于軟件設(shè)計(jì)之中為其提供指導(dǎo)；另一方面設(shè)計(jì)模型中缺乏

2、安全屬性來源無法對系統(tǒng)安全性予以保障。傳統(tǒng)的故障樹分析法及其擴(kuò)展模型可用于安全需求獲取，但無法確定獲取的安全需求在系統(tǒng)設(shè)計(jì)中是否得到滿足。系統(tǒng)體系結(jié)構(gòu)分析與設(shè)計(jì)語言AADL能夠?qū)ο到y(tǒng)功能及非功能屬性進(jìn)行描述，但缺乏對系統(tǒng)安全需求的直觀表達(dá)，很難發(fā)現(xiàn)系統(tǒng)的潛在危害。
　　本文利用模型檢測技術(shù)，將安全需求分析與軟件功能設(shè)計(jì)相結(jié)合，提出一種基于擴(kuò)展故障樹的實(shí)時(shí)系統(tǒng)安全性驗(yàn)證方法。該方法通過驗(yàn)證時(shí)序故障樹中提取的安全屬性是否在AADL建立

3、的系統(tǒng)模型中得到滿足實(shí)現(xiàn)系統(tǒng)安全性驗(yàn)證工作。論文主要研究內(nèi)容如下：
　　（1）為解決實(shí)時(shí)系統(tǒng)安全性驗(yàn)證問題，提出一種結(jié)合時(shí)序故障樹提取的安全屬性與AADL建立的系統(tǒng)模型對軟件安全性進(jìn)行驗(yàn)證的分析框架。
　?。?）為保證最小割集求解的軟件安全屬性的正確性，采用分步確認(rèn)的方法，為驗(yàn)證工作的正確執(zhí)行提供保障。主要包括結(jié)合測試用例的方法對時(shí)序故障樹的構(gòu)建正確性進(jìn)行驗(yàn)證以及借鑒定理證明的思想對安全屬性規(guī)約進(jìn)行一致性檢測。
　?。?/p>

4、3）為提供安全屬性驗(yàn)證所需系統(tǒng)模型，給出AADL建模子集到時(shí)間自動機(jī)的轉(zhuǎn)換規(guī)則，實(shí)現(xiàn)AADL模型到時(shí)間自動機(jī)模型的自動轉(zhuǎn)換，在模型檢測工具UPPAAL下對安全屬性進(jìn)行驗(yàn)證和分析。
　　最后，將本文提出的方法運(yùn)用到汽艇自動駕駛系統(tǒng)的案例分析中，給出系統(tǒng)時(shí)序故障樹的構(gòu)建及約簡過程，驗(yàn)證了時(shí)序故障樹構(gòu)建的正確性及提取的安全屬性的一致性；同時(shí)，給出系統(tǒng)速度控制模塊的AADL建模，將AADL模型轉(zhuǎn)換為時(shí)間自動機(jī)網(wǎng)，用UPPAAL進(jìn)行了驗(yàn)證與