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

  更多相關文章： 可追蹤性 謂詞邏輯 語義模型 推導 一致性檢驗

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

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

，

本文編號：1123671