In RESTful APIs, interactions with a database are a common and crucial aspect. When generating white-box tests, it is essential to consider the database’s state (i.e., the data contained in the database) to achieve higher code coverage and uncover more hidden faults. This article presents novel techniques to enhance search-based software test generation for RESTful APIs interacting with NoSQL databases. Specifically, we target the popular MongoDB database by dynamically analyzing its state—via automated code instrumentation—during test generation, with the goal of producing non-empty results for the queries executed by the generated tests. Additionally, to achieve better results, our novel approach also allows inserting automatically generated NoSQL data directly from test cases. This is particularly beneficial when testing read-only microservices, or when it is challenging or time-consuming to generate the correct sequence of HTTP calls to populate the NoSQL database. Our novel techniques are implemented as an extension of EvoMaster, the only open-source tool for white-box fuzzing RESTful APIs. Experiments conducted on six RESTful APIs demonstrated significant improvements in code coverage, with increases of up to 18% compared to existing white-box approaches. To better highlight the improvements of our novel techniques, comparisons are also carried out with four state-of-the-art black-box fuzzers.

Smart contracts manage valuable assets, and their immutability hinders bug fixing. Therefore, pre-deployment verification and validation are critical. In fact, auditing has become mandatory in the pipeline of smart contract development. Auditors usually combine manual inspection with automated tools in their auditing work, looking for issues that may be domain dependent (i.e., pertaining to the correct implementation of requirements-which are often informal, partial, and implicit) or independent (e.g., reentrancy, overflow, etc.), To identify domain dependent issues, it is important to understand the non-trivial behavior of the implementation over sequences of calls made by callees playing different roles in the contract. In this paper, we propose a novel approach that combines predicate abstraction with modal transition systems to build abstractions that can help auditors in the smart contract validation process. The required inputs are a set of predicates provided as code and, optionally, constraints over smart contract function parameters. The output is a modal transition system that captures the contract's behavior. We report on a prototype that builds modal abstractions and an evaluation on two established benchmarks where we identified four previously unreported issues.

In this paper, we present the latest version 3.0.0 of EvoMaster, an open-source search-based fuzzer aimed at Web APIs. We discuss and present all its recent improvements, including advanced white-box heuristics, advanced search algorithms, support for databases and external services, as well as dealing with GraphQL and RPC APIs besides the original use case for REST APIs. The tool's installers have been downloaded more than 3000 times. EvoMaster is in daily use for fuzzing millions of lines of code in hundreds of APIs in large Fortune 500 companies, such as for example the e-commerce Meituan.

The ESPRESSO testing framework for ANDROID has gained popularity among developers as it allows to write concise and reliable VI tests. State-of-the-art tools for automatically testing ANDROID apps, however, tend to produce crash reports rather than human-readable tests, and even if they produce tests these (1) rarely use the ESPRESSO format; (2) are often unreliable due to the volatile nature of widget identifiers; and (3) usually contain no test assertions to serve as regression oracles. While the lack of ESPRESSO support of test generation tools has been addressed by reverse engineering ESPRESSO tests, the other problems remain even with this workaround. In this paper, we therefore introduce a novel ESPREsso-based representation that allows test generators to generate ESPRESSO test cases directly that (1) can reliably identify widgets using clear and concise ESPRESSO selectors, and (2) can check test executions using ESPRESSO assertions. Experiments on 1,035 ANDROID apps demonstrate that the proposed approach generates ESPRESSO tests that are significantly more reliable than reverse engineered tests, and the ESPRESSO assertions of the generated tests are effective at detecting faults in ANDROID apps.

