wecom
qy
选择丰蕾

关于

竞争优势

见解主张

产品

工业软件

自动化 AI 嵌入式开发

控制器软件

联系我们
简介
优势
功能点
核心能力
使用场景
行业应用
联系我们

SMAVE Code Analyzer
前置风险防控

SMAVE Code Analyzer 面向嵌入式 C 软件，提供缺陷检查、代码度量、MISRA C 规范检查及基于需求的形式化验证。平台可扫描并定位风险代码，将需求规范、ACSL 验证规范与源码关联，帮助发现实现偏差，提升代码安全性、可靠性和可维护性。

优势

icon
缺陷覆盖全面

覆盖除零、移位越界、指针越界、非法内存访问、类型转换异常和变量未初始化等常见问题，帮助开发阶段尽早发现潜在运行风险。
icon
定位结果清晰

检查结果可标记具体文件、函数和代码位置，便于研发人员快速复核问题成因、修正缺陷并开展回归检查，减少人工排查成本。
icon
质量度量完整

统计方法调用、程序退出点、条件分支、指针解引用、函数声明、代码行数和圈复杂度，为质量评估、模块拆分和代码重构提供量化依据。
icon
规范检查自动

依据 MISRA C 编码标准自动扫描规则违规，覆盖类型转换、变量使用、控制结构、函数参数、指针数组、动态内存及宏定义等检查。
icon
需求验证闭环

支持建立功能需求和验证规则，将自然语言需求、ACSL 验证规范与目标源码关联，在源码层面判断实现是否满足预期功能。
icon
结果便于追溯

验证结果明确显示通过或失败，并保留需求、规范和代码之间的关联关系，便于问题定位、整改复核、版本回归和项目质量资料整理。

功能点

缺陷检查
度量分析
规范检查
功能验证
多类型代码缺陷检查

多类型代码缺陷检查

平台可对嵌入式 C 代码开展静态缺陷检查，覆盖除零、左移与右移越界、指针越界、浮点数转整数、非法内存访问、局部变量和指针未初始化、常量表达式异常等问题，并定位到具体代码位置，便于快速复核和修复。

1/4

关键质量指标度量

关键质量指标度量

平台可统计方法调用、程序退出点、if 语句、goto 语句、指针解引用、声明函数和代码行数等指标，并计算函数圈复杂度。通过文件与函数层面的量化结果，帮助识别复杂度过高、规模过大或结构不合理的代码模块。

2/4

MISRA C 规范检查

MISRA C 规范检查

平台依据 MISRA C 编码标准自动扫描用户代码，检查不可移植或未定义行为、类型转换、变量声明与使用、运算符优先级、控制结构、函数参数、指针与数组边界、动态内存分配、宏定义及头文件保护等规则。

3/4

需求驱动形式化验证

需求驱动形式化验证

平台支持创建功能需求及需求描述，为每条需求配置验证标准和方法。用户可在源码中使用 ACSL 语言建立验证规范，将验证规范与需求规范绑定，再选择目标需求执行形式化验证，并查看通过或失败结果。

4/4

核心能力

嵌入式代码静态分析

平台面向嵌入式 C 代码提供自动化静态分析，识别除零、移位越界、指针越界、非法内存访问、类型转换异常、变量未初始化和常量表达式问题，并将结果定位到具体代码位置，帮助研发人员在开发早期发现潜在缺陷和未定义行为。

嵌入式代码静态分析
代码质量量化评估

平台对方法调用、退出点、条件分支、goto 语句、指针解引用、函数声明、代码行数和圈复杂度进行统计分析，形成文件级与函数级量化结果。研发人员可据此识别复杂函数、冗余结构和规模过大的模块，为代码评审、拆分和重构提供依据。

代码质量量化评估
安全编码合规审查

平台依据 MISRA C 规则自动检查不可移植行为、类型转换、变量使用、运算符优先级、控制结构、函数参数、指针数组、动态内存、宏定义和头文件保护等问题，并标记违规代码位置，辅助安全关键软件开展规范符合性审查和整改复核。

安全编码合规审查
需求到源码闭环验证

平台支持建立功能需求、自然语言描述和 ACSL 验证规范，并将需求规范、验证规范与目标源码关联。用户可按需求发起形式化验证，查看通过或失败结论，及时发现代码实现与功能需求之间的偏差，形成从需求定义到源码验证的闭环。

需求到源码闭环验证

使用场景

img

嵌入式软件代码质量验证

开发阶段缺陷排查

在编码与联调阶段自动扫描越界、非法内存访问、未初始化变量和异常类型转换等问题，定位风险代码位置，帮助问题在进入系统测试前完成修复。

代码评审量化分析

在代码评审和版本检查时统计函数调用、分支语句、代码行数和圈复杂度，识别复杂度过高或规模过大的模块，为拆分、优化和重构提供量化参考。

安全编码规范审查

针对嵌入式和安全关键软件执行 MISRA C 规则检查，识别类型使用、控制结构、指针数组、动态内存、宏定义和头文件等违规项，为代码整改提供依据。

需求功能形式化验证

为项目功能需求建立需求规范，使用 ACSL 配置源码验证规则并与对应需求关联，通过形式化验证确认代码实现是否满足需求，并输出通过或失败结果。

行业应用

航空航天
核电领域
汽车电子
轨道交通
航空航天

航空航天

面向飞行控制系统、航电系统和任务软件，支持对嵌入式 C 代码开展静态缺陷扫描、质量度量和 MISRA C 规范审查，提前发现内存访问、指针使用、类型转换和复杂分支逻辑风险。结合需求规范与 ACSL 验证规范关联，可对关键控制算法开展源码级形式化验证，支撑代码评审、适航审查资料准备和版本基线交付。

1/4

核电领域

核电领域

面向核电站保护系统、安全级仪控和监测软件，支持对高可靠 C 代码开展缺陷识别、复杂度评估和编码规范符合性检查，重点关注指针越界、非法内存访问、类型转换和异常分支处理等问题。通过将安全需求映射为源码验证规则，可为独立验证、缺陷闭环整改和质量证据归档提供可追溯依据。

2/4

汽车电子

汽车电子

面向车载 ECU、底盘控制、动力控制和智能驾驶相关软件，支持在持续集成和版本迭代中发现除零、移位越界、变量未初始化、非法内存访问等常见缺陷，并输出函数调用、代码规模和圈复杂度等质量指标。配合 MISRA C 规则检查和基于需求的源码验证，帮助团队在量产交付前确认关键控制功能实现质量。

3/4

轨道交通

轨道交通

面向列车运行控制系统、信号联锁系统和车载控制软件，支持对交付版本中的 C 代码进行静态分析、度量统计和编码规范审查，聚焦数组访问、指针越界、类型转换、边界条件和复杂控制结构等可靠性风险。通过为关键联锁逻辑和安全约束建立源码验证规则，可提升问题定位、回归复核和版本发布评审效率。

4/4

message

获取专业解决方案

联系解决方案专家，进行详细沟通