装备电子系统的研发、测试、保障解决方案中心

符合DO-178B/C验证要求的需求可追踪工具VeroTrace

VeroTrace是一个需求和生命周期可追踪管理的工具，允许产生、管理和发布用于支持DO-178B/C软件认证/审核的所有数据。它可以追踪系统需求、软件需求，追踪与需求相关的工件，例如：源代码，设计组件，功能测试结果，覆盖率测试结果。

 VeroTrace提供一个需求跟踪数据库，在数据库中可以添加、修改、删除、提问，追踪验证状态，执行在线验证，可以从配置管理中提取工件数据，创建验证检查列表，提供在工件和验证证据之间基本的跟踪XML文件。VeroTrace通过自动生成超链接的可追踪性信息，可以组织需求、与需求相关的工件及所有评审文件，到一个链接所有生命周期中可追踪性数据的CD-ROM，以便于验证和审核。

●需求的导入、编辑和查询

●定义完整的需求状态（比如部件是否导入、评审状态、声明周期阶段等）

●跟踪每个需求和部件的评审状态（评审状态转换时管理基线）

●在线评审需求和部件（可以集成配置管理系统，或使用桌面文件系统）

■需求评审和分析

■工作产品和评审

■测试和评审

将评审意见记录到可追踪性数据库；自动生成评审检查单（通过VeroStyle的帮助）以及检入检查单到配置管理中

●生成XML数据用于VeroStyle转换到报告和度量中，管理需求和工作产品报告以及从VeroTrace中产生的文档。  

●验证追踪（VoT）

VeroTrace 是一个生命周期追踪管理工具，可以产生、管理和交付支持安全关键软件确认和许可的数据。工具完成两大任务：工作产品追踪的验证（AVoT）和超链接的追踪验证（HVoT）。

VeroTrace产生一个校验数据包的CD-ROM 影像，内含超链接追踪所有的需求和工作产品。可以确保：

■工作产品的名称为RTD，匹配CD中实际相对应的文件，包含从配置管理系统中提取的基线工作产品。这就是工作产品追踪的验证（AVoT）

■所有的超链接是由VeroTrace自动生成，含有期望的目标文件。这就是超链接的追踪验证（HVoT）。

l运行平台：Windows XP/7/10

符合DO-178B/C验证要求的目标码分析工具VerOCode

VerOCode是一个不需要特殊硬件的执行跟踪分析工具。被测试的代码不需要插装（不添加记录执行状态的功能调用）。应用代码在目标计算机（例如PowerPC，V8）上执行，执行的数据图表搜集到一个宿主机上（PC/Windows或更高配置）。VerOCode使用搜集的执行数据图表与链接器符号信息和编译器产生的清单一起，可以显示出哪些指令执行了，哪些指令没有执行，以及条件指令执行过程中的条件代码状态。产生的VerOCode结果清单包含了DO-178B/C A级，最高级别的安全性要求所要求的覆盖率分析的证明。

VerOCode记录和显示被测试程序中执行的指令。对于条件指令，VerOCode显示每次指令执行时的条件代码的状态。覆盖率在机器码级获得，结果通过一个包含源代码和汇编语言扩展的程序清单来报告。 工作在交叉模式。监控和测试程序（测试控制和被测单元）在目标机上执行， 目标机通过通信口语宿主机连接。一个测试运行以后，搜集的覆盖率数据上载到宿主机来分析。

VerOCode设计为三个模块：

1) 第一个驻留在目标系统中（监控程序），搜集覆盖率数据；

2) 第二个是基于宿主机的（分析工具），实现覆盖率分析和报告；

3) 一旦覆盖率分析完成，结果文件可以通过第三个Coverage Editor来注解。这个模块帮助确认无用的代码。

●显示目标代码级的覆盖率；

●能够结合多个测试的结果，以提供累计覆盖率数据；

●通过单独搜集每个条件的结果能够获得条件判断的覆盖率（MCDC） ；

●不插装被测代码；

●能够记录覆盖率数据；

●能够形成一部分可重复的、自动化的测试和覆盖率分析脚本；

●作为认证证明数据，VerOCode 可以用作一个验证工具，其覆盖率结果可以作为认证信用。 VerOCode可以与认证材料一起提供，能够用于A级认证系统；

支持的目标平台：SPARC V8、PPC、Intel处理器。

符合DO-178B/C验证要求的控制耦合目标的验证工具VerOLink

基于需求的测试验证了软件行为是按照预期来实现的。使用结构覆盖率分析，尤其在目标码上的分析，能够证明不期望的功能已经被去掉。那么剩下来的工作就是确定和给出目标证明，每个软件函数是按照预期被调用的，由链接器产生的错误没有被发现，符合DO-178B/C的控制联合目标的要求。

VerOLink帮助满足DO-178B/C的控制目标。VerOLink验证了在链接器（linker）链接多个目标模块时产生的可执行镜像内的函数调用可以被正确分解。VerOLink检查在可执行镜像内的被调用函数的地址与函数调用时的地址是否一致，在本质上验证系统链接器产生的链接，这些链接来自单独的编译单元内的函数调用。

●VerOLink是一个满足DO-178B的控制联合目标的验证工具。控制联合要求检测集成多个分别编译的目标文件形成一个可执行映像的正确性。

●VerOLink用来完成这个最终的检查。代码集成的验证再现链接器和相关工具分别执行的过程，交叉检查集成的一致性。

●VerOLink验证当链接器组合目标模块时一个可执行映像中的函数调用已经被正确地解析了。

