模型检验中抽象技术研究综述

在模型检验中,抽象技术是解决状态空间爆炸问题的有效方法之一。论文描述了模型检验对抽象模型的基本要求,给出了抽象模型的定义及其评价指标,对抽象技术和自动化的抽象精化技术的主要方法及其研究进展作了比较深入、全面的综述,并讨论了抽象技术今后的发展方向。     

实现数据存储、数据计算和资源管理的分离

在传统操作系统中,数据存储的抽象(进程虚拟地址空间)、数据计算的抽象(线程)和资源管理的抽象(进程)是不可分离的.首先分析了在操作系统中由于3类抽象不可分离而存在的问题,根据分析提出了数据存储抽象、数据计算抽象和资源管理抽象互相分离的思想,进而根据这一思想提出了虚拟地址空间基于文件操作系统,分析该操作系统的体系结构模型,研究了实现3类抽象分离的线程迁移技术和指令对文件寻址技术,最后讨论了系统的实现，测试和性能评价.此项研究说明了在操作系统中实现数据储存、数据计算和资源管理的分离是可行的.     

面向随机模型检验的模型抽象技术

随机模型检验是经典模型检验理论的延伸和推广,由于其结合了经典模型检验算法和线性方程组求解或线性规划算法等,并且运算处理的是关于状态的概率向量而非经典模型检验中的位向量,所以状态爆炸问题在随机模型检验中更为严重.抽象作为缓解状态空间爆炸问题的重要技术之一,已经开始被应用到随机模型检验领域并取得了一定的进展.以面向随机模型检验的模型抽象技术为研究对象,首先给出了模型抽象技术的问题描述,然后按抽象模型构造技术分类归纳了其研究方向及目前的研究进展,最后对比了目前的模型抽象技术及其关系,总结出其还未能给出模型抽象问题的满意答案,并指出了有效解决模型抽象问题未来的研究方向.     

一种基于抽象与精化技术的Web服务组合验证方法

模型检测因其自动化程度高、能够提供反例路径等优势,被广泛应用于Web服务组合的兼容性验证。本文针对模型检测过程中存在的状态爆炸问题,在传统的模型检测方法中引入谓词抽象和精化技术,提出了一种针对Web服务组合的抽象精化验证框架。使用谓词抽象技术对原子Web服务抽象建模,将各Web服务抽象模型组合成组合抽象模型;将模型检测后得到的反例在各原子Web服务上做投影操作,对投影反例进行确认;对产生伪反例的Web服务抽象模型进行精化,生成新的组合抽象模型,再次对性质进行验证。最后通过实例分析说明基于抽象精化技术的Web服务组合验证框架在缓解状态爆炸问题上的可行性。     

基于抽象符号表的内存模型

符号执行技术在软件测试和程序验证中发挥着重要作用。如何抽象和处理程序中各种数据类型和语法成分是符号执行必须解决的问题。本文提出抽象符号表的概念,以及基于抽象符号表建模内存的方法。抽象符号表记录可寻址对象的名称、类型、抽象地址和符号值,是一种简单、精确的内存抽象机制。内存模型是所有使用符号执行的技术的前提,本文系统给出了一个面向符号执行的内存模型。基于抽象符号表的内存模型能够统一处理各种数据类型和语法成分,包括函数和类,能够直接处理指针别名问题,不需要额外的别名分析算法。经过一些性能优化处理,基于抽象符号表的内存模型具有较好的性能。     

抽象技术及其在蒙特卡洛树搜索中的应用研究综述

抽象技术作为人工智能研究中高效拓展决策的重要组成部分,已广泛应用于大规模的决策问题.蒙特卡洛树搜索虽然在众多决策领域取得了卓越成就,但是在现实决策问题中面临着决策空间巨大和规划周期很长的问题.鉴于此,研究抽象技术及其在蒙特卡洛树搜索中的应用,从状态空间和动作空间两个角度出发分析抽象技术如何提升蒙特卡洛树搜索的决策能力,并对抽象蒙特卡洛树搜索研究中仍需要解决的问题和未来的研究方向作进一步展望.     

