不仅仅是测试

针对安全关键系统的证明

BTC 形式验证套件

针对安全关键系统的证明

BTC EmbeddedValidator(形式验证套件)是对安全关键需求进行形式验证的工具。形式验证是在量产C代码上执行的,形式验证基于在BTC EmbeddedSpecifier上定义的形式化需求。

 

不仅仅是测试

对于现代嵌入式开发项目中的典型软件组件,输入信号和标定量的可能值组合的数量几乎是无限的。因此,很明显的,即使是大量的测试用例也不能覆盖所有可能的路径。这意味着,即使有一个很好的测试用例集,仍然有一个疑问没有得到解答,那就是“是否仍然存在某个特定安全需求会被违反?”

BTC形式验证套件使用Model-Checking技术来自动提供完整的数学证明,表明一个需求不会被分析系统所违背。这就保证了不存在任何一组输入信号和标定量的值组合能将系统驱动到违反需求的状态。

 

 

 

 反例生成

如果一个需求被违反,BTC EmbeddedValidator以测试用例的形式提供一个反例。这个生成的测试便是一个说明如何将系统驱动到违反相应需求的状态的例子。

综合调试

如果已经生成了一个反例,您可以使用BTC EmbeddedPlatform的强大调试功能来自动生成调试环境。由此生成的调试环境可以是一个Simulink/TargetLink模型或者是一个VisualStudio 项目。