Controlling test case explosion in test generation from B formal models

BZ‐TESTING‐TOOLS (BZ‐TT) is a tool set for automated test case generation from B and Z specifications. BZ‐TT uses boundary and cause–effect testing on the basis of the formal model. It has been used and validated on several industrial applications in the domain of critical software, particularly smart card and transport systems. This paper presents the test coverage criteria supported by BZ‐TT. On the one hand, these correspond to various classical structural coverage criteria, but specialized to the case of B abstract machines. The paper gives algorithms for these in Prolog. On the other hand, BZ‐TT introduces new coverage criteria for complex data structures, based on boundary analysis: this paper defines weak and strong state‐boundary coverage, input‐boundary coverage and output‐boundary coverage. Finally, the paper describes how BZ‐TT presents a unified view of these criteria to the validation engineer, and allows him or her to control the test case explosion on a coarse basis (choosing from a range of coverage criteria) as well as a fine basis (selecting options for each state or input variable). Copyright © 2004 John Wiley & Sons, Ltd.     

Issues in using model checkers for test case generation

The use of model checkers for automated software testing has received some attention in the literature: It is convenient because it allows fully automated generation of test suites for many different test objectives. On the other hand, model checkers were not originally meant to be used this way but for formal verification, so using model checkers for testing is sometimes perceived as a “hack”. Indeed, several drawbacks result from the use of model checkers for test case generation. If model checkers were designed or adapted to take into account the needs that result from the application to software testing, this could lead to significant improvements with regard to test suite quality and performance. In this paper we identify the drawbacks of current model checkers when used for testing. We illustrate techniques to overcome these problems, and show how they could be integrated into the model checking process. In essence, the described techniques can be seen as a general road map to turn model checkers into general purpose testing tools.     

面向测试的构件系统模型及测试用例生成方法

随着面向构件的软件开发方法的广泛应用,构件系统的描述和测试成为保证软件质量的关键所在。由于构件系统的复杂性和开发方法的特殊性,用传统方法对构件系统进行集成测试往往面对很多困难。提出了一种改进的面向测试的构件描述模型,称为TCSM,它着重对构件系统中的构件间的交互和约束进行了动态描述,为构件系统集成测试阶段的功能测试和边界测试等提供了大量可用信息。在此基础上,进一步提出一种把TCSM转换成测试模型的方法,以UML协作图模型为原型,实现了构件系统从描述模型到测试模型的自动转换。最后,实现了一种在所产生的测试模型上自动生成测试用例的算法。TCSM更好地描述了构件的交互行为信息,进一步实现了系统的自动化测试,减少了通常需要在构件系统搭建完成后,针对测试对系统手工建立测试模型的工作,提高了构件系统开发的效率和可靠性。     

Test sequence generation and model checking using dynamic transition relations

The task of finding a set of test sequences that provides good coverage of industrial circuits is infeasible because of the size of the circuits. For small critical subcircuits of the design, however, designers can create a set of test sequences that achieve good coverage. These sequences cannot be used on the full design because the inputs to the subcircuit may not be accessible. In this work we present an efficient test generation algorithm that receives a test sequence created for the subcircuit and finds a test sequence for the full design that reproduces the given sequence on the subcircuit. The algorithm uses a new technique called dynamic transition relations to increase its efficiency .The most common and most expensive step in our algorithm is the computation of the set of predecessors of a set of states. To make this computation more efficient we exploit a partitioning of the transition relation into a set of simpler relations. At every step we use only those that are necessary, resulting in a smaller relation than the original one. A different relation is used for each step, hence the name dynamic transition relations. The same idea can be used to improve symbolic model checking for the temporal logic CTL.We have implemented the new method in SMV and run it on several large circuits. Our experiments indicate that the new method can provide gains of up to two orders of magnitude in time and space during verification. These results show that dynamic transition relations can make it possible to verify circuits that were previously unmanageable due to their size and complexity .     

Modelling and Verification of Real-Time Publish and Subscribe Protocol Using Uppaal and Simulink/Stateflow

