一种新的针对仿真系统的测试方法

针对普通被动测试方法的测试目标难以主动控制、被动机制下获取的测试数据实用性和充分性都较低等难点, 提出了新的测试方法。建立测试数据获取的被动机制, 对数据驱动的准被动测试法和目标驱动的准被动测试法的处理流程分别进行了设计, 创建了针对仿真系统测试过程的Z模型, 并对Z模型中各环节的技术关键给予设计解释。实践证明, 这种测试方法能够发现其他测试方法难以发现的bug, 对于仿真系统Z模型相比其他模型有多方面的优势。     

Formal methods applied to high‐performance computing software design: a case study of MPI one‐sided communication‐based locking

There is a growing need to address the complexity of verifying the numerous concurrent protocols employed in the high‐performance computing software. Today's approaches for verification consist of testing detailed implementations of these protocols. Unfortunately, this approach can seldom show the absence of bugs, and often results in serious bugs escaping into the deployed software. An approach called Model Checking has been demonstrated to be eminently helpful in debugging these protocols early in the software life cycle by offering the ability to represent and exhaustively analyze simplified formal protocol models. The effectiveness of model checking has yet to be adequately demonstrated in high‐performance computing. This paper presents a case study of a concurrent protocol that was thought to be sufficiently well tested, but proved to contain two very non‐obvious deadlocks in them. These bugs were automatically detected through model checking. The protocol models in which these bugs were detected were also easy to create. Recent work in our group demonstrates that even this tedium of model creation can be eliminated by employing dynamic source‐code‐level analysis methods. Our case study comes from the important domain of Message Passing Interface (MPI)‐based programming, which is universally employed for simulating and predicting anything from the structural integrity of combustion chambers to the path of hurricanes. We argue that model checking must be taught as well as used widely within HPC, given this and similar success stories. Copyright © 2009 John Wiley & Sons, Ltd.     

面向高可信软件的整数溢出错误的自动化测试

面向高可信软件提出了一种二进制级高危整数溢出错误的全自动测试方法(dynamic automatic integer-overflow detection and testing,简称DAIDT).该方法无需任何源码甚至是符号表支持,即可对二进制应用程序进行全面测试,并自动发现高危整数溢出错误.在理论上形式化证明了该技术对高危整数溢出错误测试与发掘的无漏报性、零误报性与错误可重现特性.为了验证该方法的有效性,实现了IntHunter原型系统.IntHunter对3个最新版本的高可信应用程序(微软公司Windows 2003和2000 Server的WINS服务、百度公司的即时通讯软件BaiDu Hi)分别进行了24小时测试,共发现了4个高危整数溢出错误.其中3个错误可导致任意代码执行,其中两个由微软安全响应中心分配漏洞编号CVE-2009-1923,CVE-2009-1924,另一个由百度公司分配漏洞编号CVE-2008-6444.     

Covering arrays for efficient fault characterization in complex configuration spaces

Many modern software systems are designed to be highly configurable so they can run on and be optimized for a wide variety of platforms and usage scenarios. Testing such systems is difficult because, in effect, you are testing a multitude of systems, not just one. Moreover, bugs can and do appear in some configurations, but not in others. Our research focuses on a subset of these bugs that are "option-related"-those that manifest with high probability only when specific configuration options take on specific settings. Our goal is not only to detect these bugs, but also to automatically characterize the configuration subspaces (i.e., the options and their settings) in which they manifest. To improve efficiency, our process tests only a sample of the configuration space, which we obtain from mathematical objects called covering arrays. This paper compares two different kinds of covering arrays for this purpose and assesses the effect of sampling strategy on fault characterization accuracy. Our results strongly suggest that sampling via covering arrays allows us to characterize option-related failures nearly as well as if we had tested exhaustively, but at a much lower cost. We also provide guidelines for using our approach in practice.     

Source Code Prioritization Using Forward Slicing for Exposing Critical Elements in a Program

