典型用户

机载嵌入式软件形式化方法审定技术研究设备

其它通用分析品牌：DR 型号：测试向量生成/自动测试/集成测试

仪器名称：

英文名称：

T-VEC/LDRAToolSuit/RTinsight

所属分类：

其他仪器 > 其他 > 其他

学科领域：

航空、航天科学技术

主要技术指标：

支持：用形式化语言描述需求；用图形化方法描述需求；形式化验证；测试用例自动生成；测试驱动自动生成；自动度量与测试报告生成。在民航机载软件领域广泛应用；不仅可以揭示逻辑组合类错误，同时可以揭示计算类错误；与软件自动测试工具完全兼容。软件测试执行功能组件支持：编码规则检查、数据流分析、软件度量分析、单元测试、集成测试驱动与桩模块自动生成、代码覆盖率分析（支持单元级、集成级与系统级）；能够支持5人同时开展测试工作；与形式化方法测试向量生成器完全兼容。软件运行时错误分析组件支持采用形式化静态分析方法验证C语言动态运行错误。包括：企图读未初始的变量；对空指针和越界指针的应用；对超界数组的访问；非法类型转换；非法的算术运算（例，除零错误）；整数和浮点数的上溢出／下溢出；不可到达的代码；分析的结果经过推导证明，如果分析没有发现问题，则能够保证不存在问题，可以直接作为适航证据。

主要功能：

需求形式化建模及分析；测试向量自动生成； C语言代码运行错误静态分析；采用静态分析方法进行堆栈分析；采用静态分析方法进行WCET分析；代码静态分析及代码规则检查测试执行结构覆盖率分析（语句、分支/判定、MC/DC）支持性能分析，监控每个模块最大/最小执行时间、执行次数及累加执行时间；支持变量监控，实时监控被测目标系统变量执行；支持堆栈监控。