發(fā)布時(shí)間：2017-04-03 21:18

  本文關(guān)鍵詞：面向AltaRica模型的系統(tǒng)安全性設(shè)計(jì)驗(yàn)證方法研究，由筆耕文化傳播整理發(fā)布。

【摘要】：隨著計(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)功能行為,同時(shí)描述系統(tǒng)存在的失效行為的建模語言,面向AltaRica模型的系統(tǒng)安全性分析是當(dāng)前的研究熱點(diǎn)之一。目前已有相應(yīng)的一些工具利用AltaRica模型進(jìn)行系統(tǒng)安全性分析,而支持AltaRica模型的窮舉分析和時(shí)序?qū)傩苑矫娴尿?yàn)證工具還很缺少,成熟的模型檢測(cè)工具SPIN對(duì)模型的窮舉分析和線性時(shí)序邏輯驗(yàn)證有很大優(yōu)勢(shì),但SPIN工具并不能直接對(duì)AltaRica模型進(jìn)行驗(yàn)證。針對(duì)以上問題,本文首先將AltaRica模型轉(zhuǎn)換到Promela模型,對(duì)安全需求使用線性時(shí)序邏輯進(jìn)行規(guī)約;然后將Promela模型導(dǎo)入模型檢測(cè)工具SPIN進(jìn)行驗(yàn)證和分析;最后結(jié)合驗(yàn)證結(jié)果和可追蹤性信息模型,追蹤AltaRica模型存在的設(shè)計(jì)缺陷。本文的主要研究?jī)?nèi)容如下:第一,通過對(duì)AltaRica模型和Promela模型的語義分析,提出了AltaRica模型到Promela模型的轉(zhuǎn)換規(guī)則,并對(duì)兩模型語義的等價(jià)性進(jìn)行證明。使用線性時(shí)序邏輯對(duì)安全性需求進(jìn)行規(guī)約并結(jié)合轉(zhuǎn)換得到的Promela模型導(dǎo)入模型檢測(cè)工具進(jìn)行形式化驗(yàn)證。在此基礎(chǔ)上,提出一種面向AltaRica模型的系統(tǒng)安全性設(shè)計(jì)驗(yàn)證方法。第二,針對(duì)模型檢測(cè)的驗(yàn)證結(jié)果,給出了根據(jù)驗(yàn)證結(jié)果的反例路徑追蹤到AltaRica模型設(shè)計(jì)缺陷的可追蹤性信息模型。通過對(duì)驗(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)組件存在的安全性問題。第三,針對(duì)本文提出的面向AltaRica模型的系統(tǒng)安全性設(shè)計(jì)驗(yàn)證方法,設(shè)計(jì)并實(shí)現(xiàn)相應(yīng)的原型工具A2STool,對(duì)A2STool的功能模塊進(jìn)行相應(yīng)地說明,并給出該工具的設(shè)計(jì)框架、執(zhí)行流程以及關(guān)鍵的實(shí)現(xiàn)技術(shù)。最后,運(yùn)用本文提出的方法對(duì)機(jī)輪剎車系統(tǒng)控制單元進(jìn)行案例分析,利用原型工具給出了AltaRica模型到Promela模型轉(zhuǎn)換的完整過程,使用SPIN對(duì)Promela模型和安全性需求的線性時(shí)序邏輯規(guī)約進(jìn)行驗(yàn)證和分析,接著基于驗(yàn)證結(jié)果結(jié)合可追蹤性信息模型發(fā)現(xiàn)系統(tǒng)安全性設(shè)計(jì)缺陷。說明了本文方法的有效性和可行性,為系統(tǒng)的安全性分析提供了一種新思路。
【關(guān)鍵詞】：系統(tǒng)安全性設(shè)計(jì) AltaRica模型 線性時(shí)序邏輯 可追蹤性信息模型 模型檢測(cè)
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類號(hào)】：V227;TP368.1
【目錄】：