Even after thorough testing,a few bugs still remain in a program with moderate complexity.These residual bugs are randomly distributed throughout the code.We have noticed that bugs in some parts of a program cause frequent and severe failures compared to those in other parts.Then,it is necessary to take a decision about what to test more and what to test less within the testing budget.It is possible to prioritize the methods and classes of an object-oriented program according to their potential to cause failures.For this,we propose a program metric called influence metric to find the influence of a program element on the source code.First,we represent the source code into an intermediate graph called extended system dependence graph.Then,forward slicing is applied on a node of the graph to get the influence of that node.The influence metric for a method m in a program shows the number of statements of the program which directly or indirectly use the result produced by method m.We compute the influence metric for a class c based on the influence metric of all its methods.As influence metric is computed statically,it does not show the expected behavior of a class at run time.It is already known that faults in highly executed parts tend to more failures.Therefore,we have considered operational profile to find the average execution time of a class in a system.Then,classes are prioritized in the source code based on influence metric and average execution time.The priority of an element indicates the potential of the element to cause failures.Once all program elements have been prioritized,the testing effort can be apportioned so that the elements causing frequent failures will be tested thoroughly.We have conducted experiments for two well-known case studies - Library Management System and Trading Automation System - and successfully identified critical elements in the source code of each case study.We have also conducted experiments to compare our scheme with a related scheme.The experimental studies justify that our approach is more accurate than the existing ones in exposing critical elements at the implementation level.     

A Supermodel Framework Supporting Validated Upgrading of Reactive Systems

A software product is typically upgraded many times over its lifetime. Reactive systems are no exception, undergoing evolutionary version changes to add features and fix bugs. Evolving these stateful systems, such as email clients, software agents, smart cell phones, and personal digital assistants, is complicated by the fact that new versions of the software must deal correctly with legacy instances. Users of earlier versions have invested significant resources in creating the state of the legacy instance, and usually require that this state be upgraded appropriately when the new system version is activated. However, validating the correctness of this upgrading behavior is particularly difficult, whether through testing or automated reasoning techniques like theorem proving or model checking, because legacy states are typically unreachable to the new version of the software. This paper explores this problem and requirements for its solution. It then presents a simple and widely applicable upgrade framework, based upon the idea of a supermodel that allows upgrade behavior to be validated using mainstream approaches. Finally, it also gives techniques for simplifying the validation problem.     

Non-mutual captures in cyclic pursuit

In cyclic pursuit n bugs chase each other in cyclic order, each moving at unit speed. Mathematical problems and puzzles of pursuit, and cyclic pursuit in particular, have attracted interest for many years. In 1971 Klamkin and Newman [17] showed that if n=3 and the initial positions of the bugs are not collinear, then all three bugs capture their prey simultaneously, i.e., no bug captures its prey prior to the moment when the pursuit collapses to a single point. They asked whether the result generalizes to more bugs. Behroozi and Gagnon [4] showed that it does generalize to n=4 if the bugs' initial positions form a convex polygon. In this paper we resolve the general question in k dimensions: It is possible for bugs to capture their prey without all bugs simultaneously doing so even for non-collinear initial positions. The set of initial conditions which give rise to non-mutual captures is, however, a sub-manifold in the manifold of all possible initial conditions. Hence, if the initial positions are picked randomly according to a smooth probability distribution, then the probability that a non-mutual capture will occur is zero. This revised version was published online in August 2006 with corrections to the Cover Date.     

面向整数错误检测的蜕变测试方法研究

整型错误在安全性和功能性方面都是影响软件质量的重要因素,但是由于测试人员往往面临Oracle问题,无法判断程序是否出现整型错误,除非程序输出一个明显的异常值。本文利用蜕变测试技术发现由于整型错误产生的隐错,实验结果显示基于蜕变关系的整型错误检测方法可检测出平时发现不了的隐式非预期输出,有效地提高了检测整型错误的效率。     

Practical testing of a C99 compiler using output comparison

A simple technique is presented for testing a C99 compiler, by comparing its output with the output from pre‐existing tools. The advantage to this approach is that new test cases can be added in bulk from existing sources, reducing the need for in‐depth investigation of correctness issues and for creating new test code by hand. This technique was used in testing the PalmSource Palm OS® Cobalt ARM C/C++ cross‐compiler for Palm‐Powered® personal digital assistants, primarily for standards compliance and the correct execution of generated code. The technique described here found several hundred bugs, mostly in our in‐house code, but also in longstanding high‐quality front‐ and back‐end code from Edison Design Group and Apogee Software. It also found 18 bugs in the GNU C compiler, as well as a bug specific to the Apple version of GCC, a bug specific to the Suse version of GCC, and a dozen bugs in versions of GCC for the ARM processor, several of which were critical. Copyright © 2007 John Wiley & Sons, Ltd.     

