SMAVE MODEL SUITE
模型化嵌入式软件开发环境
SMAVE MODEL SUITE
为安全/任务关键应用量身定制、国产化自主可控的基于模型的设计、仿真、验证与代码自动生成环境
模型化嵌入式软件开发环境
SMAVE Model Suite为用户提供关键嵌入式软件领域的基于模型的开发环境，包括基于模型的设计、自动代码生成、仿真、模型验证等功能。通过简化关键控制应用程序设计、验证、代码生成、文档生成的过程，极大地降低了项目开发成本，同时增加了项目的正确性与可靠性。
模型化嵌入式软件开发环境
采用高安全模型化建模、分析、代码生成与验证技术，实现可靠系统的高效开发。
基于模型的软件开发方法
■ 以严格的形式化语言为理论基础
■ 强大的模型表述能力：数据流+状态机
■ 模型完整性、确定性保证：强类型语言+静态一致性检查
■ 模型验证：基于形式化方法的模型检查技术
■ 高质量和高安全的代码生成器
■ 图形化模型仿真与调试
可以通过不同类型的操作符的组合操作构建丰富的模型：
■ 逻辑操作符(Logical)
■ 高阶操作符(Higher Order)
■ 数学运算操作符(Mathematical)
■ 比较操作符(Comparison)
■ 结构/数组操作符(Structure/Array)
■ 时间操作符(Time)
■ 选择操作符(Choice)
■ 条件块操作符(Conditional Block Items)
■ 位操作符(Bitwise)
模型设计
模型验证
模型检查
静态一致性检查
包括命名空间分析、类型分析、时钟分析、因果关系分析等多种分析检查。如果关系分析可用于验证同一周期是否存在数据流的值依赖自身的值。
模型验证
模型检查技术
■ SMT求解技术 ■ 下推自动机
有效提高嵌入式系统可靠性
■ 基于模型的开发方法广泛的应用在航空航天、轨道交通、武器装备等安全攸关的领域
■ 增强模型设计的正确性和安全性
仿真调试
■ 图形化模型仿真与调试 ■ 变量追踪图
高质量、高安全代码自动生成
高质量和高安全
基于严格的语言理论，保证代码的运行与仿真结果完全一致
可读性强
生成代码具有较强的可读性，支持针对代码的修改
代码可移植
生成的代码具有可移植性
平台无关
生成代码与平台无关
功能可定制
可根据用户需求，生成对应格式、对应规则的任意语言代码
平台支持
支持包括自主可控处理器在内的多种CPU
■ Intel & AMD 32位 & 64位 x86处理器（包括海光、兆芯等国产品牌）
■ ARM A8、A9、A53等32位及64位处理器（包括鲲鹏、飞腾、Rockchip、全志等国产品牌）
■ MIPS处理器（包括 龙芯 等国产品牌）
■ 可进行多种处理器时间、中断和内存的分析、验证与仿真
支持包括自主可控处理器在内的多种CPU
■ 可生成与国内自主可控操作系统适配的应用代码
■ 支持与Linux、VxWorks、QNX等国外主流操作系统集成
■ 支持生成状态机驱动的零OS代码（无OS，系统内置状态机方式实现）
SMAVE 产品优势
提升效率
■ 图形化设计，提高开发效率
■ 自动生成高安全可直接运行代码
■ 模块化组件开发，提高软件重用性
提高质量
■ 基于严格的形式化语言建模，软件具备确定性
■ 静态分析检查，提前发现设计缺陷
■ 模型检查，验证需求满足性
自主可控
■ 自主研发、拥有自主知识产权
■ 支持国产操作系统
■ 支持国产处理器硬件
行业应用