Journal of Computer Science and Technology - Real-Time Publish and Subscribe (RTPS) protocol is a protocol for implementing message exchange over an unreliable transport in data distribution...     

A dynamic stochastic model for automatic grammar‐based test generation

Grammar‐based test generation provides a systematic approach to producing test cases from a given context‐free grammar. Unfortunately, naive grammar‐based test generation is problematic because of the fact that exhaustive random test case production is often explosive, and grammar‐based test generation with explicit annotation controls often causes unbalanced testing coverage. In this paper, we present an automatic grammar‐based test generation approach, which takes a symbolic grammar as input, requires zero control input from users, and produces well‐distributed test cases. Our approach utilizes a novel dynamic stochastic model where each variable is associated with a tuple of probability distributions, which are dynamically adjusted along the derivation. We further present a coverage tree illustrating the distribution of generated test cases and their detailed derivations. More importantly, the coverage tree supports various implicit derivation control mechanisms. We implemented this approach in a Java‐based system, named Gena. Each test case generated by Gena automatically comes with a set of structural features, which can play an important and effective role on automated failure causes localization. Experimental results demonstrate the effectiveness of our approach, the well‐balanced distribution of generated test cases over grammatical structures, and a case study on grammar‐based failure causes localization. Copyright © 2014 John Wiley & Sons, Ltd.     

Automatic test case generation for structural testing of function block diagrams

ContextFunction Block Diagram (FBD) is increasingly used in safety-critical applications. Test coverage issues for FBDs are frequently raised by regulators and users. However, there is little work at this aspect on testing FBD at model level. Our previous study has designed a new data-flow test coverage criterion, FB-Path Complete Condition Test Coverage (FPCC), that can directly test FBD structures and effectively detect function mutation errors. Nevertheless, because FPCC scheme involves several data-flow concepts and thus it is somewhat complicated to comprehend and to generate FPCC-complied test cases. An automatic test suite generator for FPCC is highly desirable.ObjectiveThis study designs an automatic test case generator, FPCCTestGen, for FPCC so as to enhance the practicability and acceptance of the FPCC approach.MethodFirst, a supporting infrastructure for performing automatic FBD-to-UPPAAL-for-FPCC transformation is designed. The supporting infrastructure includes templates, declarations, and functions as building blocks for transformation. Then, for each input FBD, represented in PLCopen XML format, FPCCTestGen performs parsing and converts FBD components into corresponding UPPAAL model components using aforementioned building blocks. After that, queries related to FPCC characteristics are submitted to UPPAAL model checker for verification. Finally, the verification traces are analyzed to obtain a FPCC-complied test suite.ResultsA safety injection system is used as a case study. Preliminary results show that the generated test suite achieves the highest FPCC percentage with a near optimal number of test cases.ConclusionThis automatic test case generation tool is effective and thus, can promote the use of the new test coverage criterion. Methodology used in FPCCTestGen is generic and can be applied to test suite generation for other test criteria on data-flow programs.     

用模型检验产生约简测试集

基于模型检验的自动化测试技术已经得到普遍应用,由于测试用例自动化生成过程中会产生巨大的资源消耗,优化问题越来越受到软件测试行业的广泛关注。提出一种基于节点权重的性质覆盖度计算方法,在模型检验器自动化生成测试用例之前对测试目标排序,能够更有效地检测到冗余性质,从而减少模型检验器被调用执行次数并且避免大规模的测试用例生成。     

Test data regeneration: generating new test data from existing test data

Existing automated test data generation techniques tend to start from scratch, implicitly assuming that no pre‐existing test data are available. However, this assumption may not always hold, and where it does not, there may be a missed opportunity; perhaps the pre‐existing test cases could be used to assist the automated generation of additional test cases. This paper introduces search‐based test data regeneration, a technique that can generate additional test data from existing test data using a meta‐heuristic search algorithm. The proposed technique is compared to a widely studied test data generation approach in terms of both efficiency and effectiveness. The empirical evaluation shows that test data regeneration can be up to 2 orders of magnitude more efficient than existing test data generation techniques, while achieving comparable effectiveness in terms of structural coverage and mutation score. Copyright © 2010 John Wiley & Sons, Ltd.     

