形式化验证方法

作品数：51被引量：233H指数：7
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：郭建关永施智平张凯史建琦更多>>
相关机构：华东师范大学清华大学电子科技大学浙江大学更多>>
相关期刊：《农机化研究》《航空计算技术》《计算机技术与发展》《信息安全与通信保密》更多>>
相关基金：国家自然科学基金国家高技术研究发展计划中央高校基本科研业务费专项资金国家科技支撑计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
汽车电子控制系统安全设计的形式化验证
《时代汽车》2024年第19期150-152,共3页李泽华 
汽车电子控制系统已成为现代汽车的核心组成部分,因此,深入研究汽车电子控制系统安全设计和验证方法有助于提高车辆安全性能,增强车辆竞争力。本文阐述了汽车电子控制系统安全性的重要性,探讨了当前汽车电子控制系统安全设计和验证方法...
关键词：汽车电子控制系统 安全设计 形式化验证方法 
站场电动放空阀控制逻辑的形式化建模与验证
《现代电子技术》2023年第17期155-162,共8页董秀娟 赵浩羽 徐宝昌 周裕东 董长锁 赵正开 
国家石油天然气管网集团有限公司科学研究与技术开发项目(Y180022KY01KF0330004)。
在油气管道控制系统典型逻辑标准编制的早期,对拟标准化控制逻辑的建模与验证能够提前发现设计缺陷,有助于提高控制系统的功能完整性与安全性,进而避免因控制逻辑设计失误导致的危险事故发生。根据形式化验证方法中模型检验的原理,利用...
关键词：油气管道 控制逻辑 形式化方法 时间自动机 UPPAAL 形式化验证方法 
基于健壮半径求解的循环神经网络形式化验证方法
《信息安全学报》2023年第3期12-26,共15页赵亮 戚润川 段鑫民 李春奕 王小兵 
国家自然科学基金(No.61972301,No.61672403,No.62192730,No.62192734);西安市科技计划项目(No.22GXFW0025);陕西省重点研发计划(No.2020GY-043);陕西省重点科技创新团队(No.2019TD-001)资助。
随着软硬件技术的发展,神经网络在各行各业取得了广泛的应用,然而在应用过程中也暴露出健壮性的不足。因此,采用形式化的手段来检验和保障神经网络的安全性是至关重要的。然而,由于循环神经网络结构复杂、激活函数非线性等因素,目前关...
关键词：形式化验证 循环神经网络 健壮半径 近似求解 
一种基于UPPAAL的智能合约属性形式化验证方法被引量：2
《江西师范大学学报（自然科学版）》2023年第1期45-51,共7页张取发 王昌晶 左正康 卢家兴 廖云燕 王渊 
江西省教育厅科技重点课题(GJJ220302,GJJ210307,GJJ2200303,GJJ2200304)资助项目.
针对智能合约的属性验证问题,该文提出了一种基于UPPAAL的智能合约属性形式化验证方法.首先定义了Solidity基本语句的操作语义及其到时间自动机的转换,将智能合约转换成时间自动机网络模型;然后定义并描述智能合约常见的安全性和活性,...
关键词：智能合约 UPPAAL 时间自动机 安全性 活性 
航天嵌入式软件整数溢出的形式化验证方法被引量：2
《软件学报》2021年第10期2977-2992,共16页高猛 滕俊元 王政 
国家自然科学基金(61802017);装备预研领域基金(61400020407)。
整数溢出引起的软件系统安全性问题屡见不鲜,已有的模型检测技术由于存在状态空间爆炸、不能有效支持中断驱动型程序检测等缺点而少有工程应用.结合真实案例,对航天嵌入式软件整数溢出问题的分布和特征进行了系统性的分析.在有界模型检...
关键词：航天嵌入式软件 整数溢出 有界模型检测 中断驱动型程序 顺序化 
以太坊智能合约安全形式化验证方法研究进展被引量：7
《计算机技术与发展》2021年第9期104-111,共8页王赫彬 郑长友 黄松 孙金磊 丁一先 
国家重点研发计划重点专项项目(2018YFB1403400)。
以太坊智能合约是区块链技术的典型应用和实现。由于智能合约一旦部署就难以修改,智能合约在上链之前的正确性显得至关重要。虽然很多当前工作都对于智能合约漏洞的检测与预防进行了一系列研究,但是对于检查合约属性和范式的形式化验证...
关键词：以太坊 智能合约 形式化验证 定理证明 模型检测 
Ptolemy离散事件模型形式化验证方法
《软件学报》2021年第6期1830-1848,共19页陆芝浩 王瑞 孔辉 关永 施智平 
国家自然科学基金(61877040,61876111);首都师范大学交叉研究院项目(19530012005)。
Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不...
关键词：形式化验证 Ptolemy离散事件模型 模型自动转换 时间自动机 
智能合约的形式化验证方法研究综述被引量：23
《电子学报》2021年第4期792-804,共13页朱健 胡凯 张伯钧 
国家重点研发项目(No.2018YFB1402702);国家自然科学基金(No.61672074,No.61672075);教育部中国移动基金(No.MCM20180104);软件开发重点实验室基金(No.SKLSDE-2020ZX-21)。
形式化方法是在安全关键软件系统中被广泛采用而有效的基于数学的验证方法,而智能合约属于安全关键代码,采用形式化方法验证智能合约已经成为热点研究领域.本文对自2015年以来的47篇典型相关论文进行了研究分析,对技术进行了详细的分类...
关键词：形式化验证 智能合约 区块链 隐私保护 信息安全 可信交易 
刍议面向航天器星载软件的形式化验证方法
《电脑知识与技术》2020年第25期205-206,共2页王明亮 王永 尤志坚 施敏华 
随着星载软件在航天器上实现的功能比重越来越高,星载软件可靠性和可信性的指标要求越来越严格。传统软件测试方法的局限性难以确保万无一失,形式化方法以其高度数学化和严谨性的特点,常被应用于安全关键软件的验证。本文针对星载软件...
关键词：星载软件 形式化验证 需求规约化 形式化语法 
微服务组合验证方法综述
《无线通信技术》2019年第3期46-50,共5页毛昕怡 辛园园 
微服务架构作为一种分布式的架构,因其良好的平台兼容性、灵活的动态扩展能力、强大的容错能力等特点,在业内引起了越来越多的关注.在微服务架构中,通常单一微服务仅能实现一个简单的功能,而实现复杂的业务功能时,需将系统中各个独立的...
关键词：微服务 微服务组合 形式化验证方法 运行时检测 
全选清除导出
共5页<12345>
检索报告 对象比较 聚类工具 使用帮助 返回顶部