形式化

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机工程与科学x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一种基于新型混淆操作的RFID双向认证协议
《计算机工程与科学》2025年第2期247-255,共9页贾昊洲 徐鹏 王丹琛 徐扬 
国家自然科学基金(61976130);中央高校基本科研业务费专项资金(2682021GF012)。
针对RFID系统中存在的隐私和安全问题,提出了一种基于新型混淆操作的超轻量RFID认证协议,通过利用简单的逐位异或、循环左旋转和新提出的超轻量化分组循环操作,达到低复杂度、高安全性的目的。此外,由于在协议交互过程中的消息根据随机...
关键词：RFID认证协议 混淆操作 分组循环操作 形式化验证 
以Barendregt的变量约定形式化编程语言研究
《计算机工程与科学》2024年第10期1807-1814,共8页阿力木江·亚森 艾合买提·阿不来提 沙尔旦尔·帕尔哈提 阿布都克力木·阿布力孜 哈里旦木·阿布都克里木 
国家自然科学基金(62241208,61966033);新疆维吾尔自治区自然科学基金(2023D01A72);新疆财经大学校级科研基金(2022XGC049,2022XGC070,2022XGC022)。
编程语言、类型系统和逻辑系统中常见的命名绑定,在实践中实现存在困难。在理论中以抽象思考发现并避免即将发生的变量捕获。在实践中变量捕获的检测需要定义笨拙的辅助操作,使形式化和证明变得复杂。现有几种命名绑定技术旨在表达式具...
关键词：变量命名 命名绑定 形式系统 Barendregt的变量约定 编程语言理论 
格林定理的形式化及其初步应用
《计算机工程与科学》2023年第7期1178-1187,共10页刘永梅 王国辉 关永 张景芝 施智平 董璐 
国家重点研发计划(2019YFB1309900);国家自然科学基金(62002246,62272322,62272323);科技创新服务能力建设-基本科研业务费(科研费)项目(00621530290000)。
格林定理广泛应用于物理学、流体力学和化学等领域。通常使用传统的计算机仿真和数值计算方法构建基于格林定理的系统模型。然而,由于工具软件可能存在的系统缺陷导致模型出现偏差,从而使任务失败。为解决上述问题,采用基于高阶逻辑的...
关键词：形式化验证 定理证明 格林定理 HOL Light 
序列折半划分问题的形式化推导
《计算机工程与科学》2022年第6期1063-1071,共9页左正康 梁赞杨 苏崴 黄箐 王渊 王昌晶 
国家自然科学基金(61862033,61902162);江西省自然科学基金(20202BABL202026,20202BABL202025,20202BAB202015);江西省教育厅科学技术重点研究项目(GJJ210307)。
形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序。针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题,提出了一种新的序列...
关键词：折半划分 形式化推导 分划递推 程序求精 
多序列比对算法族的形式化设计与生成被引量：3
《计算机工程与科学》2020年第8期1383-1392,共10页张旭初 石海鹤 
国家自然科学基金(61662035,61762049,61862033)。
多序列比对问题是生物信息学研究的重要部分,是解决物种进化关系、基因组序列分析等问题的基础。多序列比对算法具有很高的专用性,不同的算法适用于不同的研究环境。目前常用的多序列比对软件是在生物信息学理论指导下利用多个子算法装...
关键词：多序列比对算法 特征模型 产生式编程 算法构件 PAR平台 
模式驱动的系统安全性设计的验证被引量：1
《计算机工程与科学》2020年第7期1197-1207,共11页郑小宇 刘冬梅 杜益宁 周子健 邱玫媚 朱鸿 
国家自然科学基金(61502233,61402229);江苏高校“青蓝工程”;中央高校基本科研业务费专项资金(30916011328);欧盟移动云计算FP7项目MONICA(PIRSES-GA-2011-295222)。
随着万维网和移动计算技术的广泛应用,系统安全性得到了越来越多的关注,使用安全模式对系统安全解决方案进行设计并验证是提升系统安全性的一种有效途径。现有方法根据系统安全需求选择适用的安全模式,在此基础上将模式组合为系统的安...
关键词：安全设计模式 代数规约 形式化验证 模型检测 
图数据压缩技术综述被引量：2
《计算机工程与科学》2020年第1期89-97,共9页李凤英 杨恩乙 董荣胜 
国家自然科学基金(61762024);广西自然科学基金(2017GXNSFDA198050,2016GXNSFAA380054);桂林电子科技大学研究生创新创业项目(2019YCXS053)
应用合适的压缩技术对包含上亿个节点和边的图数据进行紧凑准确的表示和存储是对大规模图数据进行分析和操作的前提。紧凑的图数据表示不仅可以降低图数据的存储空间,而且还可以支持在图数据上的高效操作。从图数据的存储角度出发对图...
关键词：邻接矩阵 邻接表 形式化方法 图压缩 
基于一阶逻辑的可满足求解方法研究进展被引量：2
《计算机工程与科学》2019年第12期2119-2126,共8页张建民 黎铁军 马柯帆 肖立权 
国家重点研发计划（2016YFB0200203）;国家自然科学基金（61103083,61133007）
基于命题逻辑的布尔可满足SAT存在描述能力弱、抽象层次低、求解复杂度高等问题,而基于一阶逻辑的可满足性模理论SMT采用高层建模语言,表达能力更强,更接近于字级设计,避免将问题转化到位级求解,在硬件RTL级验证、程序验证与实时系统验...
关键词：形式化验证 一阶逻辑 布尔可满足 可满足性模理论 
面向需求的安全关键系统形式化建模与验证方法研究被引量：3
《计算机工程与科学》2019年第8期1426-1433,共8页胡军 张维珺 李宛倩 
南京航空航天大学研究生创新基地(实验室)开放基金(kfjj20171611)(中央高校基本科研业务费专项资金);国家重点基础研究发展计划-973计划(2014CB744903)
在安全关键系统领域中,明确的需求对于一个系统的作用至关重要。使用基于模型的系统工程思想对自动飞行控制系统进行面向需求的形式化建模与验证,使用RSML-e语言对自动飞行控制系统(AFCS)需求进行建模,提出一种将RSML-e模型转化成NuSMV...
关键词：MBSE 自动飞行控制系统(AFCS) 形式化验证 RSML-e NUSMV 模型转换 
一种支持设计时软件重用的反射式软件体系结构及其形式化研究被引量：3
《计算机工程与科学》2019年第8期1434-1443,共10页罗巨波 应时 刘天时 
陕西省教育厅科研计划项目资助(项目编号:18JK0621);国家自然科学基金(61672392,61373038)
软件体系结构在软件重用中有着特殊的意义。缺乏显式的描述并使用支持体系结构重用过程的信息和缺乏有效的重用方法是软件体系结构难以重用最根本的原因。在软件设计阶段,将元信息、元建模、反射和软件体系结构结合起来,构造了一种支持...
关键词：软件体系结构重用 反射式软件体系结构 具体化 Object-Z形式化描述 
全选清除导出
共7页<1234567>
检索报告 对象比较 聚类工具 使用帮助 返回顶部