●VerOLink检查执行映像中的函数地址是对应于被调用的函数的起始地址的。这样就验证了通过链接器产生的分别编译的单元间函数的符号链接。

●VerOLink可以与认证材料一起提供，能够用于直到A级认证的任何认证级别的系统。

●VerOLink在Windows主机平台运行，支持PPC Target和GNU C。

符合DO-178B/C 验证要求的BC级软件覆盖率分析工具VeroSource

 VeroSource可以计算在PPC目标环境下的代码覆盖率，用于得到源代码级别的语句分支覆盖率，可以满足在适航项目中对代码进行语句分支覆盖分析的验证要求。主要应用由C语言编写的B/C类软件验证。提供DO-178B/C中B/C类软件所需的证明。

VeroSource由四个模块构成：

1) 插装器（主机上）完成对C代码的插装；

2) 监控器（目标机上）从目标机捕获并传送数据到主机；

3) 分析器（主机上）使用覆盖率信息注解列表；

4) 编辑器（主机上）是一个定制工具，可以在覆盖率不完备时编辑和标记注解列表。

插装器、分析器和编辑器组成的主机系统可以运行在一个PC电脑。插装器完成对预处理过的源码进行插装，作为分析器的输入源。 插桩后的被测程序和用来驱动被测程序的测试程序，经过一起编译链接后，下载到目标机上执行。 测试运行后，由监控器捕获的覆盖率数据上载到PC主机，分析器使用覆盖率信息注解C代码列表。 编辑器根据分析器产生的带有注解的源码XML文件，在覆盖率不完备时编辑和标记注解列表，并且产生HTML格式报告。

●支持源码级别的语句分支覆盖率分析；

●支持C代码插装；提供目标平台的测试数据捕获程序；

●支持覆盖率结果标注到代码；

●提供DO178B/C中B/C类软件所需的证明。

●提供完整的Verocel工具质量文件（Tool Qualification Documents）。

●支持PPC目标平台（PSC ARINC 653或者VxWorks 653），GNU C。

符合DO-178B/C 验证要求的A级软件覆盖率分析工具VeroSource-A

VeroSource-A是覆盖率分析工具VerOCode和VeroSource的补充，可以满足DO-178B/C A级软件指定的最严格的覆盖分析要求，即修订的条件/判定覆盖率（MC/DC）。

VeroSource-A与VeroSource一样也是由插装器、监控器、分析器、编辑器四个模块构成。

●插装器的功能

 插装器在预处理的源文件中插入以下实体：

■声明覆盖监视函数（VerOSource_D和VerOSource_C）；这些函数用于获取判定和条件的覆盖信息。

■定义覆盖数据表（VerOSource_CT）；每个源码的覆盖信息保存在这张表中。

■在合适的地方调用覆盖监控函数。

■被覆盖监控函数使用的本地变量（VerOSource_S）的定义。

■附加工具-内置信息（作为一条注释在文件的结尾）。

●监控器功能

监控器是驻目标机程序模块监测插装后测试程序的执行，在覆盖率数据表格中获取覆盖率信息。每一个源文件都有一个覆盖率表格。表格可以读取目标机监控器的信息转移到主机从而进行深入分析。用户开发的测试工具用于启动和停止监控器，转移覆盖率结果从目标机到主机。

●分析器的功能

分析器校对从目标机上带有相应源码列表的的Monitor中收集的覆盖数据，并生成带注释列表的XML文件。分析器注释信息列表，使分析的覆盖信息容易理解。结果文件中的所有判定和条件，以特定的XML属性标记并显示覆盖率。XML文件可在编辑器中打开。

分析器需要有预处理过的C源码文件、插装的或注释的C源码文件，以及覆盖数据表文件。如果输入文件已被注释或相应的源码文件有两个或多个覆盖数据表，该工具会合并覆盖数据。

●编辑器的功能

编辑器接收分析器产生的XML文件，显示带有注释的列表。用户可以查看源代码和覆盖注释。如果必要，可能在带有覆盖说明的列表文件中添加注释。编辑器不会更改或不允许更改列表，源代码和覆盖数据。

●支持PPC目标平台（PSC ARINC 653或者VxWorks 653），GNU C。

最差堆栈使用情况分析工具VeroStack

VeroStack可以计算代码在最差条件下使用堆栈的情况，支持Ada、C、C++、以及汇编语言。可以在主机上运行，直接分析应用的执行镜像。可以分析系统和应用程序的堆栈使用，支持DO-178B/C中的A级软件验证。

在使用 VeroStack 编辑器标识出应用入口以及应用中代表任务和进程的程序，它们都有自己的堆栈， VeroStack 分析出程序的调用关系，通过这些信息， VeroStack 计算应用中每个堆栈在最差条件下的大小，并产生可以作为验证数据的报告。

VeroStack由三部分构成：

1) Image Processor：分析被测软件执行映像，定位所有符号和调用。

2) Editor：允许用户完善缺少的堆栈分析数据（如间接调用，未知堆栈结构等）。

3) Calculator：总结和呈现堆栈分析结果。

●基于目标码分析。

●支持C、C++、Ada和汇编语言的分析。

●VeroStack 编辑器是用来解析间接调用的。通过这些信息， VeroStack 计算应用中每个堆栈在最差条件下的大小，并产生可以作为验证数据的报告。

■直接和间接的递归调用

■通过指针的调用

■间接调用（比如在C++中通过分配表dispatch tables进行的调用）

●在Windows主机平台运行，支持PPC Target。