[00141634]安全关键软件测试与验证环境TesVESS

TesVESS是一个安全关键软件的测试与验证环境，能够从软件分析和设计阶段开始对软件的可靠性和可靠安全性进行保障。它以软件分析和设计模型为基础，有效地融合了安全关键性质的模型检验、针对安全关键性质的测试用例生成、安全关键软件可靠性测试使用模型的自动生成和测试加速等关键技术，从多种途径保障安全关键软件的可靠性和可靠安全性。TesVESS支持软件设计阶段的测试与验证活动，通过轻量级形式化方法提高了测试与验证的自动化程度；支持面向安全关键性质的切片模型检验技术，有效缩减了模型检验所需的状态空间，增强了软件设计阶段的安全性质保证能力；通过采用安全关键性质制导的状态搜索，能面向安全关键性质实施测试序列自动生成，提高了安全关键性质测试的针对性；支持构件化软件使用模型的自动综合与分析，提高了软件可靠性测试的工作效率。TesVESS有效集成基于模型的测试与验证技术，总体上达到了国际先进水平，其中UML切片模型检验技术和面向安全关键性质的测试用例生成技术处于国际领先。TesVESS为增强安全关键软件的可靠性和可靠安全性提供了重要保障，具有较高的自动化程度，能够避免由于软件失效造成的损失。TesVESS已在多家软件研制单位得到成功应用，取得良好效果。