检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

作为数学革命的形式化证明

自然辩证法研究 2024年第1期40卷 107-112页

作者：杨帆大连海事大学公共管理与人文艺术学院大连116026

随着计算机科学的兴起,数学家可以通过计算机完成对数学定理的证明与验证,由此形成了形式化证明的相关领域。在形式化证明的助力下,诸多数学难题得以攻破,这无疑改变了传统数学实践的范式。然而,学界对于形式化证明所引发的认识论转向... 详细信息

随着计算机科学的兴起,数学家可以通过计算机完成对数学定理的证明与验证,由此形成了形式化证明的相关领域。在形式化证明的助力下,诸多数学难题得以攻破,这无疑改变了传统数学实践的范式。然而,学界对于形式化证明所引发的认识论转向的论述尚不充分,究其原因主要有两个方面:其一是缺乏对形式化证明的本体论考察,其二是对数学革命的定义存在分歧。对形式化证明中人脑证明和机器证明进行区分,同时厘清两种不同的革命定义,可以为形式化证明作为数学革命的观点提供辩护。

关键词：形式化证明机器定理证明数学革命

在线全文

学校读者我要写书评

暂无评论

图搜索问题算法推导及形式化证明

江西师范大学学报（自然科学版） 2021年第6期45卷 642-651页

作者：刘晓丹胡颖左正康江西师范大学计算机信息工程学院江西南昌330022

用非形式化方法解决图搜索问题规模受限,对于一些复杂问题难以保证其正确性.传统的形式化方法推导图搜索问题难以理解且不易于形式化证明,现有形式化方法对这类问题的解决方案较少,在保证可靠性和正确性方面有欠缺.该文通过对图搜索问... 详细信息

用非形式化方法解决图搜索问题规模受限,对于一些复杂问题难以保证其正确性.传统的形式化方法推导图搜索问题难以理解且不易于形式化证明,现有形式化方法对这类问题的解决方案较少,在保证可靠性和正确性方面有欠缺.该文通过对图搜索问题的深入研究,开发出一种针对解决图搜索算法的新方法.首先刻画问题的规约,利用循环不变式的递归定义技术给出了开发图搜索问题循环不变式的新策略,在此基础上得到Apla抽象算法程序,并对该算法程序进行了形式化证明,再将已验证的Apla算法程序自动生成C++可执行程序,实现了从抽象的形式规约推演出具体的面向计算机的程序代码的程序精化完整过程.以拓扑排序和广度优先遍历为例对所提方法进行实验,实验结果验证了所提方法的有效性,不仅可以推导和证明已知算法,而且对未知算法的推导也有指导性作用.

关键词：图搜索问题循环不变式递归定义形式化证明

形式化证明在区域控制器应用软件开发中的应用

在线全文

学校读者我要写书评

暂无评论

形式化证明在区域控制器应用软件开发中的应用

第三届全国智慧城市与轨道交通学术会议

作者：吕新军罗勋陈祥卡斯柯信号技术有限公司北京市地铁运营有限公司地铁运营技术研发中心

区域控制器(ZC)是基于通信的列车自动控制(CBTC)信号系统中实现轨旁自动列车保护(ATP)功能的核心设备,用来计算列车移动授权以确保列车不发生冲撞,因此区域控制器软件实现的正确性对于确保整个CBTC信号系统的安全起着极其重要作用。采... 详细信息

区域控制器(ZC)是基于通信的列车自动控制(CBTC)信号系统中实现轨旁自动列车保护(ATP)功能的核心设备,用来计算列车移动授权以确保列车不发生冲撞,因此区域控制器软件实现的正确性对于确保整个CBTC信号系统的安全起着极其重要作用。采用形式化证明技术可以弥补传统开发过程中验证手段(如测试)片面性的缺点,是对软件(系统)全状态空间的正确性验证,确保软件(系统)实现与需求一致性。文章介绍了一种基于模型开发软件的形式化证明方法,描述了形式化证明工具、证明义务结构及形式化证明流程,并以iZC200型区域控制器应用软件为例,说明如何精确描述待证明安全属性,不同类型模型形式化证明及其优化方法。

关键词：形式化证明基于模型开发区域控制器

来源： cnki会议评论

在线全文

cnki会议

学校读者我要写书评

暂无评论

面向形式化证明的命令生成技术

计算机系统应用 2022年第1期31卷 273-278页

作者：莫广帅熊焰黄文超中国科学技术大学网络空间安全学院合肥230027 中国科学技术大学计算机科学与技术学院合肥230027

