形式化

作品数：5172被引量：11555H指数：35
导出分析报告
相关领域：自动化与计算机技术文化科学更多>>
相关作者：关永施智平薛锦云张广泉段振华更多>>
相关机构：华东师范大学国防科学技术大学西安电子科技大学清华大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划国家社会科学基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机工程x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
云网融合环境下服务组合的未来属性验证
《计算机工程》2025年第3期310-319,共10页王湛 张鹏程 金惠颖 吉顺慧 
国家自然科学基金(U21B2016,62272145)。
随着云网融合技术以及空天地一体化网络的快速发展,越来越多的服务开始在云网融合环境下运行。在云网融合环境下,用户呈现移动性特征,导致服务组合过程变得愈发复杂,服务组合验证变得尤为关键。同时,在云网融合环境下用户要求服务组合...
关键词：云网融合 服务组合 马尔可夫决策过程 服务质量 形式化验证 
基于状态图转形式化B模型的安全苛求系统开发方法
《计算机工程》2024年第11期173-186,共14页赵大地 王恪铭 
四川省自然科学基金(2022NSFSC0464);成都市软科学研究项目(2023-RK00-00084-ZF)。
形式化方法精确且严格,较多应用于安全苛求系统开发,但目前仍存在学习成本高、使用复杂、重用性低等问题。常用的非形式化状态图模型虽易于使用却缺乏严格验证。针对这些问题,提出一种将状态图SCXML模型转译为形式化B模型的模型转化方法...
关键词：软件功能安全 形式化方法 模型转化 SCXML状态图 B方法 
基于Isabelle/HOL的文件系统形式化设计与验证
《计算机工程》2024年第4期277-285,共9页王文斌 钱振江 靳勇 孙高飞 邢晓双 苏超 孙天琦 
江苏省自然科学基金面上项目(BK20191475);常熟市社会发展项目(CS202204)。
对于构建可信操作系统而言,文件系统设计和实现的正确性至关重要,即使是已经得到广泛运用的文件系统仍然有漏洞被检测出来。采用形式化方法对文件系统的设计和实现的正确性进行严格的验证是公认的可行方法。当前文件系统的形式化验证工...
关键词：形式化验证 文件系统 定理证明 有限状态机 微内核 
基于强化学习的安全协议形式化验证优化研究被引量：3
《计算机工程》2021年第12期141-146,共6页杨锦翔 熊焰 黄文超 
国家重点研发计划(2018YFB2100300,2018YFB0803400);国家自然科学基金(61972369,61572453,61520106007,61572454);中央高校基本科研业务费专项资金(WK2150110009)。
使用形式化方法能够找到安全协议设计中存在的漏洞,但高效地对安全协议进行自动的形式化分析仍然是一个挑战。针对现有形式化自动验证工具无泛化性和效率低的不足,对基于强化学习的安全协议形式化验证框架smartVerif进行优化。使用无人...
关键词：强化学习 安全协议 形式化方法 自动验证 泛化性 
轨道交通控制软件中基于场景的需求分析方法被引量：1
《计算机工程》2021年第8期284-293,300,共11页闫倩倩 缪炜恺 
国家自然科学基金面上项目“数据驱动的机器学习软件系统的形式化需求建模工程方法”(61872144);国家自然科学基金青年基金“嵌入式控制软件的形式化规格说明构建的工程方法”(61402178)。
针对轨道交通控制软件的形式化方法,在实际工程应用中存在形式化建模和系统级场景验证困难的问题。提出一种面向轨道交通领域的形式化建模和需求确认及验证方法。通过非形式化、半形式化到形式化规约三步演化过程,为形式化规约构建提供...
关键词：形式化方法 需求规约 需求确认和验证 场景优化 轨道交通控制软件 
一种基于Isabelle/HOL的安全通信协议验证方法被引量：6
《计算机工程》2021年第1期146-153,共8页夏锐 钱振江 刘苇 
江苏省自然科学基金面上项目(BK20191475);2020年度江苏省第五期“333工程”科研资助项目(BRA2020306);江苏省高校“青蓝工程”中青年学术带头人培养对象资助项目(2019);国家电网公司科技项目。
传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢。为解决上...
关键词：通信协议 混合密钥 形式化建模 形式化验证 Isabelle/HOL定理证明辅助工具 
一种代币智能合约的形式化建模与验证方法被引量：7
《计算机工程》2020年第10期41-45,51,共6页欧阳恒一 熊焰 黄文超 
国家自然科学基金(61972369,61572453,61520106007,61572454);国家重点研发计划(2018YFB2100300)。
针对代币智能合约的安全问题,提出一种基于代币智能合约整数溢出漏洞的形式化建模与验证方法。分析现有The DAO和BEC等漏洞攻击事件,定义代币智能合约的安全属性,通过引入全局变量和数值比较等约束条件对代币智能合约的建模语言进行扩展...
关键词：智能合约 代币 形式化建模 形式化验证 整数溢出漏洞 
一种面向Trace与漏洞验证的污点分析方法被引量：3
《计算机工程》2020年第5期157-166,共10页秦彪 郭帆 杨晨霞 
国家自然科学基金(61562040);江西省教育厅科学技术研究项目(GJJ161305,GJJ151330)。
静态分析方法被广泛用于Android应用的隐私泄露检测,其以(Source,Sink)对形式检测潜在漏洞,但同时会产生大量虚警。针对该问题,提出一种上下文敏感和域敏感的污点分析方法。对污点传播的操作语义和一致性约束进行形式化定义,保证污点传...
关键词：污点分析 上下文敏感 域敏感 污点传播 形式化定义 
汇编级顺序语句块的自动形式化规约及其验证被引量：1
《计算机工程》2019年第10期64-69,77,共7页祁龙云 吕小亮 路红 黄皓 
国家电网公司2018年总部科技项目“可信嵌入式操作系统关键技术研究”(SGJSNT00FZJS1800129)
软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段,但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率,构建一种自动证明模型,并在此基础上提出语义自动规约算法以及对所规约的语...
关键词：自动形式化规约 自动化验证 定理证明器 交互式定理 形式化验证 
基于STP方法的SCADE模型形式化验证框架被引量：3
《计算机工程》2019年第10期70-77,共8页林荣峰 施健 朱晏庆 沈怡颹 周宇 
国家部委基金
高安全性应用开发环境(SCADE)的形式化验证组件Design Verifier能够验证航空航天领域嵌入式软件系统的安全性质,但不能充分描述拥有复杂时序性质的安全需求。为解决该问题,构建一种SCADE状态机的时序性质验证框架,将SCADE模型转换成NuSM...
关键词：航天器系统 形式化验证 高安全性应用开发环境 安全攸关领域 模型检查 时序性质 
全选清除导出
共17页<12345678910>
检索报告 对象比较 聚类工具 使用帮助 返回顶部