Due to its importance and widespread use in industry, automated testing of REST APIs has attracted major interest from the research community in the last few years. However, most of the work in the literature has been focused on black-box fuzzing. Although existing fuzzers have been used to automatically find many faults in existing APIs, there are still several open research challenges that hinder the achievement of better results (e.g., in terms of code coverage and fault finding). For example, under-specified schemas are a major issue for black-box fuzzers. Currently, EvoMaster is the only existing tool that supports white-box fuzzing of REST APIs. In this paper, we provide a series of novel white-box heuristics, including for example how to deal with under-specified constrains in API schemas, as well as under-specified schemas in SQL databases. Our novel techniques are implemented as an extension to our open-source, search-based fuzzer EvoMaster . An empirical study on 14 APIs from the EMB corpus, plus one industrial API, shows clear improvements of the results in some of these APIs.

Web Services like REST, GraphQL and RPC APIs are widely used in industry. They form the backends of modern Cloud Applications. In recent years, there has been an increase interest in the research community about fuzzing web services. However, there is no clear, common benchmark in the literature that can be used for comparing techniques and ease experimentation. Even if nowadays it is not so difficult to find web services on open-source repositories such as GitHub, quite a bit of work might be required to setup databases and authentication information (e.g., hashed passwords). Furthermore, how to start and stop the applications might vary greatly among the different frameworks (e.g., Spring and DropWizard) used to implement such services. For all these reasons, since 2017 we have created and maintained a corpus of web services called EMB, together with all the tooling and configurations needed to run software testing experiments. Originally, EMB was created for evaluating the fuzzer EvoMaster, but it can be (and has been) used by other tools/researchers as well. This paper discusses how EMB is designed and how its libraries can be used to run experiments on these APIs. An introductory video for EMB can be currently accessed at https://youtu.be/wJs34ATgLEw

Abstract Several tools for automatically testing Android applications have been proposed. In particular, Sapienz is a search‐based tool that has been recently deployed in an industrial setting. Although it has been shown that Sapienz outperforms several state‐of‐the‐art tools, it is still to be seen what features of SAPIENZ impact the most on its effectiveness. We conducted an extensive empirical study where we compare the impact of the search algorithm and the usage of motif genes, a more compact representation of individuals. Our empirical study shows that the usage of motif genes improves coverage both for Evolutionary Algorithms and random approaches. In particular, it also shows that NSGA‐II, the multi‐objective evolutionary algorithm used by Sapienz, does not have a clear improvement over other algorithms. In terms of number of crashes detected, our study shows that both NSGA‐II and Random Search perform similarly. While the usage of motif genes improves the crash detection of algorithms, it is not enough to make it statistically significant. These facts cast doubts about the use of Evolutionary Algorithms in the context of Android test generation and suggest that motif genes can have a great impact on the overall effectiveness.

Research in software testing often involves the development of software prototypes. Like any piece of software, there are challenges in the development, use and verification of such tools. However, some challenges are rather specific to this problem domain. For example, often these tools are developed by PhD students straight out of bachelor/master degrees, possibly lacking any industrial experience in software development. Prototype tools are used to carry out empirical studies, possibly studying different parameters of novel designed algorithms. Software scaffolding is needed to run large sets of experiments efficiently. Furthermore, when using AI-based techniques like evolutionary algorithms, care needs to be taken to deal with their randomness, which further complicates their verification. The aforementioned represent some of the challenges we have identified for this domain. In this paper, we report on our experience in building the open-source EvoMaster tool, which aims at system-level test case generation for enterprise applications. Many of the challenges we faced would be common to any researcher needing to build software testing tool prototypes. Therefore, one goal is that our shared experience here will boost the research community, by providing concrete solutions to many development challenges in the building of such kind of research prototypes. Ultimately, this will lead to increase the impact of scientific research on industrial practice.

