• 喜报|迪捷软件“ModelCoder 建模及形式化验证代码生成软件”荣登浙江省首版次产品目录

    近日,浙江省经济和信息化厅公布《2023年浙江省首版次软件产品应用推广指导目录》,浙江迪捷软件科技有限公司的“ModelCoder 建模及形式化验证代码生成软件”经过多轮审核及专家评定被纳入目录。

    2023-12-22 digiproto

  • ModelCoder状态机中的State逻辑

    ModelCoder可以进行状态机的搭建以及仿真,其支持的状态机是通过在Mealy和Moore有限状态机的基础上进行扩展来实现的。本文主要讲解状态机中状态(State)的部分逻辑。

    2023-05-15 digiproto

  • 浅谈CompCert:经过形式化验证的可信编译器

    对编译器的正确性进行验证的诸多手段中,最为严格的莫过于采用形式化方法。点开原文查看经过形式化验证的可信编译器CompCert‍。

    2023-05-15 digiproto

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

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

    2023-05-15 digiproto

  • L2C中Lustre语义的环境定义

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

    2023-05-15 digiproto

  • 浅谈状态机

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

    2023-05-15 digiproto

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

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

    2023-05-15 digiproto

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

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

    2023-05-15 digiproto

上一页1234下一页 转至第
首页
产品
新闻
联系