分享5篇关于模型检测的计算机专业论文

今天分享的是关于模型检测的5篇计算机毕业论文范文, 如果你的论文涉及到模型检测等主题,本文能够帮助到你

基于P-RBAC的访问控制模型中职责机制的研究

这是一篇关于隐私感知RBAC,隐私策略,层叠问题,模型检测,UPPAAL的论文, 主要内容为随着计算机网络和社会经济的发展，人们在如商业、医院等交往场合中产生的数据资源日益增多，特别是现在公有云服务已广泛应用到生活和生产当中。在这之中，如银行、电商、医院或者云服务提供商等作为用户数据资源的管理者，须要提供细粒度的隐私保护机制，以使用户的数据在被收集、利用和分配等操作时，数据的隐私性可以在一定的程度上得到保护。在这种场合中，就需要一种规范、细粒度、易于管理且符合实际需求的访问控制模型来满足要求。P-RBAC的访问控制模型是在基于角色的访问控制（RBAC）模型的基础上进行的扩充，该模型不仅具有一般RBAC所具备的角色层次、最小权限、权限分离等灵活的特性，而且能提供条件、目的、职责等细粒度的隐私保护所需求的模块。但是随着模型中引入满足隐私需求的其他组成成分，策略间产生的不一致性的类型与可能性也随之增加，本文即在P-RBAC模型的基础上重点针对职责机制进行了分析。本文分析了P-RBAC访问控制模型中职责机制所具有的性质，包括职责的主体独立操作性、时间约束性和条件性等性质，并在对职责性质分析的基础上，提出一个职责的完整表示模型。结合P-RBAC策略的表示形式，分析了职责机制下P-RBAC访问控制策略存在的安全和不一致性的问题。然后，本文研究了模型中由于职责机制而导致的策略间的层叠问题。重点分析了层叠问题产生的条件与检测算法，并提出根据一定的流程进行层叠问题的消除。为了更好的检测此问题，本文设计一种算法将此问题转化为模型检测的方法，并通过现有的模型检测软件Alloy进行自动化的分析和解决这个问题。最后，本文分析了在P-RBAC背景下权限分离原则的实现机制。首先根据职责分配和执行过程的不同时间点，分析和定义了P-RBAC中职责在时间约束下的各种状态。继而给出职责的状态变换及权限分离原则在时间自动机验证工具UPPAAL中的实现模型，并根据工具的状态爆炸问题和职责特性提出对于系统的相关约简规则，最后验证了模型的有效性。

面向供应链物流的区块链产业应用研究

这是一篇关于区块链,供应链物流,智能合约,形式化验证,模型检测的论文, 主要内容为区块链技术以其交易共识、账本同步、链上信息不可篡改等特性,为企业间业务协同创造了一种全新的业务执行模式,依托区块链平台可实现在多个不同的利益实体间高效地协同业务、可信地执行交易、安全地共享数据,既可提升效率,又可保证公平。但在区块链技术与产业应用结合的具体实践中,仍存在许多需要解决的新问题,一方面是区块链上的交易数据的隐私与安全问题,链上公开交易结果及交易细节,商业应用面临新的安全挑战;另一方面,业务的实现依靠智能合约,合约的逻辑合理性、功能完善性等需要予以保证,可信、公平的业务面临着新风险。针对上述问题,本文围绕区块链技术的产业应用,从支持智能合约运行的区块链平台和支持业务实现的智能合约两个方面着手,研究了面向产业应用的区块链平台建设和保障智能合约正确性的形式化验证等工作,主要研究内容如下:(1)研究了区块链技术支持特定产业应用的网络架构设计、数据存储机制、业务系统运维等问题。结合产业业务需求,提出在网络架构上,设计具有层级化的组织结构,以证书链的模式关联网络上节点的数字身份与现实身份,保证业务参与者在链上的活动可控、可监管;在数据存储上,设计单链多账本模式,将节点计算资源虚拟划分加入不同业务域中,维护业务账本一致性,保证业务数据不会被无关节点获取;在业务运维上,设计自底向上的权限管理模式,从区块链网络、智能合约、业务交互,三个层次对业务操作者进行管理。(2)研究了基于区块链技术的供应链物流产业应用实现,从参与业务实体与实体间的交互关系上,分析传统供应链物流业务场景,提出了基于区块链的业务实现方案;依据业务参与实体的不同,将整个业务过程分为供需匹配、合同签订、货物运输三个阶段,并针对供应链物流业务在各阶段需要达成的业务目标,开发执行区块链业务交易操作的智能合约。借助Fisco Bcos区块链平台,搭建符合业务需求的区块链网络,完成合约部署测试工作。(3)研究了智能合约业务设计完备性的形式化验证方案及验证实现。为了保证智能合约能够正确实现业务需求,采用模型检测的形式化验证方法,在系统建模上,基于有穷自动机模型,从合约业务实现的角度,抽象提取合约状态集合、状态间迁移关系、状态间迁移条件,并以此构造带约束的确定自动机模型,形式化建模合约业务模型;在属性规约上,采用时序逻辑描述合约需要满足的业务属性,并提出状态、变换覆盖的属性完整性设计要求。最后,基于上述建模方案,选用Nu XMV模型检测工具,验证了所编写的智能合约业务设计完备性。(4)研究了基于区块链平台支持业务交易功能实现机制下的智能合约执行正确性的形式化验证方案及验证实现。智能合约业务执行的正确性依赖于区块链平台(系统级)交易共识等的支持,及合约代码层面(应用级)交易执行正确性的保证。依托交易在区块链上的执行流程,以用户进程、节点交易池进程、交易打包、区块执行、合约执行多个交错并发执行的进程,共同建模区块链业务执行系统模型,从系统属性和业务属性两个方面,设计相应的属性规约。最后,基于上述建模方案,选用SPIN模型检测工具,验证了在区块链平台支持下的合约执行正确性问题。

安全协议形式化分析及其应用

这是一篇关于安全协议,形式化方法,串空间模型,定理推证,模型检测的论文, 主要内容为协议是在计算机网络和分布系统中两个或多个主体(Principals)为相互交换信息而规定的一组信息交换规则和约定。安全协议也称作密码协议，是在协议中应用加密解密的手段隐藏或获取信息，以达到安全性的各种目的。对于安全协议的形式化研究始于20世纪70年代末，现在，安全协议的形式化研究成为一个热点领域，有众多的形式化和逻辑的研究方法涌现出来。串空间(strand space)模型是出现在上世纪末的一种新型的安全协议的形式化方法，它是一种能结合定理证明和模型检测的混合形式化方法。事实证明,串空间模型是分析安全协议的一种实用、直观和严格的形式化方法。基于此模型开发的自动验证工具ATHENA已经实现了对协议的认证性特性验证，但未能克服模型检测方法所造成的状态空间严重爆炸的问题，对秘密性协议的证明也是不完善的。我们结合使用定理证明和模型检测技术，开发了安全协议验证工具AVSP，其中核心算法AVSP首次使用了理想的概念来定义协议的秘密性，并对秘密性安全属性进行验证。我们还提出一些剪枝规则对状态搜索空间进行剪枝，在我们试验中得到的对于Needham-Schroeder安全协议的弱一致性认证属性验证过程中充分说明这些状态搜索空间剪枝规则的应用，该结果清楚地表明所有的空间剪枝规则可有效缩小状态搜索空间，防止状态空间爆炸。实验结果分析表明AVSP是正确的和高效的。