面向供应链物流的区块链产业应用研究
这是一篇关于区块链,供应链物流,智能合约,形式化验证,模型检测的论文, 主要内容为区块链技术以其交易共识、账本同步、链上信息不可篡改等特性,为企业间业务协同创造了一种全新的业务执行模式,依托区块链平台可实现在多个不同的利益实体间高效地协同业务、可信地执行交易、安全地共享数据,既可提升效率,又可保证公平。但在区块链技术与产业应用结合的具体实践中,仍存在许多需要解决的新问题,一方面是区块链上的交易数据的隐私与安全问题,链上公开交易结果及交易细节,商业应用面临新的安全挑战;另一方面,业务的实现依靠智能合约,合约的逻辑合理性、功能完善性等需要予以保证,可信、公平的业务面临着新风险。针对上述问题,本文围绕区块链技术的产业应用,从支持智能合约运行的区块链平台和支持业务实现的智能合约两个方面着手,研究了面向产业应用的区块链平台建设和保障智能合约正确性的形式化验证等工作,主要研究内容如下:(1)研究了区块链技术支持特定产业应用的网络架构设计、数据存储机制、业务系统运维等问题。结合产业业务需求,提出在网络架构上,设计具有层级化的组织结构,以证书链的模式关联网络上节点的数字身份与现实身份,保证业务参与者在链上的活动可控、可监管;在数据存储上,设计单链多账本模式,将节点计算资源虚拟划分加入不同业务域中,维护业务账本一致性,保证业务数据不会被无关节点获取;在业务运维上,设计自底向上的权限管理模式,从区块链网络、智能合约、业务交互,三个层次对业务操作者进行管理。(2)研究了基于区块链技术的供应链物流产业应用实现,从参与业务实体与实体间的交互关系上,分析传统供应链物流业务场景,提出了基于区块链的业务实现方案;依据业务参与实体的不同,将整个业务过程分为供需匹配、合同签订、货物运输三个阶段,并针对供应链物流业务在各阶段需要达成的业务目标,开发执行区块链业务交易操作的智能合约。借助Fisco Bcos区块链平台,搭建符合业务需求的区块链网络,完成合约部署测试工作。(3)研究了智能合约业务设计完备性的形式化验证方案及验证实现。为了保证智能合约能够正确实现业务需求,采用模型检测的形式化验证方法,在系统建模上,基于有穷自动机模型,从合约业务实现的角度,抽象提取合约状态集合、状态间迁移关系、状态间迁移条件,并以此构造带约束的确定自动机模型,形式化建模合约业务模型;在属性规约上,采用时序逻辑描述合约需要满足的业务属性,并提出状态、变换覆盖的属性完整性设计要求。最后,基于上述建模方案,选用Nu XMV模型检测工具,验证了所编写的智能合约业务设计完备性。(4)研究了基于区块链平台支持业务交易功能实现机制下的智能合约执行正确性的形式化验证方案及验证实现。智能合约业务执行的正确性依赖于区块链平台(系统级)交易共识等的支持,及合约代码层面(应用级)交易执行正确性的保证。依托交易在区块链上的执行流程,以用户进程、节点交易池进程、交易打包、区块执行、合约执行多个交错并发执行的进程,共同建模区块链业务执行系统模型,从系统属性和业务属性两个方面,设计相应的属性规约。最后,基于上述建模方案,选用SPIN模型检测工具,验证了在区块链平台支持下的合约执行正确性问题。
面向供应链物流的区块链产业应用研究
这是一篇关于区块链,供应链物流,智能合约,形式化验证,模型检测的论文, 主要内容为区块链技术以其交易共识、账本同步、链上信息不可篡改等特性,为企业间业务协同创造了一种全新的业务执行模式,依托区块链平台可实现在多个不同的利益实体间高效地协同业务、可信地执行交易、安全地共享数据,既可提升效率,又可保证公平。但在区块链技术与产业应用结合的具体实践中,仍存在许多需要解决的新问题,一方面是区块链上的交易数据的隐私与安全问题,链上公开交易结果及交易细节,商业应用面临新的安全挑战;另一方面,业务的实现依靠智能合约,合约的逻辑合理性、功能完善性等需要予以保证,可信、公平的业务面临着新风险。针对上述问题,本文围绕区块链技术的产业应用,从支持智能合约运行的区块链平台和支持业务实现的智能合约两个方面着手,研究了面向产业应用的区块链平台建设和保障智能合约正确性的形式化验证等工作,主要研究内容如下:(1)研究了区块链技术支持特定产业应用的网络架构设计、数据存储机制、业务系统运维等问题。结合产业业务需求,提出在网络架构上,设计具有层级化的组织结构,以证书链的模式关联网络上节点的数字身份与现实身份,保证业务参与者在链上的活动可控、可监管;在数据存储上,设计单链多账本模式,将节点计算资源虚拟划分加入不同业务域中,维护业务账本一致性,保证业务数据不会被无关节点获取;在业务运维上,设计自底向上的权限管理模式,从区块链网络、智能合约、业务交互,三个层次对业务操作者进行管理。(2)研究了基于区块链技术的供应链物流产业应用实现,从参与业务实体与实体间的交互关系上,分析传统供应链物流业务场景,提出了基于区块链的业务实现方案;依据业务参与实体的不同,将整个业务过程分为供需匹配、合同签订、货物运输三个阶段,并针对供应链物流业务在各阶段需要达成的业务目标,开发执行区块链业务交易操作的智能合约。借助Fisco Bcos区块链平台,搭建符合业务需求的区块链网络,完成合约部署测试工作。(3)研究了智能合约业务设计完备性的形式化验证方案及验证实现。为了保证智能合约能够正确实现业务需求,采用模型检测的形式化验证方法,在系统建模上,基于有穷自动机模型,从合约业务实现的角度,抽象提取合约状态集合、状态间迁移关系、状态间迁移条件,并以此构造带约束的确定自动机模型,形式化建模合约业务模型;在属性规约上,采用时序逻辑描述合约需要满足的业务属性,并提出状态、变换覆盖的属性完整性设计要求。最后,基于上述建模方案,选用Nu XMV模型检测工具,验证了所编写的智能合约业务设计完备性。(4)研究了基于区块链平台支持业务交易功能实现机制下的智能合约执行正确性的形式化验证方案及验证实现。智能合约业务执行的正确性依赖于区块链平台(系统级)交易共识等的支持,及合约代码层面(应用级)交易执行正确性的保证。依托交易在区块链上的执行流程,以用户进程、节点交易池进程、交易打包、区块执行、合约执行多个交错并发执行的进程,共同建模区块链业务执行系统模型,从系统属性和业务属性两个方面,设计相应的属性规约。最后,基于上述建模方案,选用SPIN模型检测工具,验证了在区块链平台支持下的合约执行正确性问题。
基于范式的MSVL编译器的设计与实现
这是一篇关于时序逻辑,形式化验证,MSVL,范式,编译器的论文, 主要内容为由于计算机技术在各个领域中的广泛应用,确保软件系统和硬件系统的正确性和可靠性显得非常关键。特别是在一些重要领域,例如航空航天、军事武器等,软硬件系统中的一个微小的错误可能会导致巨大的损失。在这些重要领域中,传统软件测试方法存在测试用例生成困难等缺点以致难以保证系统的可靠性,因此形式化验证方法作为传统软件测试方法的补充是保障系统可靠性的重要途径之一。其中基于时序逻辑的验证方法是形式化验证的方法之一,并得到了广泛的应用。实验室基于PTL(Projection Temporal Logic)自主设计并研发了MSVL(Modeling,Simulation and Verification Language)程序设计语言。该语言具有建模、仿真及验证的功能。与此同时,实验室基于MSVL的理论,自主研发了MSVL解释器和MC(MSVL Compiler)工具。MC工具虽然提高了编译MSVL程序的速度,但是其内部的语义分析过程是非形式化的,因此违背了MSVL的设计初衷。本文主要研究了一个基于范式的MCⅡ(MSVL CompilerⅡ)的设计与实现,主要贡献如下:1.MCⅡ整体框架和模块功能的设计与实现。通过使用LLVM(Low Level Virtual Machine)工具进行MCⅡ的开发,LLVM中间表示IR(Intermediate Representatio n)作为MCⅡ的中间代码。围绕着MCⅡ的输入处理模块、预处理模块、词法语法分析模块、语义分析库模块、转换器模块、IR代码重组模块、后端模块以及错误处理模块进行了详细的介绍。其中,MCⅡ中最关键的是通过使用范式约简的方法确保语义分析库中的语义分析过程是形式化的。2.在IR层面对MCⅡ进行优化,详细地介绍了优化方案,通过程序示例,获取优化前、优化后的编译时间,并进行对比,证明该优化的有效性。3.解决了MCⅡ实现过程中遇到的关键问题,比如形式化语义分析的关键问题以及与系统平台相关的关键问题,对问题和解决方法都进行了详细的说明。4.使用MSVL语言编写矩阵乘法、求解四阶幻方和并行归并排序的示例程序,并对程序进行仿真,证明了MCⅡ的可用性以及实用性。
基于范式的MSVL编译器的设计与实现
这是一篇关于时序逻辑,形式化验证,MSVL,范式,编译器的论文, 主要内容为由于计算机技术在各个领域中的广泛应用,确保软件系统和硬件系统的正确性和可靠性显得非常关键。特别是在一些重要领域,例如航空航天、军事武器等,软硬件系统中的一个微小的错误可能会导致巨大的损失。在这些重要领域中,传统软件测试方法存在测试用例生成困难等缺点以致难以保证系统的可靠性,因此形式化验证方法作为传统软件测试方法的补充是保障系统可靠性的重要途径之一。其中基于时序逻辑的验证方法是形式化验证的方法之一,并得到了广泛的应用。实验室基于PTL(Projection Temporal Logic)自主设计并研发了MSVL(Modeling,Simulation and Verification Language)程序设计语言。该语言具有建模、仿真及验证的功能。与此同时,实验室基于MSVL的理论,自主研发了MSVL解释器和MC(MSVL Compiler)工具。MC工具虽然提高了编译MSVL程序的速度,但是其内部的语义分析过程是非形式化的,因此违背了MSVL的设计初衷。本文主要研究了一个基于范式的MCⅡ(MSVL CompilerⅡ)的设计与实现,主要贡献如下:1.MCⅡ整体框架和模块功能的设计与实现。通过使用LLVM(Low Level Virtual Machine)工具进行MCⅡ的开发,LLVM中间表示IR(Intermediate Representatio n)作为MCⅡ的中间代码。围绕着MCⅡ的输入处理模块、预处理模块、词法语法分析模块、语义分析库模块、转换器模块、IR代码重组模块、后端模块以及错误处理模块进行了详细的介绍。其中,MCⅡ中最关键的是通过使用范式约简的方法确保语义分析库中的语义分析过程是形式化的。2.在IR层面对MCⅡ进行优化,详细地介绍了优化方案,通过程序示例,获取优化前、优化后的编译时间,并进行对比,证明该优化的有效性。3.解决了MCⅡ实现过程中遇到的关键问题,比如形式化语义分析的关键问题以及与系统平台相关的关键问题,对问题和解决方法都进行了详细的说明。4.使用MSVL语言编写矩阵乘法、求解四阶幻方和并行归并排序的示例程序,并对程序进行仿真,证明了MCⅡ的可用性以及实用性。
基于PVS的PPTLI定理证明系统的设计与实现
这是一篇关于形式化验证,定理证明,PPTLI,PVS,索引表达式的论文, 主要内容为随着计算机技术的飞速发展,软件开发形式趋于多样化,同时软件的规模和复杂性也持续增长。面对层出不穷的软件质量问题,保证系统的安全性和可信性尤为重要。在此背景下,形式化验证方法作为一种以数学为理论支撑的技术,越来越广泛地应用于各种软、硬件安全特性的验证中,并逐渐成为各领域研究人员保障软件系统正确性和可靠性的重要方法。定理证明是形式化验证的重要手段之一,它基于严格的数学基础进行可靠的验证,在一定程度上弥补了模型检测的不足。同时,在使用定理证明方法对系统及性质进行描述和验证的过程中,使用的逻辑表达能力越强,能够描述和验证的系统性质越多。带索引表达式的命题投影时序逻辑(PPTLI)具有着完全正则的表达能力,与其它时序逻辑相比,PPTLI更适用于描述和刻画计算机程序和系统的各类性质。因此,使用一种表达能力更强的时序逻辑来开展定理证明工作有利于对更大规模系统的设计与性质验证。结合以上背景,本文以带索引表达式的命题投影时序逻辑PPTLI为主要研究对象,基于原型验证系统(PVS)开发了一套PPTLI半自动定理证明系统。本文的研究内容主要包括如下三个方面。(1)基于PVS的基本时序构造的证明系统的开发。首先,通过PVS规约语言对PPTLI中基本类型、基本时序操作符以及基本逻辑公式进行构建。然后,设计辅助规则来对状态公式进行约束,并对系统推理形式进行设计。在此基础上,通过PVS完成对基本时序构造的证明系统中的公理、推理规则的形式化描述。(2)基于PVS的索引表达式构造的证明系统的开发。首先,在完成对基本索引项类型以及无穷或操作符的类型构建的基础上,设计了一系列索引项类型间的连接词,并通过辅助公理来保证索性项类型与PPTLI类型间的正确转换。然后,设计了一种复杂索引表达式用于等价表示线性时序逻辑中的逻辑构造。最后,根据以上定义,通过PVS完成对索引表达式构造的证明系统中公理和推理规则的形式化描述。(3)定理实例的证明。通过本文开发的证明系统,对PPTLI中一系列具有典型性质的定理实例进行理论推导和交互式证明,主要包括了基本时序构造的定理以及索引表达式构造的定理。实例运行结果表明,本文构建的证明系统能够完成对复杂定理的描述和证明,并在定理证明过程中,呈现出良好的性能。
Lustre语言安全性及活性模型检测工具的研究与实现
这是一篇关于Lustre同步语言,形式化验证,模型检测,可满足性模理论,活性性质的论文, 主要内容为作为保障软件系统符合设计需求的重要手段之一,模型检测技术在现代系统,特别是反应式实时系统的设计与开发中受到了越来越多的关注。在反应式实时系统这一领域,Lustre同步数据流语言占据了代表性地位。随着Lustre语言在航空航天、工业能源和轨道交通等领域反应式实时系统的设计中被广泛使用,这些领域对软件苛刻的正确性要求使得对Lustre语言构建的程序进行验证变得至关重要。目前已经有许多对Lustre程序进行验证的工具,并且在工业领域也得到了一定的应用。然而,这些工具几乎都只关注了对安全性性质的验证,而在对活性性质的验证方面则尚未有工具提供支持。为了填补这一空白,本文对Lustre语言提出了一种适合于验证的形式化语义,并根据这一语义设计并实现了一种基于SMT求解技术的支持安全性及活性性质验证的模型检测工具。本文的主要研究工作包括:·提出了Lustre语言的形式化语义:为了在性质验证部分将Lustre语言模型转换为迁移系统,本文详细解释了Lustre语言中包括节点和表达式等在内的各个语法结构的含义,然后根据Lustre语言的特点提出了形式化的语义,从瞬时语义和数据流语义两方面分别刻画了Lustre这一同步数据流语言在某一具体时刻和整体时间上的性质,在理论方面保证了后续验证过程中模型变换的正确性。·设计并实现了同时支持安全性和活性验证的Lustre模型检测工具:在对Lustre程序进行语法解析后,将整体的验证流程分为用于消去复杂语法结构的Lustre简化器、将Lustre程序转换为SMT格式迁移关系的SMT翻译器和负责调用模型检测算法进行验证的验证控制器三个部分,使用包括有界模型检测、k-归纳法、不变式生成和IC3算法在内的算法对性质进行并行验证;同时在此基础上使用L2SIA-WFR算法对活性性质提供了支持。·在安全性和活性测试用例集下进行实验评估和分析:对于设计并实现的模型检测工具NKind,在安全性性质和活性性质方面分别采用了经典的测试用例集对其和现有的工具Kind2,JKind和ic3ia进行了性能表现方面的评估和对比。实验评估的结果表明,NKind能够有效地对安全性和活性性质进行求解,同时在求解的效率方面与现有的类似工具相比具有竞争力。
Lustre语言安全性及活性模型检测工具的研究与实现
这是一篇关于Lustre同步语言,形式化验证,模型检测,可满足性模理论,活性性质的论文, 主要内容为作为保障软件系统符合设计需求的重要手段之一,模型检测技术在现代系统,特别是反应式实时系统的设计与开发中受到了越来越多的关注。在反应式实时系统这一领域,Lustre同步数据流语言占据了代表性地位。随着Lustre语言在航空航天、工业能源和轨道交通等领域反应式实时系统的设计中被广泛使用,这些领域对软件苛刻的正确性要求使得对Lustre语言构建的程序进行验证变得至关重要。目前已经有许多对Lustre程序进行验证的工具,并且在工业领域也得到了一定的应用。然而,这些工具几乎都只关注了对安全性性质的验证,而在对活性性质的验证方面则尚未有工具提供支持。为了填补这一空白,本文对Lustre语言提出了一种适合于验证的形式化语义,并根据这一语义设计并实现了一种基于SMT求解技术的支持安全性及活性性质验证的模型检测工具。本文的主要研究工作包括:·提出了Lustre语言的形式化语义:为了在性质验证部分将Lustre语言模型转换为迁移系统,本文详细解释了Lustre语言中包括节点和表达式等在内的各个语法结构的含义,然后根据Lustre语言的特点提出了形式化的语义,从瞬时语义和数据流语义两方面分别刻画了Lustre这一同步数据流语言在某一具体时刻和整体时间上的性质,在理论方面保证了后续验证过程中模型变换的正确性。·设计并实现了同时支持安全性和活性验证的Lustre模型检测工具:在对Lustre程序进行语法解析后,将整体的验证流程分为用于消去复杂语法结构的Lustre简化器、将Lustre程序转换为SMT格式迁移关系的SMT翻译器和负责调用模型检测算法进行验证的验证控制器三个部分,使用包括有界模型检测、k-归纳法、不变式生成和IC3算法在内的算法对性质进行并行验证;同时在此基础上使用L2SIA-WFR算法对活性性质提供了支持。·在安全性和活性测试用例集下进行实验评估和分析:对于设计并实现的模型检测工具NKind,在安全性性质和活性性质方面分别采用了经典的测试用例集对其和现有的工具Kind2,JKind和ic3ia进行了性能表现方面的评估和对比。实验评估的结果表明,NKind能够有效地对安全性和活性性质进行求解,同时在求解的效率方面与现有的类似工具相比具有竞争力。
本文内容包括但不限于文字、数据、图表及超链接等）均来源于该信息及资料的相关主题。发布者：代码驿站 ，原文地址：https://m.bishedaima.com/lunwen/54065.html
