A rule-based software test data generator

Rule-based software test data generation is proposed as an alternative to either path/predicate analysis or random data generation. A prototype rule-based test data generator for Ada programs is constructed and compared to a random test data generator. Four Ada procedures are used in the comparison. Approximately 2000 rule-based test cases and 100000 randomly generated test cases are automatically generated and executed. The success of the two methods is compared using standard coverage metrics. Simple statistical tests showing that even the primitive rule-based test data generation prototype is significantly better than random data generation are performed. This result demonstrates that rule-based test data generation is feasible and shows great promise in assisting test engineers, especially when the rule base is developed further     

Model management system for IRT-based test construction decision support system

Decision support system (DSS) has become widespread for some specific domains in recent years. However, DSS for IRT-based (item response theory) test construction has not yet been developed. This domain basically imposes a semi-structured or unstructured decision and, therefore, involves a very complex modeling process. This study develops a model management system (MMS) architecture to assist a non-expert user in manipulating test construction process efficiently and effectively. This architecture consists of four components: problem analysis, model type selection, model formulation and solver. The model type selection subsystem is further organized into three levels of hierarchy, i.e., environment, structure and parameter. A prototype is presented to demonstrate the feasibility of this architecture. The results indicate that this approach can be applied for providing an integrated, flexible and user-friendly DSS environment for producing better quality of results in less solution time.     

Abstraction and refinement of mathematical functions toward SMT-based test-case generation

We propose a novel approach for generating test cases of software that includes mathematical functions, such as trigonometric functions, logarithmic functions, functions implemented as look-up tables with non-linear interpolation, and so on. A satisfiability modulo theories (SMT) solver is iteratively used to generate test cases in the scheme of bounded model checking. In the proposed method, mathematical functions are abstracted so that the derived formula can be easily treated using an SMT solver. The abstraction is refined adaptively based on the previous counterexamples. We also propose a general method to estimate an abstraction of a mathematical function by means of sampling and machine learning. Although the method proposed in this paper addresses mainly the topic of test-case generation, it is also applicable to ordinary bounded model checking under the assumption that the abstraction should be a correct over-approximation. We evaluated the proposed method by applying it to an example of embedded control software taken from the automotive industry. The experimental results show the usefulness of the proposed method.     

Integrating LP-guided variable fixing with MIP heuristics in the robust design of hybrid wired-wireless FTTx access networks

This study investigates how to model and solve the problem of optimally designing FTTx telecommunications access networks integrating wired and wireless technologies, while taking into account the uncertainty of wireless signal propagation. We propose an original robust optimization model for the related robust 3-architecture Connected Facility Location problem, which includes additional variables and constraints to model wireless signal coverage represented through signal-to-interference ratios. Since the resulting robust problem can prove very challenging even for a modern state-of-the art optimization solver, we propose to solve it by an original primal heuristic that combines a probabilistic variable fixing procedure, guided by peculiar Linear Programming relaxations, with a Mixed Integer Programming heuristic, based on an exact very large neighborhood search. A numerical study carried out on a set of realistic instances show that our heuristic can find solutions of much higher quality than a state-of-the-art solver.     

Estimating software testing complexity

ContextComplexity measures provide us some information about software artifacts. A measure of the difficulty of testing a piece of code could be very useful to take control about the test phase.ObjectiveThe aim in this paper is the definition of a new measure of the difficulty for a computer to generate test cases, we call it Branch Coverage Expectation (BCE). We also analyze the most common complexity measures and the most important features of a program. With this analysis we are trying to discover whether there exists a relationship between them and the code coverage of an automatically generated test suite.MethodThe definition of this measure is based on a Markov model of the program. This model is used not only to compute the BCE, but also to provide an estimation of the number of test cases needed to reach a given coverage level in the program. In order to check our proposal, we perform a theoretical validation and we carry out an empirical validation study using 2600 test programs.ResultsThe results show that the previously existing measures are not so useful to estimate the difficulty of testing a program, because they are not highly correlated with the code coverage. Our proposed measure is much more correlated with the code coverage than the existing complexity measures.ConclusionThe high correlation of our measure with the code coverage suggests that the BCE measure is a very promising way of measuring the difficulty to automatically test a program. Our proposed measure is useful for predicting the behavior of an automatic test case generator.     

遗传算法辅助的动态符号执行测试方法

动态符号执行是一种有效的软件测试方法,但由于受到约束求解器求解能力的限制,在面对较为复杂的程序和路径条件时,动态符号执行的路径覆盖率还有待提升。针对上述问题,提出了一种遗传算法辅助的动态符号执行测试方法,并基于此方法实现了原型工具JDart-Ga。该方法结合遗传算法的优势,生成约束求解器无法求解的约束条件对应测试输入,从而提升动态符号执行的路径覆盖率。实验结果表明,在测试存在动态符号执行无法覆盖路径的3个实验对象时,所提出方法的路径覆盖率与JDart相比分别提升了16%至23%。     

基于FPGA的数据域边界扫描测试向量发生器的设计与实现

设计了一种基于FPGA的边界扫描测试向量发生器,该发生器可以为边界扫描故障诊断系统提供测试向量,并可计算测试向量的故障覆盖率.与以往通过软件提供测试向量的方法相比,该设计在速度和效率上有了较大提高.     

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.     

使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。     

Generalization of queueing network product form solutions tostochastic Petri nets

