现在，工作在航空航天，国防，运输以及汽车工业的工程师们必须面对复杂的具有很高安全性要求的嵌入式软件开发，对于安全和质量管理部门来说在早期阶段使用最好的实践经验来恰当地设计和测试嵌入式系统显得十分重要。 TNI-Valiosys 提供了一个功能强大易于使用的基于模块设计的确认解决方案，它专注于 Simulink?/Stateflow? 用户。 这个安全检查模块显著提高了模块的可靠性，以及减少测试成本，而无需改变设计流。

仿真是在测试模型设计时采用的最传统的验证手段，它的本质是在功能上验证系统，不可能穷尽所有的测试，不可能运行到任意一个测试条件。当我们仅仅用仿真来验证模型时，一些原本不希望的情况很难由仿真达到，比如错过一个可能改变产品质量的情况；更糟的事，错过了可能破坏关键性系统的情况。

另外一点重要的是，在被仿真模型上手工建立及运行测试场景是非常耗时的，并且增加了仿真的成本。所以，需要在开发过程中尽可能早地采用新的验证方法以提升系统的可靠性。

易于验证你的 Simulink?/Stateflow? 的设计

TNI-Valiosys 的 Safety-Checker Blockset 使得工程师们可以用简单的拖放操作来形式化验证模型的属性（ Property ）。属性是连接到确认算子（如“ Never Together ”）的模型变量（如“ Cruise ControlActive ”，“ Driver Braking ”）的组合。对一个属性（如“ the cruise control should never be active while driver is braking ”）进行验证则启动了模型检查（ model checker ）

属性典型地表达了一个“非我所愿”的情况，模型检查为你验证这种情况出现与否。如果模型检查发现了一个反例（ counter-example ），你就可以重新在 Stateflow? 中执行以检查这个模块失败在哪里；如果没有发现反例，该属性即被验证并由此可以确知系统不可能达到这个情况，这样就节省了你试图通过仿真来达到该情况的时间，

图 1 Simulink 中“ Never Together ”属性的验证

图 2 为 Simulink 提供的验证算子

使用 TNI-Valiosys Safety-Checker Blockset 的好处

•  自动寻找不希望的情况，显著减少测试时间

•  通过提升测试覆盖率提高设计可靠性

•  和 Simulink?/Stateflow? 实现无缝集成

•  仿真的补充手段

•  自动化生成验证报告，能够兼容 MS-Word

•  支持需求管理

仿真可以突出出现的错误，但是对没有出现的错误无能为力。这正是 Safety-Checker Blockset 的主要功能。

应用

对于软件和系统工程师， Safety-Checker Blockset 工具专用于那些状态机比控制算法更占显著地位的软件的验证工作。

典型的应用有：

•  汽车

  X-By-Wire systems: Brake-BW, Steer-BW,Throttle-BW, Shift-BW...

  Radar-based systems:ACC, Pre-crash, Land keeping...

  Vehicle synthesis: multi-ECU architecture design, global vehicle safety

  Comfort: entry systems (key-less...), body-controllers

  Energy management: 42-V systems, hybrid systems, starters, fuel cells

  ...

•  航空 / 国防 / 空间

  Critical systems: flight controls, engine control,Attitude and Orbit Control Systems...

  Flight warning computers

  ...

支持的环境

•  支持的平台： Windows NT/2000/XP

•  Matlab 6.5 (R13) ， Simulink 5.0 ， Stateflow 5.0 ，或各以上版本