《C/Verilog程式的MSVL驗證理論與方法》是依託西安電子科技大學，由段振華擔任項目負責人的重大研究計畫。
基本介紹
- 中文名：C/Verilog程式的MSVL驗證理論與方法
- 項目類別：重大研究計畫
- 項目負責人：段振華
- 依託單位：西安電子科技大學
中文摘要,結題摘要,
中文摘要
軟體已成為國防建設和國計民生的基礎設施，如何構造安全可靠的軟體系統是目前計算機軟體領域面臨的重大挑戰。本項目擬通過C/Verilog程式的MSVL模型檢測理論與方法，提高使用C/Verilog語言開發的網路和嵌入式軟體系統的可靠性和安全性。首先，研究C/Verilog程式到MSVL程式的轉換規則和轉換的語義等價性。然後，以得到的MSVL程式作為模型，研究MSVL的統一限界和抽象模型檢測理論與方法。進而，在上述研究的基礎上，開發C/Verilog程式的MSVL自動模型檢測平台，包括C/Verilog到MSVL程式轉換器，以及MSVL的統一限界和抽象模型檢測器。最後，以太空飛行器控制系統軟體的驗證為套用示範，展示本項目所建立的理論與方法在國家重大工程中的套用。
結題摘要
軟體已成為國防建設和國計民生的基礎設施，如何構造安全可靠的軟體系統是目前計算機軟體領域面臨的重大挑戰。本項目通過C/Verilog程式的MSVL模型檢測理論與方法，提高了使用C/Verilog語言開發的網路和嵌入式軟體系統的可靠性和安全性。為此，首先研究了C/Verilog程式到MSVL程式的轉換規則和轉換的語義等價性。然後，以得到的MSVL程式作為模型，研究MSVL的統一限界和抽象模型檢測理論與方法。進而，在上述研究的基礎上，開發了C/Verilog程式的MSVL自動模型檢測平台，包括C/Verilog到MSVL程式轉換器，以及MSVL的統一限界和抽象模型檢測器。最後，以太空飛行器控制系統軟體的驗證為套用示範，展示本項目所建立的理論與方法在國家重大工程中的套用。
