初探形式化方法基本原理

1.形式化方法基本概念形式化方法是基于严格的数学基础，通过采用数学逻辑证明来对计算机软硬件系统进行建模、规约、分析、推理和验证，是用于保证计算机软硬件系统正确性以及安全性的一种重要方法。形式化方法使用数学及逻辑证明的手段对计算机系统进行建模、规约、分析、推理，其主要涵盖以下几个研究方向：定理证明、形式模型、形式语义与形式建模、形式规约、形式验证技术。下面以高可信工业领域实际应用中最广泛的形式化规格

2022-08-01 digiproto 2099

ModelCoder状态机：对柴油机工况判断策略进行建模

1.柴油机ECU简介柴油机是用柴油作燃料的内燃机，属于压缩点火式发动机。柴油机ECU（Electronic Control Unit，电子控制单元）的主要功能有：接受来自柴油机上的各个传感器信号；进行工况判断；根据开发人员事先编写的控制策略与标定存储的各类MAP（汽车工程上常用的实验数据图），计算判断在当前工况下的所需的喷油量、喷油正时与喷射压力等控制参数；通过功率驱动模块控制执行器输出。柴油机E

2022-07-29 digiproto 695

SAFERTOS在医疗设备中的应用

SAFERTOS为开发人员提供响应迅速、稳健、确定性的嵌入式实时操作系统 (RTOS)。它包含开发医疗设备所需的功能，并且提供设计历史文件(DHF)，为医疗设备集成SAFERTOS提供满足认证所需的文档。

2022-07-18 digiproto 681

SkyEye Q&A ——第二期

Q1：什么是车载ECU？A1：ECU（Electronic Control Unit）电子控制单元，又称“车载电脑”等。它和普通的电脑一样，由微控制器（MCU，Microcontroller Unit）、存储器（ROM，Read-Only Memory）、RAM（Random Access Memory，随机存取存储器）、输入/输出接口（I/O，Input/Output）、模数转换器（A/D，An

2022-07-14 digiproto 736

小迪和小捷的太空之旅——海盗篇

小迪小捷遭邪恶太空海盗绑架，SkyEye助小迪小捷虎口脱险！

2022-06-15 digiproto 597

ModelCoder：实现汽车四轮转向控制系统的建模仿真

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

2022-04-27 digiproto 893

SkyEye Q&A ——第一期

Q1.什么是SkyEye？A1.SkyEye，中文全称天目全数字实时仿真软件，是基于可视化建模的硬件行为级仿真平台，运用软件仿真技术，逼真地模拟出被测软件运行的物理环境。理想情况下，嵌入式软件的二进制可以不加修改直接运行于全数字实时仿真系统，且其运行的动态特性与真实环境一致。Q2.全数字实时仿真又是什么？A2.全数字实时仿真，指仿真的全过程可完全脱离原有的真实硬件环境完成。它不仅能够解决全物理和半

2022-04-13 digiproto 709

ModelCoder模块系列：PID模块介绍

ModelCoder是一款支持多种嵌入式系统建模并可以自动生成高安全可靠的C代码的软件设计和开发工具。ModelCoder当前拥有9个基础模块库，40余个模块，PID Controller为ModelCoder实现PID控制算法的模块。

2022-03-17 digiproto 884

媒体中心

媒体中心

产品与解决方案

媒体中心

人才战略

关于迪捷