普适计算环境下上下文不一致性的消除算法研究*

在普适计算环境下,由于所获得上下文信息的不一致性,往往会导致应用不一致性的产生。针对上下文不一致性的消除问题,提出了全丢弃消除算法、最新上下文丢弃算法、基于确定性上下文丢弃算法和基于相关性的上下文丢弃算法,并对算法的性能进行了比较和分析。实验表明,这些算法能够有效达到消除上下文不一致性的目的。     

基于变化的服务演化一致性判定

由于Web服务处在开放、动态、多变的网络环境下,为了有效响应用户需求、运行平台及外部环境的变化,服务必须具备演化的能力。演化后的服务应维持与原伙伴服务或服务用户之间的正常交互,这种性质称为演化一致性。由于Web环境的多样性,服务开发者对演化一致性的判定的标准并不统一。对于服务演化一致性判定问题,现有方法大多基于固定的判定标准,缺乏可调节、细粒度的定量分析且不能显式地反映服务版本之间的变化。针对上述不足,面向服务演化导致的变化,从服务的结构层和非功能层两个角度建立基于变化的服务描述模型,并在该模型的基础上引入演化一致度对演化一致性进行度量。基于所提出的方法,设计并实现了一个服务演化一致性判定工具,验证了所提出方法的可行性与有效性。     

非一致上下文的自动修复技术

在普适计算中,上下文持续快速变化,上下文感知的应用根据上下文变化自动调整自身的行为以适应这种变化。然而,由于不可预测的环境噪声和动态变化等诸多因素的影响,很容易造成上下文不一致。非一致上下文会导致应用异常,甚至失败。为了解决这个问题,提出了一种自动修复上下文的新技术。它分为两个阶段:生成抽象修复用例;执行用例,以验证上下文不一致性是否已经修复。从用户的实际需要出发,生成的修复用例可以分别满足完整性或正确性。实验结果表明,这种技术在修复成功率上远远超过其他技术。     

上下文一致性错误及其处理对应用的影响

在普适计算环境中,上下文信息由于受到噪声等不可控因素的干扰,面临着一致性错误的问题。这些错误会影响应用的正常运行,使其表现异常甚至失效。目前已经有自动的一致性错误处理方法来保障应用所获取的上下文满足数据层面的一致性约束,然而在数据层面保持一致是否能提升应用的运行质量并不明确。系统地研究了这个问题,并基于一组真实的上下文感知机器人小车应用,设计了一系列受控实验,来分析和比较在模拟和真实世界中上下文一致性错误的处理方式对应用运行质量的改善程度及潜在的负面影响。利用该实验的分析结果,将有助于提高普适计算中上下文感知应用的运行质量。     

一种网络备份系统的数据一致性检测方法

为了消除原始数据持续变化对数据一致性检测带来的影响,设计并实现了一种基于Windows操作系统的网络备份系统数据一致性检测方法。本方法在一致性检测过程中使用实时的Windows卷影拷贝数据来替代原始的动态变化数据执行与备份数据的一致性检测。通过实验结果证明,本方法的检测结果和使用原始数据与备份数据进行检测的结果一致。     

点物体主方向关系的一致性检验

一致性检验问题是主方向关系推理中非常重要的基础理论问题,提出了一种利用欧几里德空间坐标图实施一致性检验的新方法。首先对研究的问题进行了定义,阐述了方向关系的坐标图表示方法,从而使得对点物体方向关系约束集的一致性检验就转化为检测图中是否存在环的问题,通过一致性判定、环的检测、实施方法这3个环节来具体实现。其算法的时间复杂度是O（n+e）,优于传统的O（n²）     

实时并发系统的PTSL模型检测