抽象技术与面向对象程序设计教学

抽象技术是人类理解和解决复杂问题最重要的工具之一,更是面向对象程序设计中应用最广泛的原则之一。本文介绍了抽象的概念、抽象层次的划分以及两种典型的抽象方法,并从抽象这个较高层次来理解面向对象技术的主要思想:类、对象、封装、继承和多态,等等。     

IA64二进制翻译中过程抽象技术及其实现

过程抽象技术是用机器无关的表达方式对过程中与机器相关的内容进行抽象。然而用传统的Pascal,C或者是C 语言来实现该技术是相当困难的。本文基于IA64二进制翻译框架,提出了一种新的过程抽象技术,并对扩展的过程抽象语言进行了详细介绍。     

基于ASM模型的协议一致性测试研究

针对协议测试中,状态机描述、测试集成环境和被测实现彼此独立带来的问题,提出了在可视化编程环境下利用抽象状态机模型和桩函数结合实现协议一致性测试方法。在分析抽象状态机测试理论的基础上,给出基于抽象状态机和remoting技术的协议分布式测试模型。以抽象状态机语言描述简单文件传输协议为例,采用分布式测试模型,实现了被测协议的远程一致性测试。     

Android系统非标准设备驱动程序设计

在深入研究Android硬件抽象层HAL和Java本地接口JNI技术原理的基础上,提出了一个Android非标准硬件驱动程序的设计方案。以一个非标准设备的驱动程式的实现为例介绍了驱动程序的功能模块分层设计,讨论了使用HAL Stub技术对硬件抽象层HAL模块进行优化的方法。     

Application of static analyses for state-space reduction to the microcontroller binary code

This paper describes the application of two abstraction techniques, namely dead variable reduction and path reduction, to the microcontroller binary code in order to tackle the state-explosion problem in model checking. These abstraction techniques are based on static analyses, which have to cope with the peculiarities of the binary code such as hardware dependencies, interrupts, recursion, and globally accessible memory locations. An interprocedural static analysis framework is presented that handles these peculiarities. Based on this framework, extensions of dead variable reduction and path reduction are detailed. A case study using several microcontroller programs is presented in order to demonstrate the efficiency of the described abstraction techniques.     

视频摘要技术综述

目的 类似于文本摘要,视频摘要是对视频内容的总结。为了合理地评估视频摘要领域的研究进展,正确导向视频摘要的继续研究,本文归纳总结视频摘要技术的主要研究方法和显著性成果,对视频摘要技术进行综述。方法 依据视频摘要的两个主要生成步骤:视频内容分析和摘要生成分别介绍视频摘要的主要研究方法。同时,分析了近5年视频摘要领域的研究状况,对视频摘要发展的新趋势:实时视频摘要和多视角视频摘要进行了阐述。最后,还对视频摘要的评价系统进行了分类总结。结果 对视频摘要进行综述,对摘要中的语义获取难题提出了2种指导性建议。并依据分析结果,展望了视频摘要技术未来的发展方向。结论 视频摘要技术作为视频内容理解的重要组成部分,有较大研究价值。而目前,视频摘要在视频语义表达和摘要评价系统方面并不精确完善,还需进一步的深入研究。     

An abstraction refinement approach combining precise and approximated techniques

Predicate abstraction is a powerful technique to reduce the state space of a program to a finite and affordable number of states. It produces a conservative over-approximation where concrete states are grouped together according to a given set of predicates. A precise abstraction contains the minimal set of transitions with regard to the predicates, but as a result is computationally expensive. Most model checkers therefore approximate the abstraction to alleviate the computation of the abstract system by trading off precision with cost. However, approximation results in a higher number of refinement iterations, since it can produce more false counterexamples than its precise counterpart. The refinement loop can become prohibitively expensive for large programs. This paper proposes a new approach that employs both precise (slow) and approximated (fast) abstraction techniques within one abstraction-refinement loop. It allows computing the abstraction quickly, but keeps it precise enough to avoid too many refinement iterations. We implemented the new algorithm in a state-of-the-art software model checker. Our tests with various real-life benchmarks show that the new approach almost systematically outperforms both precise and imprecise techniques.     

