《一種軟體功能性安全驗證理論和方法》是依託西安電子科技大學，由張琛擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：一種軟體功能性安全驗證理論和方法
- 項目類別：青年科學基金項目
- 項目負責人：張琛
- 依託單位：西安電子科技大學
中文摘要,結題摘要,
中文摘要
軟體已成為國防建設和國計民生的基礎設施，如何提高軟體的安全性是目前計算機軟體領域面臨的一個重要問題。本項目擬研究基於MSVL的軟體功能性安全驗證理論和方法。首先，定義UML的安全擴展規則得到UMLs模型，以建立軟體功能性安全的半形式化模型。其次，採用建模、仿真和驗證語言MSVL給出軟體功能性安全半形式化模型的形式化描述。然後，使用MSVL的性質描述語言命題投影時序邏輯PPTL公式描述待驗證的安全性質，通過基於MSVL的統一模型檢測方法驗證設計模型是否存在安全缺陷。最後，在理論研究的基礎上，設計、開發UMLs建模工具和UMLs到MSVL的模型轉換工具。
結題摘要
軟體已成為國防建設和國計民生的基礎設施，提高軟體的安全性是目前計算機軟體領域面臨的一個重要問題。本項目研究了基於MSVL的軟體功能性安全驗證理論和方法。首先，定義UML的安全擴展規則得到UML擴展模型，以建立軟體功能性安全的半形式化模型。其次，採用建模、仿真和驗證語言MSVL給出軟體功能性安全半形式化模型的形式化描述。然後，使用MSVL的性質描述語言命題投影時序邏輯PPTL公式描述待驗證的安全性質，通過基於MSVL的統一模型檢測方法驗證設計模型是否存在安全缺陷。並以航空電子系統的設計、實現為特定套用領域，研究了系統功能和體系結構的建模、驗證方法，模型之間的轉換規則。最後，在理論研究的基礎上，設計、開發了相關建模工具和模型轉換工具。
