形式化验证-媒体中心-国产MBSE工业软件,迪捷软件,ModelCoder,SkyEye,SysModeler

ModelCoder中的代数环问题

2020年5月23日，美国商务部宣布，将共计33家中国公司和机构列入实体清单，哈工大、哈工程被禁用“工科神器”Matlab，而Simulink是Matlab软件的扩展，它是一个实现动态系统建模和仿真的软件。Matlab在国内知名院校和关键领域研究院所的禁用，给在国内坐了多年冷板凳，从事基础软件研究和产业化的我们，带来了机遇。

2021-12-30 digiproto

L2C中CtempGen层语义保持证明中环境匹配的定义

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

2021-12-20 digiproto

设计模式六大原则你都知道吗？

单一职责原则的核心是功能单一化，功能单一化后每个模块只受该功能的影响，不会出现其他功能的改变导致必须修改该模块。比方说登录模块和用户管理模块，如果合在一起，会导致如果需要增加一个临时登录的功能必然会影响用户管理模块，至少上线的时候用户管理模块也是断掉的。

2021-12-14 digiproto

浅谈状态机

在工业生产中，常常会使用到建模软件，而建模的目的就是为了在制造的前期进行验证和试错，以确保制造出来的东西能够很好的使用。而在建模仿真的领域中，状态机又是逃不开的一个话题。

2021-12-13 digiproto

基于常微分方程初值问题的ModelCoder固定步长求解器分析

形式化验证的代码生成工具ModelCoder由迪捷软件自主开发，是一款支持多种嵌入式系统建模并可以自动生成高安全可靠的C代码的软件设计和开发工具。ModelCoder支持同步数据流以及状态机等嵌入式模型，其从模型生成代码的过程经过了形式化验证，以保证生成过程的正确无误性，能够用于飞行控制系统，航空电子系统，核电的DCS等多个安全关键领域的嵌入式软件的设计和开发。对标产品有国外ANSYS公司的SCADE或者MathWorks公司的MATLAB/Simulink。

2021-12-10 digiproto

L2C中Lustre语义的环境定义

随着计算机技术越来越多地应用于航空航天、核电、高速铁路等安全关键系统(SCS，Safety-Critical System)，对计算机技术的安全性要求也越来越高。安全关键系统中的丝毫错误都可能引发巨大的灾难。如何为安全关键系统构造一个基础的安全软件环境是需要面对的首要问题，尤其是对操作系统、编译器等基础软件。

2021-11-05 digiproto

编译器前端概述与可信编译器

Java程序员应该会非常熟悉Spring，在Spring框架中对注解的支持和字节码动态生成都属于编译技术；前端程序员通常会使用Babel这个工具，主要是为了将ES6语法编写的代码转换为做向后兼容的JS语法...

2021-10-25 digiproto

初识CPS方法的连续动态建模

信息物理融合系统（CPS）是对计算进程与物理进程进行集成所形成的综合系统，其行为由系统的信息部分及物理部分共同定义。嵌入式系统中的计算机与网络监测并控制物理进程，且在通常情况下这些物理进程与计算进程在反馈环路中相互影响。

2021-10-25 digiproto

产品与解决方案

媒体中心

人才战略

关于迪捷