<Emphasis Type="Italic">Mondex</Emphasis>, an electronic purse: specification and refinement checks with the <Emphasis Type="Italic">Alloy</Emphasis> model-finding method

This paper explains how the Alloy model-finding method has been used to check the specification of an electronic purse (also called smart card) system, called the Mondex case study, initially written in Z. After describing the payment protocol between two electronic purses, and presenting an overview of the Alloy model-finding method, this paper explains how technical issues about integers and conceptual issues about the object layout in Z have been tackled in Alloy, giving general methods that can be used in most case studies with Alloy. This work has also pointed out some significant bugs in the original Z specification such as reasoning bugs in the proofs, and proposes a way to solve them. J. C. P. Woodcock     

Detecting races in Relay Ladder Logic programs

Relay Ladder Logic (RLL) [5] is a programming language widely used for complex embedded control applications such as manufacturing and amusement park rides. The cost of bugs in RLL programs is extremely high, often measured in millions of dollars (for shutting down a factory) or human safety (for rides). In this paper, we describe our experience in applying constraint-based program analysis techniques to analyze production RLL programs. Our approach is an interesting combination of probabilistic testing and program analysis, and we show that our system is able to detect bugs with high probability, up to the approximations made by the conservative program analysis. We demonstrate that our analysis is useful in detecting some flaws in production RLL programs that are difficult to find by other techniques.     

High-Impact Bug Report Identification with Imbalanced Learning Strategies

In practice, some bugs have more impact than others and thus deserve more immediate attention. Due to tight schedule and limited human resources, developers may not have enough time to inspect all bugs. Thus, they often concentrate on bugs that are highly impactful. In the literature, high-impact bugs are used to refer to the bugs which appear at unexpected time or locations and bring more unexpected effects (i.e., surprise bugs), or break pre-existing functionalities and destroy the user experience (i.e., breakage bugs). Unfortunately, identifying high-impact bugs from thousands of bug reports in a bug tracking system is not an easy feat. Thus, an automated technique that can identify high-impact bug reports can help developers to be aware of them early, rectify them quickly, and minimize the damages they cause. Considering that only a small proportion of bugs are high-impact bugs, the identification of high-impact bug reports is a difficult task. In this paper, we propose an approach to identify high-impact bug reports by leveraging imbalanced learning strategies. We investigate the effectiveness of various variants, each of which combines one particular imbalanced learning strategy and one particular classification algorithm. In particular, we choose four widely used strategies for dealing with imbalanced data and four state-of-the-art text classification algorithms to conduct experiments on four datasets from four different open source projects. We mainly perform an analytical study on two types of high-impact bugs, i.e., surprise bugs and breakage bugs. The results show that different variants have different performances, and the best performing variants SMOTE (synthetic minority over-sampling technique) + KNN (K-nearest neighbours) for surprise bug identification and RUS (random under-sampling) + NB (naive Bayes) for breakage bug identification outperform the F1-scores of the two state-of-the-art approaches by Thung et al. and Garcia and Shihab.     

Message filters for hardening the Linux kernel

Various mechanisms for hardening the Linux kernel (for example, enforcing system call policies, device driver failure recovery, protection against exploitation of bugs in code) are proposed in the literature. The main problem with these mechanisms is that, they require changes in the kernel code leading to the possibility of introducing new bugs and hence increasing the testing time. We propose a message filter model as an extension to object‐oriented wrappers for the Linux kernel, to dynamically provide various filtering capabilities to the kernel. This model works as a comprehensive framework for specifying system call policies, handling device driver faults, protecting the kernel against exploits of bugs in code etc, without modifying the existing kernel code. This considerably reduces the possibility of creating new bugs in the kernel code. We have integrated policies for system call interception and device driver failure handling, into the Linux kernel (2.6.9), using message filter model. Our experiments show that the overhead due to our filter objects is very low, making it a useful mechanism for providing filtering capabilities to the Linux kernel. Copyright © 2010 John Wiley & Sons, Ltd.     

