形式化验证

作品数：548被引量：1339H指数：16
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：关永施智平李晓娟史建琦郭建更多>>
相关机构：华东师范大学西安电子科技大学电子科技大学国防科学技术大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划中央高校基本科研业务费专项资金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
航天嵌入式软件安全性验证技术
《航天控制》2025年第2期72-78,共7页高猛 王晓玲 朱晓程 
作为影响安全苛刻系统的重要因素,软件安全性问题日益受到关注。本文结合航天嵌入式软件工程实践,以软件安全性需求为线索,聚焦典型安全性问题,从源代码安全性质的形式化验证、软件安全性需求的自动化测试两个维度,分析总结了包括安全...
关键词：航天控制 嵌入式软件 中断驱动 软件安全性 形式化验证 自动化测试 
基于多访问控制的智能合约重入攻击防御方法
《信息安全研究》2025年第4期333-342,共10页陈虹 谢金彤 金海波 武聪 马博宇 
国家自然科学基金项目(62173171);辽宁省教育厅科研项目(LJKFZ20220198)。
为解决智能合约在处理外部合约调用时存在漏洞而导致的重入攻击问题,提出一种基于多访问控制(multiple access controls,MAC)的智能合约重入攻击防御方法.通过采用多访问控制仅允许合约所有者进行调用,并防止函数在执行期间对同一事务...
关键词：智能合约 多访问控制 重入攻击 形式化验证 银行存取款 
同步数据流语言pre算子在Coq中的翻译验证
《西华大学学报(自然科学版)》2025年第2期87-95,共9页李春燕 赵长名 杨斐 马权 侯荣彬 
四川省重点研发计划项目“面向电力领域的规划评审知识库智能构建关键技术研究”(2021YFG0307);四川省科技计划资助(2019ZDZX0001)。
文章对同步数据流语言的pre算子进行详细处理,除了将pre算子翻译至fby算子,还对pre算子在第一周期的值根据其输入参数类型的不同做了相应的初始化,解决了pre算子第一周期为空的问题。输入参数为整型和布尔型,其第一周期初始化为false,...
关键词：同步数据流语言 可信编译器 形式化验证 
云网融合环境下服务组合的未来属性验证
《计算机工程》2025年第3期310-319,共10页王湛 张鹏程 金惠颖 吉顺慧 
国家自然科学基金(U21B2016,62272145)。
随着云网融合技术以及空天地一体化网络的快速发展,越来越多的服务开始在云网融合环境下运行。在云网融合环境下,用户呈现移动性特征,导致服务组合过程变得愈发复杂,服务组合验证变得尤为关键。同时,在云网融合环境下用户要求服务组合...
关键词：云网融合 服务组合 马尔可夫决策过程 服务质量 形式化验证 
并发进程的互模拟语义理论
《中国科技成果》2025年第5期58-58,共1页邓玉欣 
计算机软件已经成为国计民生的基础设施.如何保障计算系统的可信性是软件领域面临的重要挑战,以多核、并发、分布、异构和智能交互等为主要特征的系统已成为当今计算系统发展的主流.并发现象以其固有的复杂性增加了软件可信性保障的困难...
关键词：互模拟 形式化验证 行为相似性 并发进程 
一种基于新型混淆操作的RFID双向认证协议
《计算机工程与科学》2025年第2期247-255,共9页贾昊洲 徐鹏 王丹琛 徐扬 
国家自然科学基金(61976130);中央高校基本科研业务费专项资金(2682021GF012)。
针对RFID系统中存在的隐私和安全问题,提出了一种基于新型混淆操作的超轻量RFID认证协议,通过利用简单的逐位异或、循环左旋转和新提出的超轻量化分组循环操作,达到低复杂度、高安全性的目的。此外,由于在协议交互过程中的消息根据随机...
关键词：RFID认证协议 混淆操作 分组循环操作 形式化验证 
面向龙芯处理器的一种CompCert可信编译器重定向实现
《计算机科学》2024年第S02期747-755,共9页胡少儒 王隽伟 王生原 
国家重点研发计划(2022YFB3305204)。
CompCert是著名的C语言可信编译器,它借助于交互式定理证明工具Coq实现,能够确保生成的目标汇编代码保持源代码的语义,具有极高的可信度,近年来被广泛应用于学术界和工业界的许多安全攸关任务的研发工作中。CompCert编译器的当前版本支...
关键词：CompCert 编译器 编译器重定向 龙芯架构 形式化验证的编译器 COQ 
WebAssembly安全综述
《计算机研究与发展》2024年第12期3027-3053,共27页庄骏杰 胡霜 华保健 汪炀 潘志中 
国家自然科学基金项目(62072427,12227901);中国科学院稳定支持基础研究领域青年团队计划项目(YSBR-005);中国科学技术大学学术带头人培养项目。
WebAssembly是一种新兴的二进制指令集体系结构与代码分发格式,旨在为高级程序语言提供统一且架构无关的编译目标.由于其安全、高效与可移植等先进特性,WebAssembly在Web领域与非Web领域均得到了广泛应用,正在成为最有前景的跨平台公共...
关键词：WebAssembly 语言安全 漏洞检测与利用 安全增强 形式化验证 
计算机联锁形式化验证典型反例分析
《铁路通信信号工程技术》2024年第11期41-45,共5页刘丽娟 陈虹 陈耀华 
卡斯柯信号有限公司科研课题项目(RB.1X123015)。
形式化验证是确保计算机联锁系统满足特定安全需求的有效且重要的手段。由于形式化方法的特殊性,要求对于系统模型和安全需求模型的描述完全准确,否则均会导致验证不通过。根据计算机联锁形式化验证的实际经验,总结在安全需求模型建立...
关键词：形式化验证 计算机联锁 安全需求 反例 
面向物联网设备移动与通信行为的建模及验证
《软件学报》2024年第11期4993-5015,共23页刘靖宇 李晅松 陈芝菲 叶海波 宋巍 
国家自然科学基金(61702263,61761136003);CCF-华为创新研究计划(CCF-HuaweiFM2021004)。
物联网设备的使用范围正在不断扩张.模型检测是提升这类设备可靠性和安全性的有效手段,但常用的模型检测方法不能很好地刻画这类设备常见的跨空间移动和通信行为.为此,提出一种面向物联网设备移动与通信行为的建模及验证方法,以实现对...
关键词：模型检测 物联网 形式化验证 建模语言 
全选清除导出
共55页<12345678910>
检索报告 对象比较 聚类工具 使用帮助 返回顶部