【摘 要】
：
Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.How
【机 构】
：
School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026
论文部分内容阅读
Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.However,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and clients.In this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer.We also design a program logic to verify contextual refinement of concurrent objects w.r.t.their abstract specifications.We have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.
其他文献
由于轴承故障数据存在数据量少和分布不均衡的问题,将迁移学习引入故障诊断领域,同时由于轴承故障数据的分布与源数据集分布差异巨大,直接采用迁移学习的方法会产生负迁移效应,即由于源数据集与目标数据集间分布差异过大而导致无法学习到源数据集的知识,提出一种对迁移学习进行改进的诊断新方法:即两步迁移学习法,使用DCGAN来制作辅助数据集,在辅助数据集上进行迁移学习,再将网络放在目标数据集上再次进行迁移学习训练,根据与普通迁移学习和不使用迁移学习的对比实验,新方法相较于目前已有的方法具有更快的速度与更高的准确率.
针对机械故障、天气状况等随机因素在运输过程中易对各种运输方式造成影响,研究更具有实际意义的带软时间窗的多式联运4PL路径问题.在软时间窗约束下,以总运输费用最小为目标,建立带有软时间窗的多式联运4PL路径优化模型.设计基于天牛须搜索思想和莱维飞行机制的乌鸦搜索算法对模型进行求解,采用田口方法确定算法最优参数组合,与其他算法进行对比分析,实验结果表明改进算法具有更好的求解效果和稳定性.通过数据分析,采用多式联运的运输组织形式,相比单一3PL服务商的单一运输方式,能够有效降低总运输费用;对于客户不同的软时间窗
To cater for the scenario of coordinated transportation of multiple trucks on the highway,a platoon system for autonomous driving has been extensively explored in the industry.Before such a platoon is deployed,it is necessary to ensure the safety of its d
Modern multiprocessors deploy a variety of weak memory models(WMMs).Total Store Order(TSO) is a widely-used weak memory model in SPARC implementations and x86 architecture.It omits the store-load constraint by allowing each core to employ a write buffer.I
利用关系数据进行股价预测的方法最近已经被提出,但目前还没有找到一种有效的方法可以有选择地聚合不同类型的关系数据去预测股价.提出一种改进的多层节点图注意力网络(FHAN)模型,该方法融合Fraudar算法,提供了一种对多个对象关系之间看问题的视角.模型把公司看做节点,把交互看成边,选择性地聚合不同关系类型的信息,并将这些信息添加到每个公司的节点表示中,添加了信息的节点表示被输入到特定任务层自动选择信息,实验结果表明,该方法比目前流行的神经网络算法在股价预测的效果上更准确,实验选取不同神经网络算法做对比,在最
As a continuation of previous years\'special section on software systems,this special section encourages and promotes research to address challenges from the perspective of software systems.The goal of this special section is to present state-of-the-art
Many applications need to meet diverse requirements of a large-scale distributed user group.That challenges the current requirements engineering techniques.Crowd-based requirements engineering was proposed as an umbrella term for dealing with the requirem
Programmable logic controllers(PLCs)play a critical role in many industrial control systems,yet face in-creasingly serious cyber threats.In this paper,we propose a novel PLC-compatible software-based defense mechanism,called Heterogeneous Redundant Proact
Allocation,dereferencing,and freeing of memory data in kernels are coherently linked.There widely exist real cases where the correctness of memory is compromised.This incorrectness in kernel memory brings about significant security issues,e.g.,information
A quantum circuit is a computational unit that transforms an input quantum state to an output state.A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it.However,when the number of qubits increases,the ma