Generating effective tests for concurrent programs via AI automated planning techniques

Testing concurrent programs is a challenging problem due to interleaving explosion: even for a fixed set of inputs, there is a huge number of concurrent runs that need to be tested to account for scheduler behavior. Testing all possible schedules is not practical. Consequently, most effective testing algorithms only test a select subset of runs. For example, limiting testing to runs that contain data races or atomicity violations has been shown to capture a large proportion of concurrency bugs. In this paper we present a general approach to concurrent program testing that is based on techniques from artificial intelligence (AI) automated planning. We propose a framework for predicting concurrent program runs that violate a collection of generic correctness specifications for concurrent programs, namely runs that contain data races, atomicity violations, or null-pointer dereferences. Our prediction is based on observing an arbitrary run of the program, and using information collected from this run to model the behavior of the program, and to predict new runs that contain bugs with one of the above noted violation patterns. We characterize the problem of predicting such new runs as an AI sequential planning problem with the temporally extended goal of achieving a particular violation pattern. In contrast to many state-of-the-art approaches, in our approach feasibility of the predicted runs is guaranteed and, therefore, all generated runs are fully usable for testing. Moreover, our planning-based approach has the merit that it can easily accommodate a variety of violation patterns which serve as the selection criteria for guiding search in the state space of concurrent runs. This is achieved by simply modifying the planning goal. We have implemented our approach using state-of-the-art AI planning techniques and tested it within the Penelope concurrent program testing framework [35]. Nevertheless, the approach is general and is amenable to a variety of program testing frameworks. Our experiments with a benchmark suite showed that our approach is very fast and highly effective, finding all known bugs.     

BUTTER：一种基于主题模型和异构网络的缺陷分发方法

当软件缺陷被提交到缺陷跟踪系统并经过确认之后,它会被分发给开发人员进行缺陷修复．这个过程就叫做缺陷分发．随着被提交到系统的缺陷报告日益增多,手工分发缺陷报告会变得越来越困难．提出了一种自动分发缺陷的方法BUTTER．与其他方法不同的是,BUTTER不仅利用主题模型分析缺陷报告中的文本信息,而且创新性地建立了一个包含提交者、缺陷和开发者三种节点及其相互关系的异构网络,从该异构网络中抽取了更多的结构信息．实验证明,BUTTER进行自动缺陷分发较其他缺陷自动分发方法要好．     

What do developers search for on the web?

Developers commonly make use of a web search engine such as Google to locate online resources to improve their productivity. A better understanding of what developers search for could help us understand their behaviors and the problems that they meet during the software development process. Unfortunately, we have a limited understanding of what developers frequently search for and of the search tasks that they often find challenging. To address this gap, we collected search queries from 60 developers, surveyed 235 software engineers from more than 21 countries across five continents. In particular, we asked our survey participants to rate the frequency and difficulty of 34 search tasks which are grouped along the following seven dimensions: general search, debugging and bug fixing, programming, third party code reuse, tools, database, and testing. We find that searching for explanations for unknown terminologies, explanations for exceptions/error messages (e.g., HTTP 404), reusable code snippets, solutions to common programming bugs, and suitable third-party libraries/services are the most frequent search tasks that developers perform, while searching for solutions to performance bugs, solutions to multi-threading bugs, public datasets to test newly developed algorithms or systems, reusable code snippets, best industrial practices, database optimization solutions, solutions to security bugs, and solutions to software configuration bugs are the most difficult search tasks that developers consider. Our study sheds light as to why practitioners often perform some of these tasks and why they find some of them to be challenging. We also discuss the implications of our findings to future research in several research areas, e.g., code search engines, domain-specific search engines, and automated generation and refinement of search queries.     

1553B接口仿真测试系统设计及典型软件缺陷分析

介绍了一种1553B接口仿真测试软件硬件设计方案,详细介绍了自动化测试引擎设计以及Lua脚本语言的测试流程设计,并以某装备软件1553B通信接口测试中发现的一些具有代表性的接口问题为例,对1553B软件接口测试典型案例的测试设计、测试结果进行了较为详细的描述,介绍了如何设计有效的软件测试用例,高效地发现通信软件的设计缺陷和程序问题,提升了软件的质量.