01

ModelCoder的介绍


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


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


02

ModelCoder的原理


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


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


ModelCoder的翻译过程如下:


图片关键词

▲图1:ModelCoder翻译流程简图



03

ModelCoder的功能


ModelCoder的功能分为三个部分:


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

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

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


图片关键词

▲图2:ModelCoder的图形化前端


图片关键词

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



04

ModelCoder支持的算法模型


支持模型支持的模型列表
参数模型输入参数、输出参数、常量参数、类型参数
数学计算模型加法模型、减法模型、乘法模型、除法模型、取负模型、取模模型
比较模型大于模型、大于等于模型、小于模型、小于等于模型、等于模型、不等于模型
逻辑判断模型逻辑与模型、逻辑或模型、逻辑异或模型、逻辑非模型
时序模型Init模型、Previous模型、FollwedBy模型
选择模型IfThenElse模型
数组模型DataArray模型、DynamicProjection模型、Projection模型、ScalarToVector模型、Slice模型
结构体模型DataStructure模型、Flatten模型、Make模型、Project模型


05

ModelCoder的建模规则


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

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

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

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

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


首页
产品
新闻
联系