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

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

构件组合的集成测试

模型检验是一种自动化验证技术,其应用主要的困难在于状态空间爆炸问题。针对构件组合形成的状态空间爆炸问题,结合构件抽象组合原理及反例引导的抽象精化框架,提出了一种测试用例自动生成的方法。根据某个待集成构件抽象已集成的其他构件,并通过组合各个抽象构件生成抽象组合模型。利用模型检验工具对组合模型进行集成测试,生成抽象测试用例,再通过精化得到原模型对应的具体测试用例。实验结果表明该方法减小了状态空间,在一定程度上减缓了状态空间爆炸的问题。     

构件组合的集成测试

模型检验是一种自动化验证技术,其应用主要的困难在于状态空间爆炸问题.针对构件组合形成的状态空间爆炸问题,结合构件抽象组合原理及反例引导的抽象精化框架,提出了一种测试用例自动生成的方法.根据某个待集成构件抽象已集成的其他构件,并通过组合各个抽象构件生成抽象组合模型.利用模型检验工具对组合模型进行集成测试,生成抽象测试用例,再通过精化得到原模型对应的具体测试用例.实验结果表明该方法减小了状态空间,在一定程度上减缓了状态空间爆炸的问题.     

反例引导的模型检验工具的设计

针对模型组合中常见的"状态空间爆炸"问题,分析了抽象和组合两种方法各自的优缺点,采用"反例引导的抽象精化"框架和模型检验思想,将抽象和组合结合起来,为模型组合的检验提出了一种新的方法.设计了模型的抽象、组合、检验和精化算法,开发了一款基于反例引导的、图形化的模型检验工具,使用Kripke结构建立模型,用LTL描述性质,从而表明了反例引导的模型检验方法的过程.     

谓词抽象技术研究

随着软、硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.     

模型检验综述

在软硬件验证里,模型检验是一个重要手段,至今它已经形成一个庞大的方法论体系。现在我们把模型检验内容从标准方法、抽象解释方法、综合方法3个范畴加以介绍,旨在形成人们对模型检验总的印象,从而全面理解和掌握模型检验各个方法的精神实质和具体情况,有助于将这些方法运用到实际软硬件验证中并从中受到启发,以便进一步发展模型检验理论或开发模型检验新的方法和工具。     

面向源代码的软件模型检测及其实现

模型检测应用于检测软件可靠性具有重要意义.介绍了一种基于谓词抽象和反例引导抽象求精技术对源程序进行建模和验证的模型检测方法,并结合自行研发的Jchecker工具详细介绍了该软件模型检测技术的运作过程和关键算法.     

基于完备抽象解释的模型检验CTL公式研究

在模型检验中,抽象是解决状态空间爆炸问题的重要方法之一.给定具体Kripke结构和时序描述语言CTL,基于抽象解释框架以及完备抽象解释和性质强保留之间的关系,抽象模型最小精化使得CTL性质强保留,可转换为抽象解释中抽象域的最小完备精化,并且总是存在抽象域的最小完备精化.根据状态标签函数确定初始抽象域,然后通过不动点求解,获得对CTL标准算子完备的最小抽象域,并依据此抽象域求得CTL性质强保留的最优抽象状态划分,最后构造出CTL性质强保留且最优的抽象状态转换系统.并指出了抽象域对CTL标准算子是完备的当且仅当抽象域对补集和标准前向转换是完备的.     

构件组合的抽象精化验证

针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间.     

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

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

Finding abstract commonalties of category members

To form a coherent conceptual category and use it for inductive inference, the cognitive system needs to discover commonalties among different objects. How does the system accomplish this task? This study compares two of the most commonly used functions of categories–classification and feature inference–and examines their effectiveness in finding abstract commonalties of category members. The results from two experiments show that a classification task is not very useful for abstraction. In contrast, a feature inference task is advantageous in extracting abstract commonalties. However, this advantage is limited. Finding abstract commonalities becomes burdensome when category labels are absent in the feature inference task. These results underscore the importance of category membership information for abstraction. It is suggested that this advantage comes from the fact that category labels help form structured representation and facilitate structural alignment.     

The Influence of the Level of Abstraction on the Evolvability of Conceptual Models of Information Systems

In today's dynamic environments, evolvability of information systems is an increasingly important characteristic. We investigate evolvability at the analysis level, i.e. at the level of the conceptual models that are built of information systems (e.g. UML models). More specifically, we focus on the influence of the level of abstraction of the conceptual model on the evolvability of the model. Abstraction or genericity is a fundamental principle in several research areas such as reuse, patterns, software architectures and application frameworks. The literature contains numerous but vague claims that software based on abstract conceptual models has evolvability advantages. Hypotheses were tested with regard to whether the level of abstraction influences the time needed to apply a change, the correctness of the change and the structure degradation incurred. Two controlled experiments were conducted with 136 subjects. Correctness and structure degradation were rated by human experts. Results indicate that, for some types of change, abstract models are better evolvable than concrete ones. Our results provide insight into how the rather vague claims in literature should be interpreted.     

Modular abstractions for verifying real-time distributed systems

