Name: SMAVE Model Suite
Brand: SMAVE

SMAVE Model Suite
量身定制、国产化自主可控

面向高安全嵌入式软件的模型设计、仿真、验证与代码自动生成一体化环境，开发环境与核心组件 TCG 均已通过 TÜV 南德五大功能安全标准最高等级（T3）认证，拥有完整自主知识产权。

优势

最高等级安全认证

开发环境与核心 TCG 组件通过 TÜV 南德 T3 认证，覆盖 ISO 26262、EN 50128、EN 50716、IEC 61508、IEC 60880 五项标准。

完全自主可控

实现模型定义、语义解析及代码生成全栈自主研发，适配国产软硬件平台，构建完全自主可控的核心工具链。

无缝项目迁移

原生支持旧有工程项目无缝导入，保留原项目结构与功能逻辑，实现资产平滑过渡与持续开发，降低迁移成本与重构风险。

形式化验证保障

依托形式化推理机制，对模型关键属性进行精确证明与系统化校验，属性不满足时自动生成反例并精准定位潜在缺陷，助力构建高可信工程化研发与质量保障体系。

自动化代码生成

自研 TCG 模块可基于模型自动生成高安全 C/FPGA 代码，具备确定性、可读性与可追溯性，显著降低人工编码风险。

全生命周期覆盖

覆盖建模、验证、生成、部署与文档生成全生命周期，打通工程开发闭环，提升研发效率、系统一致性与交付可信度。

功能点

混合建模

模型检查

代码生成

模型仿真

报告生成

AI 辅助建模

形式化验证

堆栈分析

时序分析

覆盖率分析

全流程追溯

数据流、控制流混合建模

支持数据流与控制流混合建模。覆盖逻辑运算、算术运算、比较运算、数组操作、时钟控制等，支持状态机、条件块、局部变量、信号、断言等高级建模要素。自动布局功能根据模型复杂度自适应调整，优化操作符尺寸与连线排布，确保图表结构规整、层次分明。

1/11

静态一致性模型检查

支持命名空间分析、后向命名空间分析、类型分析、时钟分析、因果分析、初始化分析 6 种静态语义检查方法。支持错误跳转链接和高亮提示，精确定位问题节点与连线，从设计源头保障软件正确性。

2/11

代码生成

内置自研 TCG（Trustworthy Code Generator）模块，支持基于模型自动生成符合 MISRA-C 规范的高质量 C 代码及 FPGA 代码，实现代码注释可继承、代码形态可配置，显著提升开发效率，增强代码一致性与工程落地能力。

3/11

模型仿真

提供一体化可视化模型仿真与调试环境，支持输入值设置、场景化配置与快速验证，兼容 FMU 仿真模式，满足多类型模型仿真需求。支持变量分组查看、实时数值展示和变量追踪分析，并提供单步、连续、断点设置等 8 种仿真操作模式，支持测试用例复用，有效提升问题定位与回归验证效率。

4/11

报告生成

基于模型设计自动生成 HTML 格式成果文档，完整呈现模型结构、操作符说明、数据流关系、接口定义及变量类型等信息，并支持详细设计、需求追溯、架构追溯和完整追溯等多类报告按样式定制输出，显著提升文档生成效率与工程可追溯性。

5/11

AI 驱动的智能建模辅助

集成 AI 辅助建模能力，支持自然语言描述到控制逻辑模型的智能转换，AI 引擎可根据模型上下文智能推荐操作符组合与建模模式，降低建模门槛、提升设计效率。支持 AI 驱动的模型质量分析，自动识别潜在设计缺陷并提供优化建议。

6/11

形式化验证

通过数学方法确保模型满足特定属性并符合需求规范，验证整数除零、溢出、越界及浮点异常等问题，无需编写测试用例和代码插装，支持反例生成、零误报优化及高级配置，并自动输出验证分析报告与反例场景。

7/11

堆栈分析

提供堆栈分析器和优化器，围绕函数调用上下文数量、函数自身栈使用量及函数与父调用链累计栈使用量等核心指标，构建多维度、可量化的运行栈评估体系，能够深入洞察函数调用关系与栈资源分布特征，精准识别高风险调用路径与潜在资源瓶颈，自动生成专业分析报告，为软件性能优化、架构设计改进及运行安全保障提供有力支撑。

8/11

时序分析

提供时序分析器和优化器，围绕函数调用上下文、函数自身 WCET 的求和、最大值、平均值，以及含子调用累计最坏执行时间等核心指标，构建全链路时延评估体系，精准识别关键路径与实时性风险，为优化调度设计与系统稳定运行提供专业支撑。

9/11

覆盖率分析

覆盖率分析支持模型级与代码级验证，面向覆盖准则构建可追踪覆盖点体系，贯通覆盖观测、结果合并、缺口诊断与合理性说明全流程，为未覆盖点提供合规依据，支撑验证充分性分析及认证级测试闭环。

10/11