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

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

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

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

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