课程文献中心 更多>>

摘要： Grove is a new framework for machine-checked verification of distributed systems. Grove focuses on modular verification. It enables developers to state and prove specifications for their components (e.g. an RPC library), and to use those specifications when proving the correctness of components that build on it (e.g. a key value service built on RPC). To enable modular specification and verification in a distributed systems, Grove uses the idea of ownership from separation logic. Using Grove, we built a verified unreliable RPC library, where we captured unreliability in the formal specification by using duplicable ownership. We also built a verified exactly-once RPC library, where we reasoned about ownership transfer from the client to server (and back) over an unreliable network by using the escrow pattern. Overall, we developed and verified an example system written in Go consisting of the RPC libraries, a sharded key-value store with support for dynamically adding new servers and rebalancing shards, a lock service, and a bank application that supports atomic transfers across accounts that live in different shards, built on top of these services. The key-value service scales well with the number of servers and the number of cores per server. The proofs are mechanized in the Coq proof assistant using the Iris  library and Goose.

关键词： 纺织工业  

ISBN: (纸本)9787565848117

摘要： 本书首先介绍了机械工程中的机构、零件与机器组成和机电控制基础的基本知识 ; 然后详细阐述了机械工程中的机电控制基础、机械设计, 最后介绍了纺织设备管理、纺织设备的使用与维护管理等内容。鉴于纺织设备管理作为纺织企业管理的一个重要领域, 直接影响到纺织企业的生产经营, 本书重点对纺织设备管理进行了介绍。本书理论层面知识简单, 介绍实践应用的内容较多, 以适应机械工程与设备管理研究的发展现状和趋势。

关键词： 消防监督   高层建筑   设备管理  

摘要： 随着我国城市化进程的深入,近几十年大量的高层建筑拔地而起,为社会经济发展和人们的生活质量提高提供了重要支持.但是对于高层建筑来说,目前还存在较多的安全隐患,尤其是当前的高层建筑结构复杂,包含的内容较多,结合了工作、娱乐、休闲、居住等多种功能,如果发生火灾,造成的后果是无法预料的.目前,我国关于高层建筑消防方面的法律法规和制度机制不健全,还存在较多缺陷亟待改善.基于此,本文以高层建筑为对象,对如何做好消防监督和设备管理工作提出建议,希望可以提高我国高层建筑的消防安全.

关键词： 并发文件系统   终止性   形式化验证   Coq  

摘要： 并发文件系统由于复杂的实现,容易产生死锁、无限循环等终止性漏洞,已有的文件系统证明工作都忽视了终止性的证明.证明了一个并发文件系统AtomFS的终止性,保证了每个文件系统接口在公平调度的条件下都能返回.证明AtomFS接口的终止性要说明当其遇到阻碍时,阻碍源头(其他线程)终将产生进展,促使当前线程阻碍的消除,证明的核心在于说明锁耦合(lock coupling)遍历算法的终止性.然而还存在着两点挑战:(1)文件系统的树形结构允许阻碍的线程分布在多条路径上,全局地识别出多个阻碍源头使证明失去了局部性;(2)rename接口由于需要遍历两条路径,会带来"跨路径阻碍"现象,多个rename可能相互跨路径阻碍成环,导致无法找到阻碍源头.提出了两个核心的技术点来应对这些挑战:(1)使用局部思想仅确定单个阻碍源头;(2)使用偏序法解决跨路径阻碍成环问题.成功地构建了一个终止性证明框架CRL-T,并验证了AtomFS的终止性,所有的证明都在Coq中实现.

关键词： 医学装备   精细化管理   Meta分析  

摘要： 目的系统评价医院医疗设备管理中开展精细化管理的应用效果。方法检索并选取1989年-2020年国内公开发表的关于我国国内医院医疗设备管理中开展精细化管理应用效果的随机对照试验文献,筛选符合纳入标准的试验进行研究,采用Review Manager5.3软件统计并分析相关数据。结果共有11项研究符合纳入标准。与未实施精细化管理的对照组相比,开展精细化管理后科室满意人数的比数比(OR)合并值为5.35(95%可信区间为3.69~7.74)。感染率的比数比(OR)合并值为0.21(95%可信区间为0.14~0.33)。两组故障维修的比数比(OR)合并值为0.15(95%可信区间为0.08~0.29)。设备完好情况的比数比(OR)合并值为5.60(95%可信区间为2.44~12.83)。结论Meta分析结果显示,医院医疗设备管理中开展精细化管理应用效果显著,值得临床推广使用。

关键词： 烧结设备   管理工作   探讨与论述  

摘要： 文章对烧结设备管理重要性的认识进行简单介绍,并对加强以人为本的建设是设备管理机制良好运行的关键单独强调,同时还提出了一些设备管理的应对策略,以供相关人员进行参考或借鉴。

关键词： 医院医疗设备管理   预防性维护模式   应用体会  

摘要： 医院医疗设备管理中,予预防性维护模式,体会效果。方法 以2020.01至2020.12为研究背景时间,按照时间差异性,分为A(传统管理)、B(预防性维护管理)组,各取医疗设备150台。分析两组管理质量,并分析统计学差异。结果 ①设备管理质量评分:B组>A组(P<0.05);②质量控制检测数据:开机率、合格率、有效利用率:B组>A组,故障次数、平均维修费用:B组A组((24.329,P0.037)。结论 医院医疗设备管理中,施以预防性维护模式,效果优良,能提高设备管理质量,值得优选。

关键词： 中间件   分布式系统   微服务   幂等性   数据一致性  

摘要： 随着国家电网深入数字化改革,移动化作业场景越来越迫切,服务入流量指数级倍增,传统单体系统架构已不能满足现有多用户高并发移动作业需求,而微服务集群架构下虽系统可用,但数据一致性和可靠性却得不到保证,这严重影响核心业务正常流转,又会引发许多数据治理问题。针对这类问题,本文提出基于中间件方案来解决高并发场景下分布式系统服务幂等性问题,通过对服务实例进行幂等性处理,提高系统的可靠性与准确性。实验表明,相比于不使用中间件或使用其它中间件,该方案有效提高了应用服务的数据准确率,保证了应用及系统有效平稳运行。