In this work we present a verification methodology for real-time distributed systems, based on their modular decomposition into processes. Given a distributed system, each of its components is reduced by abstracting away from details that are irrelevant for the required specification. The abstract components are then composed to form an abstract system to which a model checking procedure is applied. The abstraction relation and the specification language guarantee that if the abstract system satisfies a specification, then the original system satisfies it as well.The specification languageRTL is a branching-time version of the real-time temporal logicTPTL presented in Alur and Henzinger [1]. Its model checking is linear in the size of the system and exponential in the size of the formula. Two notions of abstraction for real-time systems are introduced, each preserving a sublanguage ofRTL.     

Expert-novice knowledge of computer programming at different levels of abstraction

Computer programming knowledge can be classified into five levels of abstraction: objective, conceptual, functional, logical, and physical. An experiment was carried out to determine whether the mastering of knowledge at different levels of abstraction changed with the level of skill. Ten experts and ten novices in C computer programming participated in the experiment. The subjects' knowledge at the five levels of abstraction was tested through 20 multiple-choice questions. The experimental results indicated that knowledge differences between experts and novices at an abstract level or a concrete level depended on what abstract or concrete knowledge was implied. Experts had better abstract knowledge than novices at the conceptual and functional levels but not at the objective level. Experts had better concrete knowledge than novices at the physical level but not at the logical level. The classification of computer programming knowledge in levels of abstraction and the experimental results helped in clarifying a general finding from previous studies that experts had better abstract knowledge than novices.     

面向未解释程序的合作验证方法

未解释程序的验证问题通常是不可判定的,但是最近有研究发现,存在一类满足coherence性质的未解释程序,其验证问题是可判定的,并且计算复杂度为PSPACE完全的.在这个结果的基础上,一个针对一般未解释程序验证的基于路径抽象的反例抽象精化（CEGAR）框架被提出,并展现了良好的验证效率.即使如此,对未解释程序的验证工作依然需要多次迭代,特别是利用该方法在针对多个程序验证时,不同的程序之间的验证过程是彼此独立的,存在验证开销巨大的问题.本文发现被验证的程序之间较为相似时,不可行路径的抽象模型可以在不同的程序之间复用.因此,本文提出了一个合作验证的框架,收集在验证过程中不可行路径的抽象模型,并在对新程序进行验证时,用已保存的抽象模型对程序进行精化,提前删减一些已验证的程序路径,从而提高验证效率.此外,本文通过对验证过程中的状态信息进行精简,对现有的基于状态等价的路径抽象方法进行优化,以进一步提升其泛化能力.本文对合作验证的框架以及路径抽象的优化方法进行了实现,并在两个具有代表性的程序集上分别取得了2.70x和1.49x的加速.     

Abstractions for hybrid systems

We present a procedure for constructing sound finite-state discrete abstractions of hybrid systems. This procedure uses ideas from predicate abstraction to abstract the discrete dynamics and qualitative reasoning to abstract the continuous dynamics of the hybrid system. It relies on the ability to decide satisfiability of quantifier-free formulas in some theory rich enough to encode the hybrid system. We characterize the sets of predicates that can be used to create high quality abstractions and we present new approaches to discover such useful sets of predicates. Under certain assumptions, the abstraction procedure can be applied compositionally to abstract a hybrid system described as a composition of two hybrid automata. We show that the constructed abstractions are always sound, but are relatively complete only under certain assumptions.     

From fine-grained to abstract process models: A semantic approach

Organizations actively managing their business processes face a rapid growth of the number of process models that they maintain. Business process model abstraction has proven to be an effective means to generate readable, high-level views on business process models by showing coarse-grained activities and leaving out irrelevant details. In this way, abstraction facilitates a more efficient management of process models, as a single model can provide for many relevant views. Yet, it is an open question how to perform abstraction in the same skillful way as experienced modelers combine activities into more abstract tasks. This paper presents an approach that uses semantic information of a process model to decide on which activities belong together, which extends beyond existing approaches that merely exploit model structural characteristics. The contribution of this paper is twofold: we propose a novel activity aggregation method and suggest how to discover the activity aggregation habits of human modelers. In an experimental validation, we use an industrial process model repository to compare the developed activity aggregation method with actual modeling decisions, and observe a strong correlation between the two. The presented work is expected to contribute to the development of modeling support for the effective process model abstraction.     

Verifying Time Partitioning in the DEOS Scheduling Kernel

This paper describes an experiment to use the Spin model checking system to support automated verification of time partitioning in the Honeywell DEOS real-time scheduling kernel. The goal of the experiment was to investigate whether model checking with minimal abstraction could be used to find a subtle implementation error that was originally discovered and fixed during the standard formal review process. The experiment involved translating a core slice of the DEOS scheduling kernel from C++ into Promela, constructing an abstract “test-driver” environment and carefully introducing several abstractions into the system to support verification. Attempted verification of several properties related to time-partitioning led to the rediscovery of the known error in the implementation. The case study indicated several limitations in existing tools to support model checking of software. The most difficult task in the original DEOS experiment was constructing an adequate environment to close the system for verification. The fidelity of the environment was of crucial importance for achieving meaningful results during model checking. In this paper, we describe the initial environment modeling effort and a follow-on experiment with using semi-automated environment generation methods. Program abstraction techniques were also critical for enabling verification of DEOS. We describe an implementation scheme for predicate abstraction, an approach based on abstract interpretation, which was developed to support DEOS verification.