A framework for video abstraction systems analysis and modelling from an operational point of view

Nowadays the huge amount of video material stored in multimedia repositories makes its search and retrieval a very slow and usually difficult task. Existing video abstraction systems aim to relieve this problem by providing short versions of the original content which ease the search and navigation processes and reduce the browsing time. There are many approaches for video abstraction based on the optimal selection and presentation of a subset of fragments (keyframes, shots, etc.) from the original video attending to different criteria, usually dependent on the application scenario. Nevertheless, given the huge size and growth rate of existing video repositories there is an increasing need for providing efficient techniques. This paper presents a unified taxonomy and a generic architectural model aimed for the study of existing abstraction systems computational performance and characteristics. The taxonomy has been developed taking into account and identifying the operative characteristics of current state of the art video abstraction techniques. The proposed video abstraction architecture model characterizes the stages needed to build a generic abstraction process and establishes the basic architectural aspects and requirements for the modeling of systems with specific operative requirements.     

Measuring data abstraction quality in multiresolution visualizations

Data abstraction techniques are widely used in multiresolution visualization systems to reduce visual clutter and facilitate analysis from overview to detail. However, analysts are usually unaware of how well the abstracted data represent the original dataset, which can impact the reliability of results gleaned from the abstractions. In this paper, we define two data abstraction quality measures for computing the degree to which the abstraction conveys the original dataset: the histogram difference measure and the nearest neighbor measure. They have been integrated within XmdvTool, a public-domain multiresolution visualization system for multivariate data analysis that supports sampling as well as clustering to simplify data. Several interactive operations are provided, including adjusting the data abstraction level, changing selected regions, and setting the acceptable data abstraction quality level. Conducting these operations, analysts can select an optimal data abstraction level. Also, analysts can compare different abstraction methods using the measures to see how well relative data density and outliers are maintained, and then select an abstraction method that meets the requirement of their analytic tasks     

On-line video abstract generation of multimedia news

The amount of video content available nowadays makes video abstraction techniques a necessary tool to ease the access to the already huge and ever growing video databases. Nevertheless, many of the existing video abstraction approaches have high computational requirements, complicating the integration and exploitation of current technologies in real environments. This paper presents a novel method for news bulletin abstraction which combines on-line story segmentation, on-line video skimming and layout composition techniques. The developed algorithm provides an efficient, automatic and on-line news abstraction method which takes advantage of the specific characteristics of news bulletins for obtaining representative news abstracts.     

Data-abstraction refinement: a game semantic approach

This paper presents a semantic framework for data abstraction and refinement for verifying safety properties of open programs with integer types. The presentation is focused on an Algol-like programming language that incorporates data abstraction in its type system. We use a fully abstract game semantics in the style of Hyland and Ong and a more intensional version of the model that tracks nondeterminism introduced by abstraction in order to detect false counterexamples. These theoretical developments are incorporated in a new model-checking tool, Mage, which implements efficiently the data-abstraction refinement procedure using symbolic and on-the-fly techniques.     

Relevance-based abstraction identification: technique and evaluation

When first approaching an unfamiliar domain or requirements document, it is often useful to get a quick grasp of what the essential concepts and entities in the domain are. This process is called abstraction identification, where the word abstraction refers to an entity or concept that has a particular significance in the domain. Abstraction identification has been proposed and evaluated as a useful technique in requirements engineering (RE). In this paper, we propose a new technique for automated abstraction identification called relevance-based abstraction identification (RAI), and evaluate its performance—in multiple configurations and through two refinements—compared to other tools and techniques proposed in the literature, where we find that RAI significantly outperforms previous techniques. We present an experiment measuring the effectiveness of RAI compared to human judgement, and discuss how RAI could be used to good effect in requirements engineering.