成果名稱：安全關鍵軟件測試與驗證環境TesVESS

　　成果簡介

　　TesVESS是一個安全關鍵軟件的測試與驗證環境，能夠從軟件分析和設計階段開始對軟件的可靠性和可靠安全性進行保障。它以軟件分析和設計模型為基礎，有效地融合了安全關鍵性質的模型檢驗、針對安全關鍵性質的測試用例生成、安全關鍵軟件可靠性測試使用模型的自動生成和測試加速等關鍵技術，從多種途徑保障安全關鍵軟件的可靠性和可靠安全性。TesVESS支持軟件設計階段的測試與驗證活動，通過輕量級形式化方法提高了測試與驗證的自動化程度;支持面向安全關鍵性質的切片模型檢驗技術，有效縮減了模型檢驗所需的狀態空間，增強了軟件設計階段的安全性質保證能力;通過采用安全關鍵性質制導的狀態搜索，能面向安全關鍵性質實施測試序列自動生成，提高了安全關鍵性質測試的針對性;支持構件化軟件使用模型的自動綜合與分析，提高了軟件可靠性測試的工作效率。

　　TesVESS有效集成基于模型的測試與驗證技術，總體上達到了國際先進水平，其中UML切片模型檢驗技術和面向安全關鍵性質的測試用例生成技術處于國際領先。TesVESS為增強安全關鍵軟件的可靠性和可靠安全性提供了重要保障，具有較高的自動化程度，能夠避免由于軟件失效造成的損失。

　　TesVESS獲軍隊科技進步二等獎，已在多家軟件研制單位得到成功應用，取得良好效果。隨著軟件在航天、航天、交通、裝備控制等領域的應用越來越廣泛，其關鍵軟件都需要測試與驗證來保證其安全性和可靠性，市場前景廣闊。

　　聯系方式：

　　地址 湖南長沙國防科技大學科研部 郵編：410073

　　聯系人：秦元崗 電話：0731-84572337，13308492604

　　傳真：0731-84572300 E-mail：qyg318@126.com