随着软件规模的不断增大,软件安全问题日益严重.作为软件系统安全检测的有效手段,形式化证明旨在利用数学方法完成对软件属性的严格验证.常用的形式化证明方法利用模式匹配来进行定理证明,但存在策略生成不完备等缺陷.本文提出一种基于... 详细信息

随着软件规模的不断增大,软件安全问题日益严重.作为软件系统安全检测的有效手段,形式化证明旨在利用数学方法完成对软件属性的严格验证.常用的形式化证明方法利用模式匹配来进行定理证明,但存在策略生成不完备等缺陷.本文提出一种基于注意力机制的命令预测框架,将LSTM与Coq结合,预测定理证明过程中的策略和参数.实验结果表明本文提出的模型在生成命令的准确度方面高于现有工作(本工作预测命令准确率为28.31%).

关键词：形式化证明 Coq 命令预测 LSTM 注意力机制

在线全文

学校读者我要写书评

暂无评论

面向高阶逻辑的形式化自动证明技术研究

面向高阶逻辑的形式化自动证明技术研究

作者：莫广帅中国科学技术大学

学位级别：硕士

当今,软件系统是否可信已经成为一个国家经济能否正常运转的关键因素之一。作为保障软件系统安全的有效手段,形式化方法以数理逻辑为基础,利用规约、建模和验证等手段验证软件的可靠性。相比一阶逻辑,高阶逻辑接受谓词作为参数,描述能力... 详细信息

当今,软件系统是否可信已经成为一个国家经济能否正常运转的关键因素之一。作为保障软件系统安全的有效手段,形式化方法以数理逻辑为基础,利用规约、建模和验证等手段验证软件的可靠性。相比一阶逻辑,高阶逻辑接受谓词作为参数,描述能力强,更易完成复杂软件模型的构建。在传统的高阶逻辑证明工具中,主要采用手工式的定理证明方法,学习难度大,人工成本高。因此,有研究者提出了融合模式匹配、机器学习等技术的自动化证明方法。但是这些工作在证明定理的过程中存在状态搜索爆炸问题,验证效率低、代价高。本文结合证明辅助工具Coq,针对定理证明过程中的语法树搜索关键技术展开研究,提出一种基于强化学习Deep Q Network(DQN)的动态搜索框架,提高自动证明的效率。本文开展的主要工作有:1.基于注意力机制的命令生成技术。为了预测定理证明过程中的命令(策略和参数),本文结合Gated Recurrent Unit(GRU)、Long Short-Term Memory Network(LSTM)等深度学习网络,设计了一种形式化命令预测技术。传统的命令生成方法存在命令生成不灵活、准确率不高等问题,本文有效地提取了定理中的信息,依据证明目标、上下文前提和当前策略三个特征,构建向量,针对策略和参数分别设计了相应的预测模型。在训练的过程中,模型结合注意力机制,捕捉重要的信息,减少了无用信息的干扰。实验结果表明,本文模型预测的证明命令在准确度方面高于现有工作。2.面向高阶逻辑的定理语法树搜索技术。为了解决在定理证明过程中搜索空间爆炸的问题,本文结合强化学习DQN,提出一种基于动态策略的定理证明框架。与监督学习相比,该方法不需要数据集进行神经网络训练,DQN能够自动优化当前的选择,找到正确的证明路径,完成证明的定理。为了将复杂的证明过程抽象成一个简单的、易交互的过程,本文将提取到的目标和上下文信息保存在定理树的节点中,以供DQN进行学习。本文设计了一种独热编码,解决了当前证明状态难以提取成特征向量的难题。此外,本文设计了检测算法以防止DQN算法在搜索定理树的过程中产生循环,避免证明的失败。在形式化项目CompCert中的实验表明,本工作证明定理的成功率达到了 14.5%.

关键词：形式化证明自动化 Coq 神经网络 Deep Q Network

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

重写对策在基于HOL的形式化证明中的应用

计算机工程与设计 2013年第10期34卷 3664-3668页

作者：张杰毛丹雯关永施智平北京化工大学信息科学与技术学院北京100029 首都师范大学信息工程学院北京100048

讨论了重写对策在基于高阶逻辑定理证明系统HOL的形式化证明过程中的应用。通过REWRITE_TAC对策、ASM_REWRITE_TAC对策和RW_TAC对策,详细分析了重写对策的功能、应用方法、应用环境、应用中可能出现的问题以及解决办法,给出了DB.match... 详细信息