随着实时并发系统的软件规模越来越大、复杂性日趋增加,如何保证并发实时系统正确性和可靠性成为日益紧迫的问题。模型检测技术采用自动化的验证算法判断系统是否具有某一性质,它不仅包括对系统模型的遍历以及基于图形的分析方法,而且还需要大量的数值计算。本文把实时并发模型看成对并发博弈模型（CGS）的扩展,在此基础上添加了概率与时间性质,提出了概率时间并发博弈结构（PTCGS）。同时本文还提出了新的逻辑语言-概率时间策略逻辑（PTSL）,它显式地把策略作为一阶逻辑中的对象,从而使我们能够以简单而自然的方式指定PTCGS系统中的非零和属性。PTSL模型检测方法能够让设计者准确知道模型是否满足用户的需求,从而提高系统的可靠性。最后,本文以ZeroConf协议为例来说明PTSL模型检测方法的正确性。     

Static consistency checking of web applications with WebDSL

Modern web application development frameworks provide web application developers with high-level abstractions to improve their productivity. However, their support for static verification of applications is limited. Inconsistencies in an application are often not detected statically, but appear as errors at run-time. The reports about these errors are often obscure and hard to trace back to the source of the inconsistency. A major part of this inadequate consistency checking can be traced back to the lack of linguistic integration of these frameworks. Parts of an application are defined with separate domain-specific languages, which are not checked for consistency with the rest of the application. Examples include regular expressions, query languages and XML-based languages for definition of user interfaces. We give an overview and analysis of typical problems arising in development with frameworks for web application development, with Ruby on Rails, Lift and Seam as representatives.To remedy these problems, in this paper, we argue that domain-specific languages should be designed from the ground up with static verification and cross-aspect consistency checking in mind, providing linguistic integration of domain-specific sub-languages. We show how this approach is applied in the design of WebDSL, a domain-specific language for web applications, by examining how its compiler detects inconsistencies not caught by web frameworks, providing accurate and clear error messages. Furthermore, we show how this consistency analysis can be expressed with a declarative rule-based approach using the Stratego transformation language.     

普适计算环境下上下文信息推理的研究

从各种低层上下文信息得到对人们更加有用的高层上下文信息即上下文推理是当前研究的热点.针对该问题,采用描述逻辑,研究基于本体模型的上下文推理方法.首先简要介绍基于本体的上下文模型,该模型增加了对上下文特性的建模,然后分别研究基于本体的推理、基于规则的推理及不一致性验证3种推理方式,借助Jena框架的推理接口实现,推理功能全面,通用性强,基本满足了普适计算系统中上下文推理的需求,最后给出了推理的可用性.     

Hybrid-Fixing:上下文一致性错误的正确修复

在普适计算中,上下文持续快速变化,上下文感知应用根据上下文变化自动调整自身的行为以作出适应.然而,由于不可预测和控制的环境噪声以及环境动态变化等诸多因素的影响,环境上下文会发生一致性错误,从而导致应用表现异常甚至失效.为了解决这些问题,上下文一致性错误需要被自动并正确地修复,现基于已有工作提出了一项新的修复技术hybrid-fixing,它结合了对一致性约束的静态分析和修复动作的动态产生,即使一致性约束内部存在复杂依赖关系,也能确保所生成的修复用例必然正确.实验结果表明,这项修复技术大幅提高了一致性约束内部存在复杂依赖关系下一致性错误修复的成功率,并只花费了很小的时间开销.     

基于2v-SVM和一致性检验的医学图像融合算法

对于不同模态的医学图像进行融合处理,可为临床提供更多的诊断信息。提出了一种基于2v-SVM和一致性检验的融合算法,首先对低频子图像采用2v-SVM融合规则;然后在高频部分进行一致性检验。试验结果表明,与传统方法相比,这种方法克服了在图像多尺度分解过程中产生的不稳定性和不连续性的缺点,可以使图像的视觉效果更好,并包含更多的信息。     

Model checking for action-based logics

A model checker is described that supports proving logical properties of concurrent systems. The logical properties can be described in different action-based logics (variants of Hennessy-Milner logic). The tools is based on the EMC model checker for the logic CTL. It therefore employs a set of translation functions from the considered logics to CTL, as well as a model translation function from labeled transition systems (models of the action-based logics) to Kripke structures (models for CTL). The obtained tool performs model checking in linear time complexity, and its correctness is guaranteed by the proof that the set of translation functions, coupled with the model translation function, preserves satisfiability of logical formulae.     