基于GA-PSO算法的路径测试数据自动生成*

为了实现测试数据自动生成,许多遗传算法及其改进算法应用到了测试领域。针对遗传算法具有较强的全局搜索能力,但局部搜索能力较弱,且收敛速度慢的特点。将遗传算法与粒子群算法结合起来形成新的混合算法（GA-PSO）,并成功应用到软件测试数据自动生成过程中。实验结果表明,该算法结合了遗传算法和粒子群算法的优点,在保证软件测试数据正确生成的情况下,极大地提高了数据生成的效率。     

Seeding strategies in search‐based unit test generation

Search‐based techniques have been applied successfully to the task of generating unit tests for object‐oriented software. However, as for any meta‐heuristic search, the efficiency heavily depends on many factors; seeding, which refers to the use of previous related knowledge to help solve the testing problem at hand, is one such factor that may strongly influence this efficiency. This paper investigates different seeding strategies for unit test generation, in particular seeding of numerical and string constants derived statically and dynamically, seeding of type information and seeding of previously generated tests. To understand the effects of these seeding strategies, the results of a large empirical analysis carried out on a large collection of open‐source projects from the SF110 corpus and the Apache Commons repository are reported. These experiments show with strong statistical confidence that, even for a testing tool already able to achieve high coverage, the use of appropriate seeding strategies can further improve performance. © 2016 The Authors. Software Testing, Verification and Reliability Published by John Wiley & Sons Ltd.     

Grammar‐based test generation with YouGen

Grammars are traditionally used to recognize or parse sentences in a language, but they can also be used to generate sentences. In grammar‐based test generation (GBTG), context‐free grammars are used to generate sentences that are interpreted as test cases. A generator reads a grammar G and generates L(G), the language accepted by the grammar. Often L(G) is so large that it is not practical to execute all of the generated cases. Therefore, GBTG tools support ‘tags’: extra‐grammatical annotations which restrict the generation. Since its introduction in the early 1970s, GBTG has become well established: proven on industrial projects and widely published in academic venues. Despite the demonstrated effectiveness, the tool support is uneven; some tools target specific domains, e.g. compiler testing, while others are proprietary. The tools can be difficult to use and the precise meaning of the tags are sometimes unclear. As a result, while many testing practitioners and researchers are aware of GBTG, few have detailed knowledge or experience. We present YouGen, a new GBTG tool supporting many of the tags provided by previous tools. In addition, YouGen incorporates covering‐array tags, which support a generalized form of pairwise testing. These tags add considerable power to GBTG tools and have been available only in limited form in previous GBTG tools. We provide semantics for the YouGen tags using parse trees and a new construct, generation trees. We illustrate YouGen with both simple examples and a number of industrial case studies. Copyright © 2010 John Wiley & Sons, Ltd.     

Evolutionary algorithms for the multi‐objective test data generation problem

Automatic test data generation is a very popular domain in the field of search‐based software engineering. Traditionally, the main goal has been to maximize coverage. However, other objectives can be defined, such as the oracle cost, which is the cost of executing the entire test suite and the cost of checking the system behavior. Indeed, in very large software systems, the cost spent to test the system can be an issue, and then it makes sense by considering two conflicting objectives: maximizing the coverage and minimizing the oracle cost. This is what we did in this paper. We mainly compared two approaches to deal with the multi‐objective test data generation problem: a direct multi‐objective approach and a combination of a mono‐objective algorithm together with multi‐objective test case selection optimization. Concretely, in this work, we used four state‐of‐the‐art multi‐objective algorithms and two mono‐objective evolutionary algorithms followed by a multi‐objective test case selection based on Pareto efficiency. The experimental analysis compares these techniques on two different benchmarks. The first one is composed of 800 Java programs created through a program generator. The second benchmark is composed of 13 real programs extracted from the literature. In the direct multi‐objective approach, the results indicate that the oracle cost can be properly optimized; however, the full branch coverage of the system poses a great challenge. Regarding the mono‐objective algorithms, although they need a second phase of test case selection for reducing the oracle cost, they are very effective in maximizing the branch coverage. Copyright © 2011 John Wiley & Sons, Ltd.     

