一种基于分离逻辑的块云存储系统验证工具

云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力.     

基于分离逻辑的并行程序性质验证方法

随着多核多线程并行执行方式的普及,并行程序形式化验证的需求日显突出.并行程序验证中执行流程的不确定性使验证的内容与目标的关系难以确定,且从并行程序直接进行性质验证会导致验证规模大.为此,提出一种基于分离逻辑的新的验证方法.该方法根据分离逻辑的程序语义描述兼有解释语义和公理语义的特点,从验证的性质出发,把要验证的性质式转换成并行语句序列的逻辑组合式,并进行整理和化简;然后,利用分离逻辑公理系统对语句序列进行验证,用验证了的断言集来求出性质的真值.实例进一步说明,此方法更有效,同时也简化了验证的规模.     

基于隔离逻辑的并行程序可靠性验证方法

并行程序验证的复杂性在于执行流程的不确定性以及由此导致的执行规模变大,使得验证的内容和目标之间的关系不明确。为解决该问题,提出一种基于隔离逻辑的并行程序可靠性验证方法。通过变量的执行关系图,描述变量相关的语句及执行关系,将所需验证的程序性质逻辑式转换为变量并行语句序列的逻辑组合式,使得性质表达式与并发程序的语句相关联。根据逻辑组合式确定语句执行序列和前后件逻辑表达式,基于并发隔离逻辑的公理系统对语句执行序列进行验证,并根据验证结果对并发程序进行修改和完善。通过对银行柜台业务办理的功能模块验证结果表明该方法是有效的。     

基于分离逻辑的程序验证技术

介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向.     

云存储系统的分析与应用研究

云存储系统是随着社会的发展应运而生的,在人们的生活中发挥着越来越重要的作用。本研究将向大家介绍云存储系统的一些基本概念,并针对其应用提更好的解决方案。     

存储系统功能验证方法浅析

IC日益增长的设计复杂性和在时间、代价方面的需求,使得验证工作很重要却又困难重重。传统的简单验证方法和手段已不能满足 要求,采用新的验证方法势在必行。以存储系统功能性的验证为例,介绍了目前流行的先进的验证方法.包括ABV(Assertion-based verification)和TBV(Transaction-based verification)。对ASIC芯片的一般功能验证流程也作了较为详尽的分析。     

基于云存储技术的数据库密文验证式检索研究

传统检索方法构建的检索模型与搜索体系之间缺少逻辑,检索效果不佳,因此研究基于云存储技术的数据库密文验证式检索方法.基于云存储技术设置密文搜索体系;制定检索逻辑;通过密文检索模型执行数据库密文验证式检索任务.设计对比试验,测试索引和检索性能.实验结果得知,这种方法在索引文件中用时最少,得到的检索文档数据更多.证明该方法有...     

云存储系统节能研究综述

云存储系统作为云计算的重要组成部分,是各种云计算服务的基础。但随云存储系统规模的不断扩大和在设计时对能耗因素的忽略,使其日益暴露出高能耗、低效率的问题。因为云存储系统占整个云计算中心能耗的27%～40%,所以无论从降低服务提供商的运营成本,还是从降低能耗以保护环境的角度出发,研究云存储系统中的节能技术都具有很大的现实意义与应用前景。将存储系统中的能耗优化问题分为基于硬件的节能方法与基于调度的节能方法两大类进行讨论;并将基于调度的节能方法分为基于节点调度、基于数据调度和基于缓存预取技术3类进行综合比较;最后,对适应节能的云存储体系结构、节能模式下的QoS保证、节能模式与计算模式的匹配以及纠删码容错技术下的节能研究4个方向进行了展望。     

增强云存储系统安全功能的方法探讨

我国计算机技术快速发展的过程中,云计算属于互联网中较为有效的计算形式,目前已经开始应用到中小企业、个人用户的领域中,能够系统化整合互联网资源,为用户提供相应的网络服务,充分利用既有的计算资源按照用户需求分配资源,服务质量较为良好.云存储系统属于云计算技术中的重要部分,可以根据用户需求进行各种资源的存储,服务商可以借助实...     

基于高阶逻辑的硬件验证方法

本文讨论了如何利用高阶逻辑描述硬件的行为及结构，提出了硬件验证的一般方法，高阶逻辑不仅可以作为一种描述语言用来描述硬件的行为及结构，而且可以作为证明系统用来验证硬件设计的正确性。文中给出的用以说明描述及验证的例子包括ＣＭＯＳ反相器、复位的奇偶校验器。     

云存储系统中基于分簇的数据复制策略

云存储技术已经成为当前互联网中共享存储和数据服务的基础技术,云存储系统普遍利用数据复制来提高数据可用性,增强系统容错能力和改善系统性能。提出了一种云存储系统中基于分簇的数据复制策略,该策略包括产生数据复制的时机判断、复制副本数量的决定以及如何放置复制所产生的数据副本。在放置数据副本时,设计了一种基于分簇的负载均衡副本放置方法。相关的仿真实验表明,提出的基于分簇的负载均衡副本放置方法是可行的,并且具有良好的性能。     

云存储系统性能评测技术研究