A new solution is given for the steady-state probability computation of closed synchronized queuing networks. A closed synchronized queuing network is a particular Markov stochastic Petri net (a bounded and monovaluated Petri net with a strongly connected reachability graph and constant firing rates independent of markings). It is shown that the steady-state probability distribution can be expressed using matrix products. The results generalize the Gordon-Newell theorem. The solution is similar to the Gordon-Newell product form using matrix and vectors instead of scalars. A prototype solver developed from this result is presented     

Bounded model checking of software using SMT solvers instead of SAT solvers

C bounded model checking (cbmc) has proved to be a successful approach to automatic software analysis. The key idea is to (i) build a propositional formula whose models correspond to program traces (of bounded length) that violate some given property and (ii) use state-of-the-art SAT solvers to check the resulting formulae for satisfiability. In this paper, we propose a generalisation of the cbmc approach on the basis of an encoding into richer (but still decidable) theories than propositional logic. We show that our approach may lead to considerably more compact formulae than those obtained with cbmc. We have built a prototype implementation of our technique that uses a satisfiability modulo theories (SMT) solver to solve the resulting formulae. Computer experiments indicate that our approach compares favourably with—and on some significant problems outperforms—cbmc.     

基于构件的信息系统开发框架

本文在研究了基于构件的信息系统体系结构基础上，提出了基于构件的信息系统的开发框架，其中可重用构件是其重要的一部分。该框架可以看作是一个基于构件的“标准”的原型系统，类似于一个构件化信息系统产生器，通过该框架可迅速生成一个构件化的信息系统。     

存储器模块测试系统的设计

存储器模块上集成有多种类型的存储器,整个模块提供一致的总线访问接口;对存储器模块进行完整的测试是很有必要的,在分析存储器模块的故障模型和测试原理的基础上,给出了一种基于数字波形发生器的存储器模块测试设备结构,通过对March算法进行扩展,设计了一种适合对存储器模块进行测试的算法结构;系统提高了测试的故障覆盖率和效率,在应用中取得了较好的效果.     

基于改进鲸鱼优化的覆盖表生成算法

为提高组合测试中覆盖表生成效率,基于覆盖表生成的离散性,提出一种改进的鲸鱼优化算法。该算法首先利用编码转换的思想,将鲸鱼个体连续运动方式编码为适用于覆盖表的离散方式;其次,在算法的开发与搜索阶段加入迭代演化算子,以提高算法的全局搜索能力;最后,针对覆盖表生成中算法本身的局限问题,使用平均海明距离跳出局部最优,并通过约束求解器和惩罚函数法增加约束处理机制,以提高算法实际应用能力。实验结果表明,与其它已有算法相比,所提出的算法在覆盖表生成规模上具有更好的优势。     

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.     

Exploiting deterministic TPG for path delay testing

Detection of path delay faults requires two-pattern tests.BIST technique provides a low-cost test solution.This paper proposes an approach to designing a cost-effective deterministic test pattern generator(IPG) for path delay testing.Given a set of pre-generated test-pattern generator(TPG) for path delay testing.Given a set of pre-generated test-pairs with pre-determined fault coverage,a deterministic TPG is synthesized to apply the given test-pair set in a limited test time.To achieve this objective,configuable linear feedback shift register(LFSR)structures are used.Techniques are developed to synthesize such a TPG.which is used to generate an unordered deterministic test-pair set.The resulting TPG is very efficient in terms of hardware size and speed performance.SImulation of academic benchmark circuits has given good results when compared to alternative solutions.     

嵌入式处理器在片调试功能的验证

以龙芯1号处理器为研究对象,探讨了基于JTAG的处理器在片调试功能的验证方法.根据在片调试的结构特征建立了功能覆盖率模型,并以访存模式为基准分步建立虚拟验证原型.整个验证将定向功能测试和指令集随机测试有机地结合起来,迅速定位了设计中多个难以发现的错误.最终验证的功能覆盖率达到100%,FPGA原型经长时间运行无误.     

基于SAT的多目标故障测试向量动态压缩方法

针对传统的自动测试图形向量生成采用逐个求解单一故障模型导致生成测试向量数据量巨大的缺点, 提出一种基于布尔满足性(boolean satisfiability, SAT)的多目标故障测试向量动态压缩方法, 同时论证多目标故障测试生成问题为布尔满足性问题。该方法将具有鲁棒性的SAT算法嵌入经典的动态压缩流程中, 首先利用经典动态压缩算法求解最小测试向量检测大部分失效故障, 然后采用SAT求解器对未测出的多故障电路进行同一求解和附加约束求解方式, 最终得到故障覆盖率高的测试向量和同一测试最大故障列表。实验数据表明, 在相同电路模型情况下, 此方法求得的测试向量相比经典动态压缩减少高达70%。     

Modelling demand response in organized wholesale energy markets

We propose a bi-level optimization model for demand response in organized wholesale energy markets. In this model, the lower level performs the economic dispatch of energy and generates the price and the upper level minimizes the total amount of demand response subject to a net benefit requirement. In an economic sense, demand response is a trade of ‘consuming rights’ instead of a sale of energy. Therefore it must be traded separately from the energy market. Although a bi-level optimization model is very hard to solve in general, we demonstrate that realistic power networks have characteristics that can be exploited to reduce the effective size of the problem instance. In particular, we transform the nonconvex net benefit test constraint to an equivalent linear form, and reformulate the nonconvex complementarity conditions of doubly bounded variables using SOS2 constraints. For realistic instances of the MPEC, we employ a three-phase approach that exploits the fast local solution from a nonlinear programming solver as well as LP-based bound strengthening within a mixed integer/SOS2 formulation. The model is tested against various data cases and settings, and generates useful insight for demand response dispatch operations in practice.