软件说明
ModelCoder是一个可以从模型自动生成代码的设计工具，能够自动从同步数据流语言Lustre生成C代码。ModelCoder的优势在于对模型到C语言的转换过程进行了形式化验证，从而严格地证明了模型转换过程的可靠性。ModelCoder可以与经过形式化验证的CompCert C编译器对接，从而实现从模型到汇编语言的可信编译。这是SCADE等同类产品所不具备的，SCADE只是对模型进行了形式化验证，但因缺少对转换过程的验证，从而无法保证模型和生成代码的一致性。
ModelCoder包含图形化建模模块、代码生成模块以及代码安全性检查模块等。用户可以通过友好易用的图形界面根据需求进行建模，最后生成可运行的代码。此外，ModelCoder可与迪捷软件的SkyEye天目全数字实时仿真软件相结合，将自动生成代码经过编译后的二进制文件直接运行在虚拟硬件上，进行进一步的测试验证。ModelCoder具有高可靠性和高安全性，这些特性促成了它在航空、航天、高铁、核电等关键领域的嵌入式软件系统设计中的应用。目前，ModelCoder已在国内相关单位的生产环境中得到应用，未来必将发挥更大的作用。
ModelCoder的功能分为三个部分：
-
图形化的软件建模：使用直观的图形符号构建数据流模型；
-
仿真测试：基于自动生成的C代码仿真各模块的运行过程，可在早期发现设计缺陷；
-
自动代码生成：将模型语言经过形式化方法自动生成可靠的C代码。
ModelCoder的建模规则
-
特定的运算符用来支持特定的数据结构，例如Map用来支持对Array的操作；
-
控制模块的复杂度，尽量减少子模块的调用，生成的代码每调用一次函数，就会产生函数传参的开销，此时如果上层有较多循环，则传参的代价较高；
-
检查重复模块，尽量归并重复项，形成基础库；
-
对门电路，建模前应先优化，可降低模型的复杂度；
-
控制局部变量数量，减少不必要的局部变量，以防产生额外的堆栈创建和销毁的开销。