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

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

基于Petri网的WSCI形式化模型分析

WSCI是一种Web服务组合标记语言,对于一些关键的业务流程,任何设计错误都会造成重大损失,因此有必要为WSCI语言建立形式化模型并给予分析,从而保证正确的业务流程部署。本文主要给出了WSCI的分析方法,基于文献[1]给出了形式化模型,提出了该形式化模型下的一种网融合方法。该方法将表示进程的网模型与其表示例外处理和子流程的网模型进行合并,形成统一的网模型。本文最后还给出了在该网模型下的可达图分析方法,从而达到分析带有例外处理的WSCI形式化模型的目的。     

基于模型转换的MARTE顺序图的形式化分析

作为一项新规范,MARTE有许多方面亟待完善.如何对依照MARTE设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行验证和精化,以完成A的验证和精化工作.此思想面临的难题是如何保证B能够完整且准确地模拟A的行为.提出了形式化模型-TrS4SD,用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析.首先给出顺序图的形式定义,把时阃变迁系统(TrS)扩充成TrS4SD,用TrS4SD描述顺序图的形式语义,最后对TrS4SD展开分析.这在一定程度上提高了设计阶段模型的正确性.通过一个实例说明从顺序图到TrS4SD的转化过程以及基于TTS4SD的验证方法.     

边缘加强的超高清视频质量评估

目的 随着网络和电视技术的飞速发展,观看4 K(3840×2160像素)超高清视频成为趋势。然而,由于超高清视频分辨率高、边缘与细节信息丰富、数据量巨大,在采集、压缩、传输和存储的过程中更容易引入失真。因此,超高清视频质量评估成为当今广播电视技术的重要研究内容。本文提出了一种边缘加强的超高清视频质量评估方法。方法 对输入视频的每一帧进行拆分处理,利用边缘检测算子对R、G、B三通道的图像分别进行边缘检测,合并R、G、B三通道的边缘信息得到视频帧的边缘图像。设计边缘掩蔽、内容依赖和时域记忆3个网络模块分别提取相应的特征,将特征输入到全连接层中进行降维处理后获得质量特征,基于质量特征计算输入视频的视频质量分数。由于超高清视频具有丰富的边缘,边缘细节清晰度极高,因此在边缘处引入的失真通常较为明显,而本文提出的边缘加强方法特别适用超高清视频的质量评估。同时由于提出的方法引入了内容依赖和时域迟滞特性,因此也同时适用其他野生视频的质量评估。结果 实验在包括超高清在内的4个视频质量评估数据集上进行,与5种主流方法进行比较,结果表明提出的方法性能优越。在KoNViD-1K、DVL2021、LIVE-Qualcomm、LSVQ据集上,与当前性能最好的方法相比,SROCC(Spearman rank-order correlation coefficient)指标分别提升了3.9%、4.2%、10.0%和0.6%,PLCC(Pearson’s linear correlation coefficient)指标分别提升了3.9%、2.2%、10.1%和0.1%。结论 本文方法结合超高清视频的特点,更好地拟合了人眼视觉特性,获得了当前最好的性能;同时由于未使用光流方法,大幅减少了计算量,获得了很好的泛化能力。     

无线自组织网络中构造2-连通k-支配虚拟主干网的近似算法

在无线自组织网络中,经常选取一些节点形成虚拟主干网,用以支持路由和区域监视等任务。由于无线网络自身存在误码率高、易受干扰等弱点,虚拟主干网需要具有一定的容错性。已经有研究者提出使用k-连通k-支配集合在无线自组织网络中构造容错虚拟主干网,并通过模拟实验评估了算法的性能。近年来,Wang Feng等人设计了常数近似算法用来构造2-连通虚拟主干网。本文将设计一个常数近似算法用以在无线自组织网络中构造一个2-连通k-支配虚拟主干网。     

一种新的时段演算及其验证

在Pandya提出的CTL*[DC]逻辑的基础上,对其语法和语义进行扩展,并对路径长度进行限制,定义了一个新的逻辑CTL*[k-QDDC],它可应用于实时系统的描述和验证.给出了在Kripke结构中直接验证CTL*[k-QDDC]逻辑公式在某状态是否成真的基本算法.在某些假设下,也证明了CTL*[k-QDDC]中的某个逻辑运算符的验证问题是NP完全的,这就说明CTL*[k-QDDC]的验证问题至少是NP难的.     

最大边染色的指数时间算法

最近,凤旺森,张立昂,曲婉玲,王捍贫对源于无线Mesh网络中的一个新的计算问题--最大边染色问题--提出了常数比近似算法.最大边染色问题要求对图的所有边染色,满足对任一顶点v,与其相关联的所有边所染的颜色种数不超过正整数q(q≥2),求使用颜色种数最多的染色方案.然而,他们并没有给出该问题的任何精确算法.提出了几个指数时间的精确算法并分析了它们的复杂度.对完全图可以在多项式时间内找到精确解.