Verified Systems RT-Tester 介绍

RT-Tester 是德国 Verified Systems International GmbH 提供的一个嵌入式测试自动化平台，主要面向实时和安全关键软件的测试执行和评估。

核心定位

• 动态测试工具
• 支持：单元测试、软件集成测试、硬件/软件集成测试、系统测试
• 目标：自动生成测试、执行测试、实时评估测试结果

主要特点

• 一个工具覆盖所有测试层级
  • 同一套工具可用于 unit、SW integration、HW/SW integration 以及 system tests
• 强大的存根生成器
  • 自动生成子函数/方法存根
  • 记录调用参数
  • 可模拟正常返回、异常行为，便于稳健性测试
• 模型驱动测试支持
  • 与多种规范形式集成：UML 2.0、领域专用语言（DSL）、CSP 等
  • 适用于模型基础测试工作流
• 接口抽象机制
  • 使用 channel（消息传递）和 vector（分布式共享变量）机制抽象系统与被测对象接口
  • 适合 SW、HW/SW 和系统层集成测试
• 高性能多线程运行时
  • 自带运行时环境
  • 基于 Windows/Linux 轻量级进程（LWP）
  • 低上下文切换开销
• 硬实时能力
  • 在 Linux 多核/多 CPU 上可选装硬实时内核补丁
  • 可把部分 CPU 独占给 RT-Tester 线程
  • 实现微秒级调度精度
• 分布式测试与集群仿真
  • 测试刺激器、测试判定器、仿真可分布到多个 CPU/节点
  • 支持高速互连（如 Infiniband、千兆以太网）
• 工具资格认证
  • 宣称符合 RTCA DO-178B/C 的工具资格要求
• 支持平台
  • Linux：SUSE、openSUSE、CentOS/RHEL、Ubuntu
  • Windows：XP SP3、7、10、11

AbsInt 的产品定位

AbsInt 不是以测试执行为主，而是以静态分析和形式化验证为核心，主要用于确保嵌入式C/C++代码的安全性、时间行为和栈行为。

代表产品

• Astrée
  • 静态分析器
  • 检测运行时错误、缓冲区溢出、除零、空指针、数据竞争
• aiT WCET Analyzer
  • 最坏情况执行时间分析
  • 计算时间上界，支持缓存、流水线等复杂硬件
• StackAnalyzer
  • 静态栈使用分析
  • 计算最坏栈深度，避免栈溢出
• CompCert
  • 形式化验证的 C 编译器
  • 保证编译过程正确
• RuleChecker
  • 编码标准检查
  • MISRA、AUTOSAR 等
• TimeWeaver / TimingProfiler
  • 结合静态和动态信息进行时间分析
• ValueAnalyzer
  • 寄存器/内存状态分析

关键特性

• “零假阴性”
  • 绝不漏报真实错误
• 最小化假阳性
  • 尽量减少误报，降低人工审查负担
• 形式化、声音分析
  • 基于抽象解释、数学证明
• 适用于认证
  • ISO 26262、DO-178B/C、IEC-61508、EN-50128 支持

RT-Tester 和 AbsInt 的对比

什么时候选 RT-Tester，什么时候选 AbsInt

选择 RT-Tester 的场景

• 需要对嵌入式软件进行自动化测试
• 需要覆盖 HW/SW 集成或系统级测试
• 需要动态验证接口和运行时行为
• 需要硬实时时间精度和多核/分布式测试
• 需要测试工具具备 DO-178B/C 资格

选择 AbsInt 的场景

• 需要证明代码不会出现运行时错误
• 需要计算最坏情况执行时间（WCET）
• 需要进行栈使用分析、避免栈溢出
• 需要用可信编译器（CompCert）减少编译引入的错误
• 需要静态验证以支持安全标准认证

结论

• RT-Tester 是一个面向嵌入式实时系统的测试自动化平台，强调测试执行、仿真、实时测试和系统集成测试。
• AbsInt 是一套面向安全关键嵌入式软件的静态验证工具链，强调错误证明、时间分析、栈分析和形式化编译。

这两个产品更多是“互补关系”而不是“同类替代”关系。在一个完整的安全开发流程中，通常可以同时使用：

• AbsInt 做静态验证与形式证明
• RT-Tester 做动态测试与运行时验证