产品
本文作为#嵌入式系统Ansys SCADE系列专题内容，此次将主要介绍『基于SCADE Suite模型的验证』，第一部分是关于验证手段的介绍，其中包含Ansys SCADE Suite支持的验证工具介绍；第二部分是介绍如何使用SCADE认证级测试环境；第三至第七部分是其他验证手段的介绍。
1基于SCADE Suite模型的验证
1.1 不含模型的传统验证手段
《安全关键软件开发与审定—DO-178C标准实践指南》书中指出：验证，是应用于整个软件生命周期的一个整体性过程。在DO-178C中的验证，是包括评审、分析和测试的一个组合。评审是提供一个定性的评估；分析是提供正确性的可重复的证据；测试是运行一个系统或系统部件，以验证它满足指定的需求并检测其错误。
1.2 新增模型后的验证手段：模型仿真
《基于模型的开发和验证标准—DO-331》中指出使用基于模型的开发和验证(MBDV)后，就在传统验证手段基础上增加了模型仿真。模型仿真指使用仿真器检查一个模型行为的活动，模型仿真器是一个设备、计算机程序或系统，使得一个模型能够执行以表明其行为，从而支持验证确认。DO-178C中原先通常由评审，分析和测试完成的验证工作，可以由模型仿真部分来代替或者组合进行。具体验证流程中使用的关于模型仿真的方法，需要写入验证计划并通过局方的审查，DO-331提供了模型仿真的专门指南。
针对软件高层需求、软件低层需求、软件架构这些数据，相对于评审和分析的传统手段，模型仿真是一种动态的验证手段，更加直观有效。模型仿真的主要特点是：
所以，使用模型仿真依然不能省略在目标机上的测试活动。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)生成器等工具用于其他的验证活动。
2SCADE认证级测试环境Qualified Test Environment
图表1: SCADE认证级测试环境工作流
大规模的自动化验证活动推荐使用SCADE的认证级测试环境(Qualified Test Environment)来操作。SCADE QTE是可通过DO-330 TQL-5级别鉴定的验证工具。SCADE QTE工作流，主要分为如下个步骤
2.1 基于需求创建测试用例
SCADE Suite模型最常用的测试用例类型是扩展名为.sss的文件，该文件基于Tcl脚本格式的仿真文件格式，可扩展性强。其主要的语法规则如下:
下图是测试用例规则的范例
图表2: SCADE测试用例范例
从SCADE 2020版本开始，测试用例脚本语言新增了一些扩展，以支持用户更好地设计测试用例
2.1.1 输出参数支持使用Lambda表达式来检查范围
Lambda 表达式 (lambda expression) 支持以匿名函数形式编写测试用例中的输出参数
图表3: 测试用例的输出参数支持使用Lambda表达式
2.1.2 输出参数支持使用区间表达式来检查范围
区间表达式中，可取边界值用[]符号，不可取边界值用][符号，注意不是用()符号
2.1.3 输入输出参数支持直接使用模型中的常量来设置
图表5: 测试用例的输入输出参数支持使用模型中的常量
2.1.4 输入输出参数支持IEEE754标准定义的无穷数Inf和非数值Nan的使用
图表6: 测试用例的输入输出参数支持IEEE754标准定义的无穷数Inf和非数值Nan
2.1.5 输入输出支持对字符串的某字符进行单独设置
图表7: 测试用例的输入输出参数支持设置字符串的某单独字符
2.2 执行在主机上的功能测试
使用SCADE QTE在主机上进行功能测试的结果如下图，既有图形化的报告，也有文本化的报告。图形化的报告既有按照测试场景周期排列的，也有按照图形比对结果排列的。可以从结果报告中看到测试用例编号、待测变量名称、实际输出、期望输出、精度约束等信息。
图表8: 使用SCADE QTE在主机上进行功能测试
使用SCADE QTE在主机上进行功能测试
2.3 执行在主机上的模型覆盖分析
《基于模型的开发和验证标准—DO-331》中指出模型覆盖分析支持检测和解决
《安全关键软件开发与审定—DO-178C标准实践指南》中指出代码结构覆盖分析支持检测和解决
另外，覆盖分析需要依据不同的软件研制级别选择特定的覆盖准则。DO-178C中定义了以下几个准则：
使用SCADE软件进行MBDV开发时，仅需设计一套基于高层需求的仿真用例和仿真规程，即可同时应用于设计模型的覆盖分析、代码结构的覆盖分析。
SCADE MTC是可通过DO-330 TQL-5级别鉴定的验证工具。程序插桩(Instrument)是覆盖分析的关键技术之一，它是在保证被测程序原有逻辑完整性的基础上插入一些探针(本质上就是进行信息采集的代码段，可以是赋值语句或采集覆盖信息的函数调用) ，通过探针的执行并抛出程序运行的特征数据，通过对这些数据的分析，可以获得程序的控制流和数据流信息，进而得到逻辑覆盖等动态信息，从而实现测试目的的方法。SCADE同样使用插桩技术进行覆盖分析, SCADE MTC在2019版本之前是可通过DO-178C/DO-330 TQL-5级别鉴定的验证工具。
使用SCADE QTE在主机上进行模型覆盖分析结果如下图，可以便捷地通过颜色来区分覆盖分析的完整度，绿色是完全覆盖，黄色是部分覆盖，红色是未覆盖。
使用SCADE QTE在主机上进行模型覆盖分析
2.3.1 模型覆盖分析的新特性
从SCADE 2019版本开始，SCADE Suite的覆盖分析工具经过改进提升，可通过DO-178C/DO-331 TQL-4级鉴定，因此在一定条件下，使用该工具进行的模型覆盖分析也等价于代码结构覆盖分析。
而在结构覆盖点不充分时，支持使用预定义的定制操作符进行覆盖分析。定制覆盖方法中需要区分出覆盖观察操作符(CO: Coverage Observer)和被观察操作符(Observee)，覆盖观察操作符CO需要将被观察操作符的所有I/O都作为输入，根据覆盖观察操作符CO的输出不同，分为三种定制覆盖情况。
2.3.1.1 覆盖观察操作符CO无输出
2.3.1.2 覆盖观察操作符CO仅返回一个输出
图表12: 定制模型覆盖分析情况二，CO仅返回一个输出
2.3.1.3 覆盖观察操作符CO返回与被观察操作符同样多的输出
图表13: 定制模型覆盖分析情况三，CO返回若干个输出
2.3.2 使用形式化分析引擎协助进行模型覆盖分析
作为完整的验证活动的一部分, 覆盖分析总是最耗时的。在大型认证级项目中，工程师们很难对某些嵌套关系或者组合关系特别复杂的分支快速便捷地设计出对应的测试用例，以分析出该未覆盖的分支到底是：
SCADE Suite从2021版本开始推出使用形式化方法来协助分析模型覆盖结果，该方法可以极大地减少工程师们在模型覆盖分析活动中的工作量，在国内航空航天、轨道交通几家单位的试点应用后反馈良好。该方法的原理可参考《基于SCADE模型的形式化方法》中第六节的内容。通常该方法的分析结果有三种
该方法既可以在模型开发阶段使用，也可以在模型的验证阶段使用。为了缩小分析的状态空间，该方法同样支持在模型中添加包括Assume和Guarantee在内的约束,使得形式化分析引擎在限定的范围内得出有意义的结果。
使用老版本SCADE软件的用户也可以通过升级软件并使用该功能来积累测试用例，然后退回到老版本SCADE中复用先前积累的测试用例进行覆盖分析。值得一提的是，推导出来的测试用例需要进行评审或分析，补充可能的高层需求。
2.3.2.1 在开发阶段使用形式化方法对模型的覆盖分析
在开发阶段对模型的覆盖分析，有助于设计人员自主分析出所设计的模型是否有非预期的不可达分支，提前改正可能的错误，以减轻后期验证阶段测试人员覆盖分析的工作量。使用方法是在开发工程中，右键单击某操作符，在弹出菜单中选择Coverability Analysis->Analyze，等待片刻后(模型越复杂等待时间越长)，会得出分析结果。如果分支可以覆盖，条目的背景色为绿色，Result列显示COVERABLE，并在最后一列返回出可覆盖该分支的测试用例的文件路径超链接，可点击该超链接打开该文件。如果分支不可覆盖，条目的背景色为红色，Result列显示NOT COVERABLE，且最后一列为空。
图表14: 在开发阶段使用形式化方法对模型的覆盖分析，结果可覆盖
2.3.2.2 在验证阶段使用形式化方法对模型的覆盖分析
在验证阶段对模型的覆盖分析操作方法是先做完2.3节主机上的模型覆盖分析后，针对验证工程中未覆盖的分支，右键单击某分支未完全覆盖的操作符，在弹出菜单中选择Coverability Analysis->Analyze，等待片刻后(模型越复杂等待时间越长)，会得出分析结果。
使用形式化分析引擎协助进行模型覆盖分析
2.4 执行在主机上的代码覆盖分析
如2.3节所述，在SCADE 2019版本之前，SCADE Suite 覆盖分析工具仅可通过DO-178C/DO-331 TQL-5级工具鉴定，因此需要进行模型覆盖分析和代码覆盖分析两项验证活动。而在在SCADE 2019版本之后，SCADE Suite覆盖分析工具可通过DO-178C/DO-331 TQL-4级鉴定，因此在一定条件下，使用该工具进行的模型覆盖分析等价于代码结构覆盖分析。如果用户使用的是老版本的SCADE工具，依然可以通过单击代码分析按钮的操作，获取模型对应的代码级覆盖分析结果。
2.5 执行在目标机上的测试
如果需要在目标机上进行软硬件集成测试时，SCADE QTE支持将主机上测试完毕后得到的测试用例转换为可连接目标机的第三方程序对应的测试用例，以便用户能简单快捷地进行目标机上的测试。SCADE QTE可支持向LDRA Test，IBM RTRT，VectorCast，CANTAT和RapiTest等多款软件的测试用例转换。
图表18: 使用SCADE QTE在目标机上的测试
3SCADE快速原型 (Rapid Prototype)
SCADE快速原型 (Rapid Prototype) 支持快速设计人机界面，可用于和SCADE Suite模型的接口映射后，进行交互式验证或直接生成独立可执行程序。
图表19: SCADE快速原型 (Rapid Prototype) 设计的人机界面
SCADE快速原型界面与SCADE Suite模型进行联合仿真
4SCADE最坏运行时间和堆栈分析(Timing and Stack Optimizer)
SCADE嵌入了AbsInt公司的aiT WCET和StackAnalyzer两个工具，并在此基础上定制形成了SCADE Suite TSO/TSV (Timing and Stack Optimizer/Verifier) 两款工具，使得用户可基于Suite模型直接进行性能分析，以满足DO-178C中目标机兼容方面的分析工作。aiT WCET和StackAnalyzer两款工具的详细介绍可参考安装目录下AbsInt公司的手册。
图表20: SCADE Suite运行最坏运行时间和堆栈分析的工作流
5
SCADE编译器验证套件 (Complier Verification Kit)
在安全关键项目的开发中，SCADE编译器验证套件主要有两大作用
1.CVK支持验证编译器
是否可以将SCADE Suite KCG生成的C代码正确地编译为目标码。
2.在项目前期通过使用CVK后，以极小的工作量就可以得出目标机兼容相关的限制信息。可在此基础上定制Suite建模规范，完善DO-178C标准的计划过程中的开发标准。另外，也可以设计专门的规则检查器，以检测设计的模型是否违反了定制的建模规范。
编译器验证包主要包括如下内容
6
SCADE软件生命周期管理 (ALM)桥接器
DO-178C标准的5.5节描述了软件开发过程的可追踪性要求：
应建立系统需求和高层需求之间的双向可追踪性，以便能完成以下功能和目标。
应建立低层需求和高层需求之间的双向可追踪性，以便能完成以下功能和目标。
应建立低层需求和源代码之间的双向可追踪性，以便能完成以下功能和目标。
DO-178C标准的6.5节主要描述软件验证过程的可追踪性要求：
应建立软件需求和测试用例之间的双向可追踪性，以便能完成以下功能和目标。
支持基于需求的测试覆盖分析。
应建立测试用例和测试规程之间的双向可追踪性，以便能完成以下功能和目标。
验证测试用例被完整地开发成测试规程了。
应建立测试规程和测试结果之间的双向可追踪性，以便能完成以下功能和目标。
验证测试规程是否被完整地执行了
SCADE软件生命周期管理 (ALM: Application Lifecycle Management) 桥接器支持与第三方ALM工具连接起来，将SCADE Architect架构模型，SCADE Suite控制模型，SCADE Display人机界面模型，SCADE Test测试用例与高层需求进行双向追踪，帮助用户管理需求、模型、测试用例、测试规程等和其他结构化文档之间的追踪关系。SCADE当前支持桥接的第三方ALM工具包括Reqtify，DORRS 9.6+(Native)，DOORS Next Generation，Jama和Polarion等。
图表22: SCADE软件生命周期管理 (ALM)桥接器的简易操作方法
7SCADE多学科仿真文件生成 (FMI/FMU)
FMI标准的全称是Functional Mock-up Interface，是一个不依赖于工具的标准，其通过XML文件和已编译的C代码的组合来同时支持动态模型的模型交换 (Model Exchange) 和联合仿真 (Co-Simulation) 。两者的区别是模型交换方法导出的FMU文件不包含求解模型方程的求解器，而联合仿真方法导出的FMU文件包含求解模型方程的求解器。即是否包含求解器是两者最大的区别。
由于FMI标准是一个通用的第三方接口标准，不依赖于任何工具特有的接口形式。所以，只要是支持FMI标准的工具都可以将其他工具导出的FMU文件导入到自身的软件平台内，这时仿真软件会自动解析FMU中的.xml文件，并在软件的操作界面上给用户提供操作FMU的选项。
SCADE多学科仿真文件生成 (FMI/FMU) 支持将SCADE模型导出为FMU文件后，再导入到多学科仿真平台中进行系统级仿真。
使用SCADE生成FMU文件，并导入到Ansys数字孪生软件中联合仿真
免责声明：本文系网络转载或改编，未找到原创作者，版权归原作者所有。如涉及版权，请联系删
155-2731-8020
