嵌入式系统验证新视角：基于SCADE Suite模型

1、基于SCADE Suite模型的验证

1.1 不含模型的传统验证手段

《安全关键软件开发与审定—DO-178C标准实践指南》书中指出：验证，是应用于整个软件生命周期的一个整体性过程。在DO-178C中的验证，是包括评审、分析和测试的一个组合。评审是提供一个定性的评估；分析是提供正确性的可重复的证据；测试是运行一个系统或系统部件，以验证它满足指定的需求并检测其错误。

1.2 新增模型后的验证手段：模型仿真

《基于模型的开发和验证标准—DO-331》中指出使用基于模型的开发和验证(MBDV)后，就在传统验证手段基础上增加了模型仿真。模型仿真指使用仿真器检查一个模型行为的活动，模型仿真器是一个设备、计算机程序或系统，使得一个模型能够执行以表明其行为，从而支持验证确认。DO-178C中原先通常由评审，分析和测试完成的验证工作，可以由模型仿真部分来代替或者组合进行。具体验证流程中使用的关于模型仿真的方法，需要写入验证计划并通过局方的审查，DO-331提供了模型仿真的专门指南。

针对软件高层需求、软件低层需求、软件架构这些数据，相对于评审和分析的传统手段，模型仿真是一种动态的验证手段，更加直观有效。模型仿真的主要特点是：

• 测试是针对可执行目标码来进行的，模型仿真主要是针对低层需求(设计模型和软件架构)的仿真；

• 大部分模型仿真工具使用的代码通常不同于加载到目标环境的代码；

• 模型仿真的环境通常是PC，也不同于测试使用的目标机运行环境。

所以，使用模型仿真依然不能省略在目标机上的测试活动。DO-331的MB.6.8.3节指出：模型是基于需求开发出来的，为模型仿真而开发的仿真用例和仿真规程，也应该是基于同样的需求编写的。考察DO-178C的流程，Suite模型通常相当于低层需求，则Suite模型、仿真用例和仿真规程都是基于高层需求设计的。如果仿真用例和仿真规程用于正式验证置信度，那么，仿真用例和仿真规程的准确性需要验证，仿真结果需要评审，仿真结果与预期结果的差异需要解释。

1.3 SCADE Suite模型支持的验证工具

SCADE模型检查器 (Model Checker) 支持静态检查Suite模型的语法语义，这是最基本的验证活动，也是成功运行其他SCADE验证工具和方法的前提。它通过一组内置的规则检查SCADE模型，检查完毕后生成报告，其中包含检测到的可能的警告或错误。其主要功能是检查1.丢失的或多余的定义；2类型一致性；3. 时序一致性；4. 因果分析的一致性；5. 初始化分析一致性等规则。

SCADE模型仿真器 (Model Simulation) 支持在PC端仿真模型的行为，也可以作为QTE大规模自动化模型仿真活动之前的预仿真。SCADE 仿真器是可视化的调试环境，支持断点设定，测试用例的保存、载入、测试结果的输出等功能完成模型仿真。

SCADE认证级测试环境 (Qualified Test Environment) 是一套自动化环境，除融合了模型仿真和模型覆盖验证功能外，还支持管理仿真用例、仿真规程和仿真结果。

SCADE模型覆盖分析 (Model Coverage) 支持低层需求的覆盖验证。除了可以单独执行外，更常见的操作是基于QTE进行大规模自动化的模型覆盖。

以上四个工具可应用于SCADE开发安全关键项目中最基本的验证活动。除此之外，还有SCADE快速原型(Rapid Prototype)，SCADE形式化验证(Design Verify)（*关于该部分内容可详细参考《基于SCADE模型的形式化方法》的第五节），SCADE最坏运行时间和堆栈分析(Timing and Stack Optimizer)，SCADE编译器验证套件(Complier Verification Kit)，SCADE软件生命周期管理(ALM)桥接器和SCADE多学科仿真文件生成(FMI/FMU)生成器等工具用于其他的验证活动。

2、SCADE认证级测试环境Qualified Test Environment