-
![诚邀 - 迪捷软件邀您参与2023年航电国际论坛]()
诚邀 - 迪捷软件邀您参与2023年航电国际论坛
论坛背景近年来，伴随着新兴学科不断涌现，航空业也发生了以绿色、智能为特征的群体性技术革命，航空科技创新链条更加灵巧，技术更新和成果转化更加快捷，航空产品迎来了批量化生产、规模化运营、系列化发展的新阶段，升级换代不断加快。2023年（第十二届）飞机航空电子国际论坛将于6月28日至29日在上海举办。论坛自2012年以来，已经成功举办了11届，并已发展为亚太地区业内最受欢迎、规模最大的航电专业活动。本届
2023-06-20 digiproto
-
![喜报丨迪捷软件荣获浙江省专精特新荣誉称号]()
喜报丨迪捷软件荣获浙江省专精特新荣誉称号
近日，根据工业和信息化部《优质中小企业梯度培育管理暂行办法》（工信部企业〔2022〕63号）和《浙江省经济和信息化厅关于印发浙江省优质中小企业梯度培育管理实施细则（暂行）的通知》（浙经信企业〔2022〕197号）等要求，2023年度第一批浙江省专精特新中小企业名单正式公示，迪捷软件成功获评2023年度第一批浙江省“专精特新”中小企业。专精特新中小企业实现专业化、精细化、特色化发展，创新能力强，质量
2023-05-31 digiproto
-
![通过模糊测试寻找车载蓝牙的安全漏洞]()
通过模糊测试寻找车载蓝牙的安全漏洞
车载蓝牙的安全威胁主要来自蓝牙漏洞攻击、蓝牙配对窃听、DoS攻击等，可能导致目标计算机或网络无法提供正常的服务或资源访问。车载蓝牙安全漏洞不容忽视。
2023-05-15 digiproto
-
![浅谈CompCert：经过形式化验证的可信编译器]()
浅谈CompCert：经过形式化验证的可信编译器
对编译器的正确性进行验证的诸多手段中，最为严格的莫过于采用形式化方法。点开原文查看经过形式化验证的可信编译器CompCert。
2023-05-15 digiproto
-
![L2C中Lustre语义的环境定义]()
L2C中Lustre语义的环境定义
随着计算机技术越来越多地应用于航空航天、核电、高速铁路等安全关键系统(SCS，Safety-Critical System)，对计算机技术的安全性要求也越来越高。安全关键系统中的丝毫错误都可能引发巨大的灾难。如何为安全关键系统构造一个基础的安全软件环境是需要面对的首要问题，尤其是对操作系统、编译器等基础软件。
2023-05-15 digiproto
-
![L2C中CtempGen层语义保持证明中环境匹配的定义]()
L2C中CtempGen层语义保持证明中环境匹配的定义
ModelCoder是一款由迪捷软件自主研发，支持多种嵌入式系统建模并可以自动生成高安全可靠的C代码的软件设计和开发工具。ModelCoder支持同步数据流以及状态机等嵌入式模型，其从模型生成代码的过程经过了形式化验证，以保证生成过程的正确无误性，能够用于飞行控制系统，航空电子系统，核电的DCS等多个安全关键领域的嵌入式软件的设计和开发。
2023-05-15 digiproto
-
![初探形式化方法基本原理]()
初探形式化方法基本原理
1.形式化方法基本概念形式化方法是基于严格的数学基础，通过采用数学逻辑证明来对计算机软硬件系统进行建模、规约、分析、推理和验证，是用于保证计算机软硬件系统正确性以及安全性的一种重要方法。形式化方法使用数学及逻辑证明的手段对计算机系统进行建模、规约、分析、推理，其主要涵盖以下几个研究方向：定理证明、形式模型、形式语义与形式建模、形式规约、形式验证技术。下面以高可信工业领域实际应用中最广泛的形式化规格
2022-08-01 digiproto
-
![「迪捷软件」喜获Pre-A轮千万级融资，硬核科技打造安全关键领域嵌入式数字仿真平台]()
「迪捷软件」喜获Pre-A轮千万级融资，硬核科技打造安全关键领域嵌入式数字仿真平台
不积跬步，无以至千里。面对如此巨大的市场需求，潜心耕耘近20年的迪捷团队抓住机遇，厚积薄发，于2019年成立浙江迪捷软件科技有限公司，推出了基于模型的系统工程（MBSE）的自主研发产品。
2022-05-09 digiproto
-
助力中国高端装备制造业的腾飞
-
-
contact@digiproto.com
-
0575-88361699
-
19957518153（销售）/ 13260299730（合作）/ 13501153049
-