云存储系统目前应用广泛,其核心功能是向外提供存储服务,而云存储性能直接影响着云存储服务的质量.由于云存储系统的数据存储在云端,且使用角色众多,传统的性能评测技术不适用于云存储系统.从用户、云存储服务提供商、设备提供商3个角度出发,针对其关注的云存储系统不同层次,提出适用于多层次、多角色的性能评测指标和评测方法,提供可靠的适用于云存储系统的评测方案、规范测试方法,为性能优化提供数据参考,同时为用户选购、部署云存储系统提供可靠的参考意见.     

一种基于策略的云存储系统故障管理方法

为了解决云存储系统故障管理自动化的问题,基于策略管理的思想,提出了基于策略的云存储系统故障管理框架PSF-C,设计了基于XML的云存储系统故障处理策略形式化描述语言CFS-PDL,该语言简单、灵活、可扩展性强,能够适应云存储系统故障处理各类策略要素的形式化描述需求。针对云存储系统故障自动化管理的实现问题,给出了PSF-C的策略映射方法。PSF-C和CFS-PDL的提出为云存储系统故障自动化管理提供了思路,提高了可实现性。     

主动容错云存储系统的可靠性评价模型

除了传统的冗余机制,主动容错技术也被用来提高存储系统的可靠性。然而,当前对主动容错云存储系统可靠性的研究工作很少,而且都局限于硬盘故障服从指数分布的假设前提。针对主动容错磁盘冗余阵列RAID-5和RAID-6云存储系统提出两个可靠性状态转移模型,并基于转移模型设计了蒙特卡洛仿真算法,评价系统在一定运行周期内发生数据丢失事件的期望个数。该算法采用韦布分布函数模拟随时间变化（降低、恒定不变、或升高）的硬盘故障率,准确评价了主动容错机制、硬盘整体故障、故障修复、潜在块故障以及磁盘清洗过程对系统可靠性的影响。所提方法可以帮助系统设计者评估不同容错机制和系统参数对云存储系统可靠性的影响,有助于创建高可靠存储系统。     

基于TLA的UML模型形式化验证

统一建模语言(UML)不能直接对所建立模型的正确性进行形式化验证。为解决上述问题,从UML模型的静态结构和动态行为 2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法,在此基础上提出将UML模型转化为TLA+的形式化描述方法,并用TLC工具形式化检测TLA+描述的正确性。通过实例分析证明了该方法的有效性。     

云存储系统中数据完整性验证协议

在云存储网络环境中,数据的安全性和完整性是用户最关心的问题之一。综合考虑云存储网络环境中的安全需求,设计了云存储数据完整性验证(CS-DIV)协议。客户端把数据文件和校验标签上传到云存储服务器后随机抽查,服务器返回验证证据并由客户端判断文件的完整性。协议可以有效地验证云存储数据的完整性,并抵抗恶意服务器欺骗和恶意客户端攻击,从而提高整个云存储系统的可靠性和稳定性。仿真实验数据表明,所提协议以较低的存储、通信及时间开销实现了数据的完整性保护。     

复杂内核数据结构程序形式化验证

操作系统内核作为软件系统的基础组件, 其安全可靠是构造高可信软件系统的重要环节, 但是, 在实际的验证工作中, 操作系统内核中全局性质的不变式定义, 复杂数据结构程序的形式化描述和验证仍存在很多困难. 本文针对操作系统内核中满足的全局性质, 在代码层以函数为单位, 用全局不变式进行定义, 并在不同的函数中进行形式化验证, 从而证明各个函数符合操作系统内核的全局性质; 针对操作系统内核中经常使用的复杂数据结构程序, 本文通过扩展形状图理论, 提出一种使用嵌套形状图逻辑的方法来形式化描述复杂数据结构程序, 并对该方法进行了正确性证明, 最终成功验证操作系统内核中关于任务创建与调度, 消息队列创建与操作相关的代码.     

基于Swift的可去重校园云存储系统的设计与实现

随着高校信息化的发展以及教学、科研和管理应用系统的广泛应用,数据资源如:图片、文档、视频等非结构化资源增长十分迅速。如何应对校园网络环境中不断增大的存储需求,提高存储资源的利用效率,是校园数据中心运维中一个比较重要的问题。本文介绍了基于开源软件 Swift 的云存储平台的搭建,以及带有重复数据删除功能的校园云存储系统(Dedupe_swift) 的设计与实现。通过重复数据删除功能的引入,提高了底层存储空间利用率;采用源端去重机制,为用户缩短了重复文件的上传时间;通过 Web 服务将存储作为服务提供给用户,为用户提供良好的云存储访问体验。     

基于逻辑分离的无人机仿真系统设计

针对在无人机仿真系统开发过程中的结构复杂问题,以及时间、经济成本等问题,提出一种ROS环境下基于逻辑分离思想的体系结构,并设计了一款基于PX4开源固件的交互式工具包应用到仿真系统.首先,根据逻辑分离思想进行系统整体设计;其次,在单机和多机的条件下进行仿真并验证;最后对仿真进行分析,结果表明该系统可实现表示层、业务层、控制层逻辑分离的无人机仿真测试,体现出系统设计的正确性与可用性.由于逻辑分离思想的应用,使得系统各部分职能明确,具有更高的开放性和可控性.