Summary Researchers and practitioners have designed and implemented various automated test case generators to support effective software testing. Such generators exist for various languages (e.g., Java, C#, or Python) and various platforms (e.g., desktop, web, or mobile applications). The generators exhibit varying effectiveness and efficiency, depending on the testing goals they aim to satisfy (e.g., unit‐testing of libraries versus system‐testing of entire applications) and the underlying techniques they implement. In this context, practitioners need to be able to compare different generators to identify the most suited one for their requirements, while researchers seek to identify future research directions. This can be achieved by systematically executing large‐scale evaluations of different generators. However, executing such empirical evaluations is not trivial and requires substantial effort to select appropriate benchmarks, setup the evaluation infrastructure, and collect and analyse the results. In this Software Note, we present ourJUnit Generation Benchmarking Infrastructure(JUGE) supporting generators (search‐based, random‐based, symbolic execution, etc.) seeking to automate the production of unit tests for various purposes (validation, regression testing, fault localization, etc.). The primary goal is to reduce the overall benchmarking effort, ease the comparison of several generators, and enhance the knowledge transfer between academia and industry by standardizing the evaluation and comparison process. Since 2013, several editions of a unit testing tool competition, co‐located with the Search‐Based Software Testing Workshop, have taken place whereJUGEwas used and evolved. As a result, an increasing amount of tools (over 10) from academia and industry have been evaluated onJUGE, matured over the years, and allowed the identification of future research directions. Based on the experience gained from the competitions, we discuss the expected impact ofJUGEin improving the knowledge transfer on tools and approaches for test generation between academia and industry. Indeed, theJUGEinfrastructure demonstrated an implementation design that is flexible enough to enable the integration of additional unit test generation tools, which is practical for developers and allows researchers to experiment with new and advanced unit testing tools and approaches.

Several tools have been proposed to automatically test Android applications, achieving outstanding results in terms of both code coverage and crash discovery. While useful for crash reproduction and bug-fixing, these tools usually do not present the generated interactions in a format that motivates developers to read and modify such tests later on. This hinders the ability of developers to add those tests to their existing test suites, or adapt them to new scenarios - common practices in modern software development where tests are maintained and evolve alongside production code.

Smart contracts are immutable programs deployed on the blockchain that can manage significant assets. Because of this, verification and validation of smart contracts is of vital importance. Indeed, it is industrial practice to hire independent specialized companies to audit smart contracts before deployment. Auditors typically rely on a combination of tools and experience but still fail to identify problems in smart contracts before deployment, causing significant losses. In this paper, we propose using predicate abstraction to construct models which can be used by auditors to explore and validate smart contact behaviour at the function call level by proposing predicates that expose different aspects of the contract. We propose predicates based on requires clauses and enum-type state variables as a starting point for contract validation and report on an evaluation on two different benchmarks.

Search-based software testing (SBST) has been shown to be an effective technique to generate test cases automatically. Its effectiveness strongly depends on the guidance of the fitness function. Unfortunately, a common issue in SBST is the so-called flag problem , where the fitness landscape presents a plateau that provides no guidance to the search. In this article, we provide a series of novel testability transformations aimed at providing guidance in the context of commonly used API calls (e.g., strings that need to be converted into valid date/time objects). We also provide specific transformations aimed at helping the testing of REST Web Services. We implemented our novel techniques as an extension to EvoMaster , an SBST tool that generates system-level test cases. Experiments on nine open-source REST web services, as well as an industrial web service, show that our novel techniques improve performance significantly.

A significant proportion of classes in modern software introduce or use object protocols, prescriptions on the temporal orderings of method calls on objects. This article studies search-based test generation techniques that aim to exploit a particular abstraction of object protocols (enabledness preserving abstractions (EPAs)) to find failures. We define coverage criteria over an extension of EPAs that includes abnormal method termination and define a search-based test case generation technique aimed at achieving high coverage. Results suggest that the proposed case generation technique with a fitness function that aims at combined structural and extended EPA coverage can provide better failure-detection capabilities not only for protocol failures but also for general failures when compared to random testing and search-based test generation for standard structural coverage.

Search-based software testing (SBST) has been shown to be an effective technique to generate test cases automatically. Its effectiveness strongly depends on the guidance of the fitness function. Unfortunately, a common issue in SBST is the so called flag problem, where the fitness landscape presents a plateau that provides no guidance. In this paper, we provide a series of novel testability transformations aimed at providing guidance in the context of commonly used API calls. An example is when strings need to be converted into valid date/time objects. We implemented our novel techniques as an extension to EVOMASTER, a SBST tool that generates system level test cases. Experiments on six open-source REST web services, and an industrial one, show that our novel techniques improve performance significantly.

Automated system test generation for web/enterprise systems requires either a sequence of actions on a GUI (e.g., clicking on HTML links and form buttons) or direct HTTP calls when dealing with web services (e.g., REST and SOAP). When doing white-box testing of such systems, their code can be analyzed, and the same type of heuristics (e.g., the branch distance ) used in search-based unit testing can be employed to improve performance. However, web/enterprise systems do often interact with a database. To obtain higher coverage and find new faults, the state of the databases needs to be taken into account when generating white-box tests. In this work, we present a novel heuristic to enhance search-based software testing of web/enterprise systems, which takes into account the state of the accessed databases. Furthermore, we enable the generation of SQL data directly from the test cases. This is useful when it is too difficult or time consuming to generate the right sequence of events to put the database in the right state. Also, it is useful when dealing with databases that are “read-only” for the system under test, and the actual data are generated by other services. We implemented our technique as an extension of E VO M ASTER , where system tests are generated in the JUnit format. Experiments on six RESTful APIs (five open-source and one industrial) show that our novel techniques improve coverage significantly (up to +16.5%), finding seven new faults in those systems.

Automated system test generation for web/enterprise systems requires either a sequence of actions on a GUI (e.g., clicking on HTML links), or direct HTTP calls when dealing with web services (e.g., REST and SOAP). However, web/enterprise systems do often interact with a database. To obtain higher coverage and find new faults, the state of the databases needs to be taken into account when generating white-box tests. In this work, we present a novel heuristic to enhance search-based software testing of web/enterprise systems, which takes into account the state of the accessed databases. Furthermore, we enable the generation of SQL data directly from the test cases. This is useful for when it is too difficult or time consuming to generate the right sequence of events to put the database in the right state. And it is also useful when dealing with databases that are ''read-only'' for the system under test, and the actual data is generated by other services. We implemented our technique as an extension of EvoMaster, where system tests are generated in the JUnit format. Experiments on five RESTful APIs show that our novel technique improves code coverage significantly (up to +18%).

Generating unit tests automatically saves time over writing tests manually and can lead to higher code coverage. However, automatically generated tests are usually not based on realistic scenarios, and are therefore generally considered to be less readable. This places a question mark over their practical value: Every time a test fails, a developer has to decide whether this failure has revealed a regression fault in the program under test, or whether the test itself needs to be updated. Does the fact that automatically generated tests are harder to read outweigh the time-savings gained by their automated generation, and render them more of a hindrance than a help for software maintenance? In order to answer this question, we performed an empirical study in which participants were presented with an automatically generated or manually written failing test, and were asked to identify and fix the cause of the failure. Our experiment and two replications resulted in a total of 150 data points based on 75 participants. Whilst maintenance activities take longer when working with automatically generated tests, we found developers to be equally effective with manually written and automatically generated tests. This has implications on how automated test generation is best used in practice, and it indicates a need for research into the generation of more realistic tests.

We describe DynAlloy Analyzer, a tool that extends Alloy Analyzer with support for dynamic elements in Alloy models. The tool builds upon Alloy Analyzer in a way that makes it fully compatible with Alloy models, and extends their syntax with a particular idiom, inspired in dynamic logic, for the description of dynamic behaviours, understood as sequences of states over standard Alloy models, in terms of programs. The syntax is broad enough to accommodate abstract dynamic behaviours, e.g., using nondeterministic choice and finite unbounded iteration, as well as more concrete ones, using standard sequential programming constructions. The analysis of DynAlloy models resorts to the analysis of Alloy models, through an optimized translation that often makes the analysis more efficient than that of typical ad-hoc constructions to capture dynamism in Alloy.

Although automated unit test generation techniques can in principle generate test suites that achieve high code coverage, in practice this is often inhibited by the dependence of the code under test on external resources. In particular, a common problem in modern programming languages is posed by code that involves networking (e.g., opening a TCP listening port). In order to generate tests for such code, we describe an approach where we mock (simulate) the networking interfaces of the Java standard library, such that a search-based test generator can treat the network as part of the test input space. This not only has the benefit that it overcomes many limitations of testing networking code (e.g., different tests binding to the same local ports, and deterministic resolution of hostnames and ephemeral ports), it also substantially increases code coverage. An evaluation on 23,886 classes from 110 open source projects, totalling more than 6.6 million lines of Java code, reveals that network access happens in 2,642 classes (11%). Our implementation of the proposed technique as part of the EVOSUITE testing tool addresses the networking code contained in 1,672 (63%) of these classes, and leads to an increase of the average line coverage from 29.1% to 50.8%. On a manual selection of 42 Java classes heavily depending on networking, line coverage with EVOSUITE more than doubled with the use of network mocking, increasing from 31.8% to 76.6%.

Verifiers that can prove programs correct against their full functional specification require, for programs with loops, additional annotations in the form of loop invariants-properties that hold for every iteration of a loop. We show that significant loop invariant candidates can be generated by systematically mutating postconditions; then, dynamic checking (based on automatically generated tests) weeds out invalid candidates, and static checking selects provably valid ones. We present a framework that automatically applies these techniques to support a program prover, paving the way for fully automatic verification without manually written loop invariants: Applied to 28 methods (including 39 different loops) from various java.util classes (occasionally modified to avoid using Java features not fully supported by the static checker), our DYNAMATE prototype automatically discharged 97 percent of all proof obligations, resulting in automatic complete correctness proofs of 25 out of the 28 methods-outperforming several state-of-the-art tools for fully automatic verification.

Automatic unit test generation aims to support developers by alleviating the burden of test writing. Different techniques have been proposed over the years, each with distinct limitations. To overcome these limitations, we present an extension to the EvoSuite unit test generator that combines two of the most popular techniques for test case generation: Search-Based Software Testing (SBST) and Dynamic Symbolic Execution (DSE). A novel integration of DSE as a step of local improvement in a genetic algorithm results in an adaptive approach, such that the best test generation technique for the problem at hand is favoured, resulting in overall higher code coverage.

Automated test generation for object-oriented software typically consists of producing sequences of calls aiming at high code coverage. In practice, the success of this process may be inhibited when classes interact with their environment, such as the file system, network, user-interactions, etc. This leads to two major problems: First, code that depends on the environment can sometimes not be fully covered simply by generating sequences of calls to a class under test, for example when execution of a branch depends on the contents of a file. Second, even if code that is environment-dependent can be covered, the resulting tests may be unstable, i.e., they would pass when first generated, but then may fail when executed in a different environment. For example, tests on classes that make use of the system time may have failing assertions if the tests are executed at a different time than when they were generated.

Generating system inputs satisfying complex constraints is still a challenge for modern test generators. We present XMLMATE, a search-based test generator specially aimed at XML-based systems. XMLMATE leverages program structure, existing XML schemas, and XML inputs to generate, mutate, recombine, and evolve valid XML inputs. Over a set of seven XML-based systems, XMLMATE detected 31 new unique failures in production code, all triggered by system inputs and thus true alarms.

SUMMARY Translation of Annotated COde (TACO) is a SAT‐based tool for bounded verification of Java programs. One challenge many formal tools share is to provide a practical interface for a non‐proficient user. In this article, we present an Eclipse plug‐in for the static verifier TACO. This plug‐in allows a user to walk a counterexample trace mimicking a debugging session. TacoPlug (our plug‐in) uses and extends TACO to provide a better debugging experience. TacoPlug interface allows the user to verify an annotated software using the TACO verifier. If TACO finds a violation to the specification, TacoPlug presents it in terms of the annotated source code. TacoPlug features several views of the error trace to facilitate fault understanding. It resembles any software debugger, but the debugging occurs statically without executing the program. Furthermore, should a dynamic analysis be required, TacoPlug presents the user with a unit test case generated by TACO based on the detected violation. We show the usability of our tool by means of a motivational example taken from a real‐life software error. Copyright © 2013 John Wiley & Sons, Ltd.

We present a novel and general technique for automated test generation that combines tight bounds with incremental SAT solving. The proposed technique uses incremental SAT to build test suites targeting a specific testing criterion, amongst various black-box and white-box criteria. As our experimental results show, the combination of tight bounds with incremental SAT, and the testing criterion driven approach implemented in our prototype tool FAJITA, enable us to effectively generate test suites for container classes with rich contracts, more efficiently than other state-of-the-art tools.

Search-based testing can automatically generate unit test suites for object oriented code, but may struggle to generate specific values necessary to cover difficult parts of the code. Dynamic symbolic execution (DSE) efficiently generates such specific values, but may struggle with complex datatypes, in particular those that require sequences of calls for construction. The solution to these problems lies in a hybrid approach that integrates the best of both worlds, but such an integration needs to adapt to the problem at hand to avoid that higher coverage in a few corner cases comes at the price of lower coverage in the general case. We have extended the Genetic Algorithm (GA) in the Evosuite unit test generator to integrate DSE in an adaptive approach where feedback from the search determines when a problem is suitable for DSE. In experiments on a set of difficult classes our adaptive hybrid approach achieved an increase in code coverage of up to 63% (11% on average); experiments on the SF100 corpus of roughly 9,000 open source classes confirm that the improvement is of practical value, and a comparison with a DSE tool on the Roops set of benchmark classes shows that the hybrid approach improves over both its constituent techniques, GA and DSE.

In this article we present a novel technique for automated parallel bug-finding based on the sequential analysis tool TACO. TACO is a tool based on SAT-solving for efficient bug-finding in Java code with rich class invariants. It prunes the SAT-solver's search space by introducing precise symmetry-breaking predicates and bounding the relational semantics of Java class fields. The bounds computed by TACO generally include a substantial amount of nondeterminism; its reduction allows us to split the original analysis into disjoint subproblems. We discuss the soundness and completeness of the decomposition. Furthermore, we present experimental results showing that MUCHO-TACO, our tool which implements this technique, yields significant speed-ups over TACO on commodity cluster hardware.

SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the failure is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this paper, we present Translation of Annotated COde (TACO), a prototype tool which implements a novel, general, and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument code analysis with a symmetry-breaking predicate which, on one hand, reduces the size of the search space by ignoring certain classes of isomorphic models and, on the other hand, allows for the parallel, automated computation of tight bounds for Java fields. Experiments show that the translations to propositional formulas require significantly less propositional variables, leading to an improvement of the efficiency of the analysis of orders of magnitude, compared to the noninstrumented SAT--based analysis. We show that in some cases our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking, or SMT-solving.

SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the error is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques.

DynAlloy is an extension of Alloy to support the definition of actions and the specification of assertions regarding execution traces. In this article we show how we can extend the Alloy tool so that DynAlloy specifications can be automatically analyzed in an efficient way. We also demonstrate that DynAlloy's semantics allows for a sound technique that we call program atomization , which improves the analyzability of properties regarding execution traces by considering certain programs as atomic steps in a trace. We present the foundations, case studies, and empirical results indicating that the analysis of DynAlloy specifications can be performed efficiently.

We present DynAlloy, an extension to the Alloy specification language to describe dynamic properties of systems using actions. Actions allow us to appropriately specify dynamic properties, particularly, properties regarding execution traces, in the style of dynamic logic specifications.We extend Alloy's syntax with a notation for partial correctness assertions, whose semantics relies on an adaptation of Dijkstra's weakest liberal precondition. These assertions, defined in terms of actions, allow us to easily express properties regarding executions, favoring the separation of concerns between the static and dynamic aspects of a system specification.We also extend the Alloy tool in such a way that DynAlloy specifications are also automatically analyzable, as standard Alloy specifications. We present the foundations, two case-studies, and empirical results evidencing that the analysis of DynAlloy specifications can be performed efficiently.