在安全关键领域，基于模型的软件工程或者软件开发已逐渐进入了我国的装备研制过程中。使用SimuLink或者SCADE等嵌入式软件建模工具，对算法或控制逻辑进行可视化建模，然后生成高可靠的二进制代码逐渐成为了安全关键领域的主流软件开发方式。

由我司自主开发的ModelCoder是一款支持多种嵌入式系统建模并可以自动生成高安全可靠的C代码的软件设计和开发工具。ModelCoder支持同步数据流以及状态机等嵌入式模型，其从模型生成代码的过程经过了形式化验证，以保证生成过程的正确无误性，能够用于飞机的飞控，飞机的航电，核电的DCS等多个安全关键领域的嵌入式软件的设计和开发。

代码生成工具是编译器的一种，是把模型语言翻译成C语言的编译器。代码生成工具广泛应用于我国的航空、轨交和核电等安全关键领域。

保证代码生成工具的生成过程的安全可靠性是安全关键领域必须要面对的课题。ModelCoder采用了最严格的形式化技术，用定理证明的方式对模型到代码的生成过程进行了严格的数学证明。和同类软件SCADE的KCG相比，KCG只是采用了模型检测技术对模型本身进行了证明，而ModelCoder无疑在技术途径上更为可靠。

ModelCoder的翻译过程如下：

▲图1：ModelCoder翻译流程简图

ModelCoder的功能分为三个部分：

1. 图形化的软件建模：使用直观的图形符号构建数据流模型；

2. 仿真测试：基于自动生成的C代码仿真各模块的运行过程，可在早期发现设计缺陷；

3. 自动代码生成：将模型语言经过形式化方法自动生成可靠的C代码。

▲图2：ModelCoder的图形化前端

▲图3：ModelCoder的仿真运行测试模块

1. 特定的运算符用来支持特定的数据结构，例如Map用来支持对Array的操作；

2. 控制模块的复杂度，尽量减少子模块的调用，生成的代码每调用一次函数，就会产生函数传参的开销，此时如果上层有较多循环，则传参的代价较高；

3. 检查重复模块，尽量归并重复项，形成基础库；

4. 对门电路，建模前应先优化，可降低模型的复杂度；

5. 控制局部变量数量，减少不必要的局部变量，以防产生额外的堆栈创建和销毁的开销。