Automatic form generation

The Acuity project, in support of a collaborative brain‐tumor research effort, provides WWW‐based input forms implemented as Java applets for updating a WWW‐accessible database. The continuing need to develop new, but closely related, input forms motivated the design and implementation of the Acuity Form Generator (AFG), an automatic form‐generation tool. This paper documents the AFG technology. Copyright © 2002 John Wiley & Sons, Ltd.     

Java存储过程的自动生成与测试

通过定义存储过程模板,并根据表信息替换模板中的变量,从而生成大量具有类似处理流程的Java存储过程.给出了Update存储过程的生成模板、注册模板以及测试程序模板,并用VBA实现了自动生成Java存储过程的主要方法,还讨论了测试数据的准备、测试及测试结果的确认方法.实践表明,该方法能保证软件的质量、缩短开发周期以及提高软件的可修改性.     

Automatic, evolutionary test data generation for dynamic software testing

This paper proposes a dynamic test data generation framework based on genetic algorithms. The framework houses a Program Analyser and a Test Case Generator, which intercommunicate to automatically generate test cases. The Program Analyser extracts statements and variables, isolates code paths and creates control flow graphs. The Test Case Generator utilises two optimisation algorithms, the Batch-Optimistic (BO) and the Close-Up (CU), and produces a near to optimum set of test cases with respect to the edge/condition coverage criterion. The efficacy of the proposed approach is assessed on a number of programs and the empirical results indicate that its performance is significantly better compared to existing dynamic test data generation methods.     

软件测试用例自动生成算法综述*

按照测试用例自动生成技术的不同,将测试用例自动生成算法分为随机、遗传、蚁群、粒子群四类,对上述各类算法的现状和进展进行介绍、分析和探讨。最后,对软件测试用例自动生成的研究进行了总结。     

基于OBDD的SMC反例生成研究

针对传统的符号模型检测反例生成算法在生成反例时会产生大量的无关变量,使得反例难以理解。提出一种改进的反例生成算法,将反例中的状态扩展为一个状态集,使用零压缩二叉决策图(Zero-Suppressed Binary Decision Diagrams,ZBDD)来存储所求出的状态集。删除了系统中的无关变量,仅保留了相关的变量,实验表明该算法能有效地减少状态的变量数,减少存储反例所需的空间。     

基于动态集合进化算法的弱变异测试用例集生成

为解决基于集合进化算法（SEA）的弱变异测试用例集生成过程中个体规模固定和执行开销大的问题,提出一种基于动态集合进化算法（DSEA）的弱变异测试用例集生成方法。以测试用例集为个体,生成覆盖所有变异分支的弱变异测试用例集。在进化过程中,集合精简算子根据最优个体的最小子集及其未覆盖变异分支数量计算所需测试用例集的最小规模,并基于该最小规模调整种群中所有个体的规模,以生成最小规模的弱变异测试用例集,同时设计了适用于评估以测试用例集为个体的适应度函数。实验结果表明,动态集合进化算法指导弱变异测试用例集生成,获得的测试用例集规模比个体初始规模平均约简了50.15%,执行时间比集合进化的弱变异测试用例集生成最多降低了74.58%。因此,动态集合进化算法为最小规模的弱变异测试用例集生成和提升算法速度提供了一种解决方案。     

Declarative paradigm of test coverage

Two facts about declarative programming prevent the application of conventional testing methods. First, the classical test coverage measures such as statement, branch or path coverage, cannot be used, since in declarative programs no control flow notion exists. Second, there is no widely accepted language available for formal specification, since predicate logic, which is the most common formalism for declarative programming, is already a very high-level abstract language. This paper presents a new approach exending previous work by the authors on test input generation for declarative programs. For this purpose, the existing program instrumentation notion is extended and a new logic coverage measure is introduced. The approach is mathematically formalized and the goal of achieving 100% program logic coverage controls the automatic test input generation. The method is depicted by means of logic programming; the results are, however, generally applicable. Finally, the concepts introduced have been used practically within a test environment. © 1998 John Wiley & Sons, Ltd.