成果名称：安全关键软件测试与验证环境TesVESS

　　成果简介

　　TesVESS是一个安全关键软件的测试与验证环境，能够从软件分析和设计阶段开始对软件的可靠性和可靠安全性进行保障。它以软件分析和设计模型为基础，有效地融合了安全关键性质的模型检验、针对安全关键性质的测试用例生成、安全关键软件可靠性测试使用模型的自动生成和测试加速等关键技术，从多种途径保障安全关键软件的可靠性和可靠安全性。TesVESS支持软件设计阶段的测试与验证活动，通过轻量级形式化方法提高了测试与验证的自动化程度;支持面向安全关键性质的切片模型检验技术，有效缩减了模型检验所需的状态空间，增强了软件设计阶段的安全性质保证能力;通过采用安全关键性质制导的状态搜索，能面向安全关键性质实施测试序列自动生成，提高了安全关键性质测试的针对性;支持构件化软件使用模型的自动综合与分析，提高了软件可靠性测试的工作效率。

　　TesVESS有效集成基于模型的测试与验证技术，总体上达到了国际先进水平，其中UML切片模型检验技术和面向安全关键性质的测试用例生成技术处于国际领先。TesVESS为增强安全关键软件的可靠性和可靠安全性提供了重要保障，具有较高的自动化程度，能够避免由于软件失效造成的损失。

　　TesVESS获军队科技进步二等奖，已在多家软件研制单位得到成功应用，取得良好效果。随着软件在航天、航天、交通、装备控制等领域的应用越来越广泛，其关键软件都需要测试与验证来保证其安全性和可靠性，市场前景广阔。

　　联系方式：

　　地址 湖南长沙国防科技大学科研部 邮编：410073

　　联系人：秦元岗 电话：0731-84572337，13308492604

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