|
1、通过T-VEC发现火星着陆器的缺陷
(洛克希德.马丁公司)
火星极地登陆器1999年1月3日发射并且在
飞行了3千5百万英里后于1999年12月3日坠毁，总耗资约一亿六千五百万美元 ;在着陆前大约40 米的伪着陆指示应当被降落监控器
(TDM) 忽略，但是由于设计缺陷，事件指示被 “锁存,” 导致引擎被过早关机。
T-VEC的工程师将Lockheed
Martin的提供的着陆部分的文本模式的需求用了大概一天的时间使用T-VEC进行形式化的描述，就发现了导致着陆系统失效的问题所在。
Lockheed
Martin使用T-VEC结论如下：
-
发现火星极登陆器的缺陷
-
早期发现需求缺陷减少返工
-
可测试的需求帮助排除返工
-
测试计划时间减少50%以上
-
自动测试生成减少90%以上的手工工作
-
对测试用例开发和执行的优化避免了测试冗余
-
可以实行对需求覆盖的计划和度量
-
显著节省费用
2、通过T-VEC发现需求中隐藏的缺陷（罗克韦尔.柯林斯公司）
Rockwell
Collins在其FGS项目中采用T-VEC进行需求形式化和分析，该技术采用后，在原有的基础上，发现了25个新的以前所没有发现的问题。
从这个实际的工程中，可以明显的看出T-VEC的需求形式化和，需求分析验证功能能够发现很多使用传统方式难以发现的隐藏在工程中的深层次的缺陷。
|