• 摘要4-5
• ABSTRACT5-12
• 第一章 緒論12-18
• 1.1 課題研究背景12-14
• 1.2 國(guó)內(nèi)外研究現(xiàn)狀及選題依據(jù)14-16
• 1.2.1 國(guó)內(nèi)外研究現(xiàn)狀14-16
• 1.2.2 選題依據(jù)16
• 1.3 論文組織結(jié)構(gòu)16-18
• 第二章 面向Alta Rica模型的系統(tǒng)安全性設(shè)計(jì)驗(yàn)證方法18-29
• 2.1 系統(tǒng)安全性設(shè)計(jì)AltaRica模型18-23
• 2.1.1 系統(tǒng)安全性設(shè)計(jì)AltaRica語言18-20
• 2.1.2 系統(tǒng)安全性設(shè)計(jì)AltaRica模型構(gòu)建20-23
• 2.2 形式化方法和模型檢測(cè)23-27
• 2.2.1 形式化方法23-24
• 2.2.2 模型檢測(cè)方法和工具24-26
• 2.2.3 面向模型檢測(cè)的可追蹤性26-27
• 2.3 面向AltaRica模型的系統(tǒng)安全性設(shè)計(jì)驗(yàn)證框架27-28
• 2.4 本章小結(jié)28-29
• 第三章 基于SPIN的AltaRica模型轉(zhuǎn)換與安全性驗(yàn)證29-42
• 3.1 Alta Rica模型和Promela模型的語義29-33
• 3.1.1 接口轉(zhuǎn)換系統(tǒng)的語義描述29-30
• 3.1.2 基于接口轉(zhuǎn)換系統(tǒng)的AltaRica模型語義描述30-32
• 3.1.3 基于接口轉(zhuǎn)換系統(tǒng)的Promela模型語義描述32-33
• 3.2 Alta Rica模型到Promela模型的轉(zhuǎn)換33-39
• 3.2.1 AltaRica模型到Promela模型的轉(zhuǎn)換規(guī)則33-37
• 3.2.2 AltaRica模型和Promela模型語義等價(jià)性證明37-39
• 3.3 基于SPIN的AltaRica模型安全性驗(yàn)證39-41
• 3.3.1 基于線性時(shí)序邏輯的安全性需求規(guī)約39-40
• 3.3.2 基于SPIN的AltaRica模型安全性驗(yàn)證40-41
• 3.4 本章小結(jié)41-42
• 第四章 系統(tǒng)安全性設(shè)計(jì)的可追蹤性42-53
• 4.1 面向系統(tǒng)安全性設(shè)計(jì)的可追蹤性信息模型構(gòu)建42-46
• 4.1.1 可追蹤性信息模型的元模型42-43
• 4.1.2 可追蹤性信息模型的構(gòu)建43-46
• 4.2 基于模型檢測(cè)的設(shè)計(jì)缺陷自動(dòng)查找46-49
• 4.2.1 模型檢測(cè)驗(yàn)證結(jié)果文件的處理46-48
• 4.2.2 基于可追蹤性信息模型的設(shè)計(jì)缺陷查找48-49
• 4.3 基于模型檢測(cè)的可追蹤性實(shí)例分析49-52
• 4.4 本章小結(jié)52-53
• 第五章 系統(tǒng)安全性設(shè)計(jì)驗(yàn)證工具的設(shè)計(jì)與實(shí)現(xiàn)53-65
• 5.1 系統(tǒng)安全性設(shè)計(jì)驗(yàn)證工具A2STool的設(shè)計(jì)53-56
• 5.1.1 原型工具設(shè)計(jì)框架53-55
• 5.1.2 原型工具處理流程55-56
• 5.2 系統(tǒng)安全性設(shè)計(jì)驗(yàn)證工具A2STool的實(shí)現(xiàn)56-59
• 5.2.1 AltaRica模型語法檢查56-57
• 5.2.2 模型轉(zhuǎn)換與驗(yàn)證57-59
• 5.3 機(jī)輪剎車系統(tǒng)控制單元的實(shí)例分析59-64
• 5.3.1 機(jī)輪剎車系統(tǒng)控制單元描述59-60
• 5.3.2 機(jī)輪剎車系統(tǒng)控制單元AltaRica模型構(gòu)建60-61
• 5.3.3 機(jī)輪剎車系統(tǒng)控制單元的安全性驗(yàn)證61-64
• 5.4 本章小結(jié)64-65
• 第六章 總結(jié)與展望65-67
• 6.1 論文工作總結(jié)65-66
• 6.2 未來工作展望66-67
• 參考文獻(xiàn)67-72
• 致謝72-73
• 在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文73-74
• 附錄 TFTA系統(tǒng)安全性設(shè)計(jì)模型AltaRica模型74-75

  本文關(guān)鍵詞：面向AltaRica模型的系統(tǒng)安全性設(shè)計(jì)驗(yàn)證方法研究，由筆耕文化傳播整理發(fā)布。

，

本文編號(hào)：284994