發(fā)布時(shí)間：2017-10-31 20:38

  本文關(guān)鍵詞：基于謂詞邏輯的需求追蹤方法研究

  更多相關(guān)文章： 可追蹤性 謂詞邏輯 語義模型 推導(dǎo) 一致性檢驗(yàn)

【摘要】：嵌入式軟件在航空、核能及交通等安全關(guān)鍵領(lǐng)域應(yīng)用廣泛,保障其安全性至關(guān)重要。在軟件開發(fā)過程中維持軟件制品間的可追蹤性是保障軟件安全性面臨的一個(gè)重要挑戰(zhàn)。當(dāng)前的可追蹤性研究主要存在兩個(gè)問題:一方面,可追蹤性研究主要集中在需求與代碼、設(shè)計(jì)與代碼間,缺乏需求間、需求與設(shè)計(jì)間的可追蹤性研究;另一方面,主流的追蹤關(guān)系建立方法如基于信息檢索的關(guān)系恢復(fù)等,所建立的追蹤信息精確性和完整性不高,往往無法有效應(yīng)用于安全關(guān)鍵領(lǐng)域的軟件開發(fā)。針對(duì)上述問題,本文提出一種基于謂詞邏輯的、描述需求間以及需求與設(shè)計(jì)間追蹤信息的語義模型。基于該語義模型,可以實(shí)現(xiàn)追蹤關(guān)系的自動(dòng)推導(dǎo)和檢驗(yàn),保證追蹤關(guān)系的精確和完整。論文的主要研究?jī)?nèi)容包括:(1)構(gòu)造了支持需求追蹤的語義模型。首先定義了一個(gè)基于謂詞邏輯的符號(hào)系統(tǒng)描述制品間的追蹤信息,并分別給出了需求間依賴、精化、分解和沖突關(guān)系的語義,以及需求與狀態(tài)圖間的可滿足關(guān)系語義。(2)基于語義模型,給出追蹤關(guān)系的推導(dǎo)和檢驗(yàn)方法。通過分析關(guān)系語義,給出需求間隱含關(guān)系的推導(dǎo)、關(guān)系的一致性檢驗(yàn)規(guī)則,并設(shè)計(jì)了自動(dòng)推導(dǎo)和檢驗(yàn)算法。此外,給出支持需求與設(shè)計(jì)間可滿足關(guān)系推導(dǎo)和檢驗(yàn)的約束規(guī)則。(3)根據(jù)本文所提出的方法,設(shè)計(jì)并實(shí)現(xiàn)了支持需求追蹤的原型工具,該工具可建模制品間的追蹤信息,實(shí)現(xiàn)對(duì)追蹤關(guān)系的分析,并結(jié)合一個(gè)應(yīng)用實(shí)例說明本文方法的可行性和有效性。
【關(guān)鍵詞】：可追蹤性 謂詞邏輯 語義模型 推導(dǎo) 一致性檢驗(yàn)
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類號(hào)】：TP311.52
【目錄】：

• 摘要4-5
• ABSTRACT5-10
• 縮略詞10-11
• 第一章 緒論11-16
• 1.1 課題研究背景11-12
• 1.2 國(guó)內(nèi)外研究現(xiàn)狀及選題依據(jù)12-14
• 1.2.1 國(guó)內(nèi)外研究現(xiàn)狀12-14
• 1.2.2 選題依據(jù)14
• 1.3 論文組織結(jié)構(gòu)14-16
• 第二章 基于謂詞邏輯的需求追蹤方法16-25
• 2.1 可追蹤性16-19
• 2.1.1 可追蹤性基礎(chǔ)16-18
• 2.1.2 追蹤關(guān)系分類18-19
• 2.2 謂詞邏輯19-22
• 2.2.1 謂詞邏輯語法19-20
• 2.2.2 謂詞邏輯語義20-22
• 2.3 基于謂詞邏輯的需求追蹤框架22-24
• 2.3.1 需求可追蹤信息模型22-23
• 2.3.2 基于謂詞邏輯的需求追蹤框架23-24
• 2.4 本章小結(jié)24-25
• 第三章 支持需求追蹤的語義模型25-36
• 3.1 基于謂詞邏輯的符號(hào)系統(tǒng)25-27
• 3.2 需求間追蹤關(guān)系語義27-34
• 3.2.1 依賴關(guān)系語義28-30
• 3.2.2 精化關(guān)系語義30-31
• 3.2.3 分解關(guān)系語義31-33
• 3.2.4 沖突關(guān)系語義33-34
• 3.3 需求與設(shè)計(jì)間可滿足關(guān)系語義34-35
• 3.4 本章小結(jié)35-36
• 第四章 基于語義模型的追蹤關(guān)系推導(dǎo)及檢驗(yàn)36-50
• 4.1 需求關(guān)系到公式關(guān)系的映射36-38
• 4.2 需求間隱含追蹤關(guān)系的推導(dǎo)38-43
• 4.2.1 推導(dǎo)規(guī)則38-39
• 4.2.2 自動(dòng)推導(dǎo)的算法設(shè)計(jì)39-43
• 4.3 需求關(guān)系的一致性檢驗(yàn)43-47
• 4.3.1 一致性檢驗(yàn)規(guī)則43-44
• 4.3.2 自動(dòng)檢驗(yàn)的算法設(shè)計(jì)44-47
• 4.4 需求與狀態(tài)圖元素間可滿足關(guān)系的約束規(guī)則47-49
• 4.5 本章小結(jié)49-50
• 第五章 需求追蹤原型工具的設(shè)計(jì)與實(shí)現(xiàn)50-60
• 5.1 需求追蹤工具系統(tǒng)設(shè)計(jì)50-51
• 5.1.1 系統(tǒng)架構(gòu)50-51
• 5.1.2 系統(tǒng)執(zhí)行流程51
• 5.2 主要模塊實(shí)現(xiàn)51-54
• 5.2.1 關(guān)系推導(dǎo)模塊51-53
• 5.2.2 關(guān)系檢驗(yàn)?zāi)K53-54
• 5.3 襟縫翼控制單元案例分析54-59
• 5.3.1 需求關(guān)系的推導(dǎo)及檢驗(yàn)54-57
• 5.3.2 可滿足關(guān)系的推導(dǎo)及檢驗(yàn)57-59
• 5.4 本章小結(jié)59-60
• 第六章 總結(jié)與展望60-62
• 6.1 論文工作總結(jié)60
• 6.2 未來工作展望60-62
• 參考文獻(xiàn)62-67
• 致謝67-68
• 在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文68

，

本文編號(hào)：1123671