基于状态约简的顺序图和状态图一致性检测

为了解决系统设计过程中模型一致性问题,提出了一种对UML顺序图和状态图的语义一致性检测方法。该方法对顺序图和状态图一致性进行符号化描述,为一致性检测提供理论基础;提出状态约简规则和状态约简算法,能够减少冗余状态和迁移,证明了状态约简不影响一致性检测;提出改进的UML模型到PROMELA的转换方法并使用SPIN进行验证。实验表明上述方法能够有效地检测顺序图和状态图的一致性,在验证过程中减少冗余状态和迁移,转换后的代码结构简单、执行效率高。     

The complexity of checking consistency of pedigree information and related problems

Consistency checking is a fundamental computational problem in genetics. Given a pedigree and information on the genotypes (of some) of the individuals in it, the aim of consistency checking is to determine whether these data are consistent with the classic Mendelian laws of inheritance. This problem arose originally from the geneticists‘ need to filter their input data from erroneous information, and is well motivated from both a biological and a sociological viewpoint. This paper shows that consistency checking is NP-complete, even with focus on a single gene and in the presence of three alleles. Several other results on the computational complexity of problems from genetics that are related to consistency checking are also offered. In particular, it is shown that checking the consistency of pedigrees over two alleles, and of pedigrees without loops, can be done in polynomial time.     

基于二次特征的模糊分类算法在普适计算上下文变化感知中的研究*

为了简化普适计算环境原始特征的复杂度,方便该环境下的知识推理,采用核典型相关分析方法进行原始特征的二次提取,得到简约而重要的二次特征。在此二次特征的基础上施以模糊K近邻法计算待测模式相对于各类中心的隶属度,并按最大隶属度原则确定该模式所属上下文场景类。本算法致力于在不显著损失分类准确度的情况下尽可能地降低分类复杂度,从而解决普适计算环境中上下文变化感知的问题。     

混合云环境下利用世系保障数据一致性的研究

混合云环境下,公有云与私有云共同为用户提供服务,公有云中的应用可能需要频繁读取私有云中的数据,通过复制私有云中的副本到公有云中可降低网络开销,但不同云中文件副本的动态更新会导致云中各个副本的不一致性。提出了一致性服务,该服务由一致性维护模块和一致性检测与恢复模块两个部分组成。一致性维护模块通过发送文件的更新消息的方法维护副本的一致,降低了系统的响应时间;一致性检测与恢复模块利用世系的思想,通过对比副本的世系记录来检测副本的一致性,可将副本不一致状态恢复成一致状态。实验证明混合云下利用世系一致性服务是可行的,由此带来的通信和存储开销在可接受范围内。     

基于交际接口的Web应用模型检验

为了验证Web应用的质量,首次采用了基于交际接口及其工具TICC的建筑智能化系统Web应用验证方法,通过一个简单的能源管理Web应用系统实例说明了整个建模、构件模块组合验证和系统性质验证过程.结果表明验证能够顺利实现,因而该方法是一种合适的Web应用验证方法.     

Solving finite domain constraint hierarchies by local consistency and tree search

We provide a reformulation of the constraint hierarchies (CHs) framework based on the notion of error indicators. Adapting the generalised view of local consistency in semiring-based constraint satisfaction problems, we define constraint hierarchy k-consistency (CH-k-C) and give a CH-2-C enforcement algorithm. We demonstrate how the CH-2-C algorithm can be seamlessly integrated into the ordinary branch-and-bound algorithm to make it a finite domain (FD) CH solver. Experimentation confirms the efficiency and robustness of our proposed solver prototype. Unlike other FD CH solvers, our proposed method works for both local and global comparators. In addition, our solver can support arbitrary error functions.