讨论了重写对策在基于高阶逻辑定理证明系统HOL的形式化证明过程中的应用。通过REWRITE_TAC对策、ASM_REWRITE_TAC对策和RW_TAC对策,详细分析了重写对策的功能、应用方法、应用环境、应用中可能出现的问题以及解决办法,给出了DB.match搜索和DB.find搜索等重写对策的定理参数的选择方法,并进行了分析与比较。进一步说明了重写对策在基于HOL系统的形式化证明中的重要性,以期对HOL系统用户提供一些帮助与启发,促进HOL系统的进一步发展与完善,使形式化方法能够解决更多的实际问题。

关键词：定理证明方法高阶逻辑定理证明系统形式化证明目标制导法重写对策

高可靠性温室环境测控系统架构形式化建模与特性证明

在线全文

学校读者我要写书评

暂无评论

小型微型计算机系统 2012年第8期33卷 1723-1729页

作者：袁凌李国徽张晓芳华中科技大学计算机科学学院武汉430074

温室环境测控系统由多个可并发执行的子系统共同协作来构造适宜的温室环境以确保作物有效生长.为提高温室环境测控系统设计的效率和可靠性,本文提出一个能为设计者提供指导性框架的融入容错技术的高可靠性温室环境测控系统架构.并且运用... 详细信息

温室环境测控系统由多个可并发执行的子系统共同协作来构造适宜的温室环境以确保作物有效生长.为提高温室环境测控系统设计的效率和可靠性,本文提出一个能为设计者提供指导性框架的融入容错技术的高可靠性温室环境测控系统架构.并且运用PVS形式化语言对系统架构进行了精确而无二义性的形式化建模,以及PVS证明工具对系统架构的容错特性进行了机械化证明,以确保系统架构能满足高可靠性需求.

关键词：系统架构 PVS系统容错形式化建模形式化证明

在线全文

学校读者我要写书评

暂无评论

面向无线传感器网络的认证密钥协商机制

小型微型计算机系统 2023年

作者：李贵勇张航韩才君李欣超重庆邮电大学通信与信息工程学院

无线传感器网络(Wireless Sensor Networks，WSN)是物联网的重要组成部分，因为WSN能通过因特网将采集到的数据发送到云服务器。认证和密钥协商机制是一个重要的密码学概念，可以确保数据传输的机密和完整性。传感器节点是资源受限的设... 详细信息

无线传感器网络(Wireless Sensor Networks，WSN)是物联网的重要组成部分，因为WSN能通过因特网将采集到的数据发送到云服务器。认证和密钥协商机制是一个重要的密码学概念，可以确保数据传输的机密和完整性。传感器节点是资源受限的设备，因此目前多数认证和密钥协商机制在计算效率上并不适用于WSN。针对该问题，本文提出了一种新的认证和密钥协商机制，该方案是一种基于椭圆曲线的轻量级认证和密钥协商方案。在eCK安全模型下，将方案的安全性规约到CDH数学困难假设之上，形式化的证明了方案的安全性。最后通过方案对比，表明文章所提出的方案实现了计算效率和安全属性之间的平衡。

关键词：无线传感器网络认证和密钥协商 eCK模型 CDH假设形式化证明

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

面向无线传感器网络的认证密钥协商机制

小型微型计算机系统 2024年第5期45卷 1204-1208页

作者：李贵勇张航韩才君李欣超重庆邮电大学通信与信息工程学院重庆400065

无线传感器网络(Wireless Sensor Networks,WSN)是物联网的重要组成部分,因为WSN能通过因特网将采集到的数据发送到云服务器.认证和密钥协商机制是一个重要的密码学概念,可以确保数据传输的安全和完整性.传感器节点是资源受限的设备,因... 详细信息

无线传感器网络(Wireless Sensor Networks,WSN)是物联网的重要组成部分,因为WSN能通过因特网将采集到的数据发送到云服务器.认证和密钥协商机制是一个重要的密码学概念,可以确保数据传输的安全和完整性.传感器节点是资源受限的设备,因此目前多数认证和密钥协商机制在计算效率上并不适用于WSN.针对该问题,本文提出了一种新的认证和密钥协商机制,该方案是一种基于椭圆曲线的轻量级认证和密钥协商方案.在eCK安全模型下,将方案的安全性规约到CDH数学困难假设之上,形式化的证明了方案的安全性.最后通过方案对比,表明文章所提出的方案实现了计算效率和安全属性之间的平衡.

关键词：无线传感器网络认证和密钥协商 eCK模型 CDH假设形式化证明