When testing a state-based system one might use a set of (negative) test cases in which each test case is a sequence of events that should not occur. Testing then involves executing the system under test (SUT) in order to check whether any of these disallowed sequences can occur. While testing using such sequences can be effective, they introduce a source of inefficiency: if a test case expects the SUT to produce output a after observing a sequence σ and the SUT instead produces a different output a ′ after σ then testing with that test case did not show an error, because the SUT can autonomously produce outputs, and terminates because the test case only makes sense if the exact sequence is observed. This is a source of inefficiency if there is another test case that starts with σ followed by a ′ : we could have continued evaluating whether the application of this second test case leads to an error. This paper considers scenarios in which events represent inputs, outputs, or the passing of discrete time. We show how a set of sequential test cases can be converted into an equivalent set of adaptive test cases, with adaptivity addressing the above source of inefficiency. The proposed approach has the potential to improve efficiency when using any test generation technique that returns negative sequential test cases.

There is extensive literature on automated test generation using reactive design models, where control is determined by events. In contrast, the (idealised) simulation paradigm defines control through cycles dictated by the passage of time. Within each cycle, inputs are read and processed, and outputs are provided, all instantaneously, and afterwards time progresses. To exercise a simulation using tests generated from a reactive design model requires changes to the tests to take into account this paradigm shift. This article focuses on automation of the necessary changes and of the use of the resulting tests in a simulation campaign. Based on a notion of conformance that establishes whether a simulation is correct with respect to a reactive design, we (1) identify the reactive tests that are meaningful; (2) define a process to convert those tests; (3) provide an algorithm to execute those tests and (4) prove soundness and completeness of our approach. Our work is described in the context of the RoboStar framework for model-based development of control software for robotics applications, and its process algebraic semantics. The testing approach we propose here represents a significant advancement in the current testing practices within the field of robotics, where simulations are widely used.

Software systems with large parameter spaces, nondeterminism and high computational cost are challenging to test. Recently, software testing techniques based on causal inference have been successfully applied to systems that exhibit such characteristics, including scientific models and autonomous driving systems. One significant limitation is that these are restricted to test properties where all of the variables involved can be observed and where there are no interactions between variables. In practice, this is rarely guaranteed; the logging infrastructure may not be available to record all of the necessary runtime variable values, and it can often be the case that an output of the system can be affected by complex interactions between variables. To address this, we leverage two additional concepts from causal inference, namely effect modification and instrumental variable methods. We build these concepts into an existing causal testing tool and conduct an evaluative case study which uses the concepts to test three system-level requirements of CARLA, a high-fidelity driving simulator widely used in autonomous vehicle development and testing. The results show that we can obtain reliable test outcomes without requiring large amounts of highly controlled test data or instrumentation of the code, even when variables interact with each other and are not recorded in the test data.

Regression testing assures software correctness after changes but is resource-intensive. Test Case Prioritisation (TCP) mitigates this by ordering tests to maximise early fault detection. Diversity-based TCP prioritises dissimilar tests, assuming they exercise different system parts and uncover more faults. Traditional static diversity-based TCP approaches (i.e., methods that utilise the dissimilarity of tests), like the state-of-the-art FAST approach, rely on textual diversity from test source code, which is effective but inefficient due to its relative verbosity and redundancies affecting similarity calculations. This paper is the first to study bytecode as the basis of diversity in TCP, leveraging its compactness for improved efficiency and accuracy. An empirical study on seven Defects4J projects shows that bytecode diversity improves fault detection by 2.3–7.8% over text-based TCP. It is also 2–3 orders of magnitude faster in one TCP approach and 2.5–6 times faster in FAST-based TCP. Filtering specific bytecode instructions improves efficiency up to fourfold while maintaining effectiveness, making bytecode diversity a superior static approach.

Software Testing is normally one of the main forms of verification and validation used in software development but it is often manual and so expensive and error prone. One of the proposed solutions to this is to use model-based testing, in which testing is based on a model of how the system should behave. If the model has a formal semantics, then there is potential to automate systematic test generation. In this paper we consider the case where the semantics of the model is a set of refusal traces, also called failure traces. We show how the notions of fundamental refusal and fundamental refusal trace can be used to derive a normalised transition system, which we call an observation transition system (OTS), from the semantics. We then show how, if this OTS has finitely many states, and we are given a bound m, one can produce a corresponding complete test suite: one that is guaranteed to determine correctness as long as the number of states of the OTS defined by the semantics of the system under test has no more than m states. In practice, the choice of value for m might be based on domain knowledge or a cost-benefit analysis. As far as we are aware, this is the first work to show how a finite complete test suite can be derived when the semantics under consideration is a set of refusal traces.

ABSTRACT There has been a significant amount of interest regarding the use of DBTtsfull in software testing over the past two decades. Diversity‐based testing (DBT) technique uses similarity metrics to leverage the dissimilarity between software artefacts—such as requirements, abstract models, programme structures or inputs—in order to address a software testing problem. DBT techniques have been used to assist in finding solutions to several different types of problems including generating test cases, prioritizing them and reducing very large test suites. This paper is a systematic mapping study of DBT techniques that summarizes the key aspects and trends of 167 papers that report the use of 79 different similarity metrics with 22 different types of software artefacts, which have been used by researchers to tackle 11 different types of software testing problems. We further present an analysis of the recent trends in DBT techniques and review the different application domains to which the techniques have been applied, giving an overview of the tools developed by researchers in order to do so. Finally, the paper identifies some DBT challenges that are potential topics for future work, such as exploring other diversity artefacts and measuring diversity for complex data input.

ABSTRACT The recent growth in popularity of wearable medical devices has improved the quality of life of people with medical conditions. Testing such devices may require users to configure these systems using physical trials, putting themselves in potentially dangerous scenarios. Misconfiguration of such devices has caused disease misdiagnoses and incorrect drug prescriptions. Digital twins have been proposed as an opportunity to reduce such risks of testing system configurations in simulated environments, decoupling the user from the system under test. In this paper, we perform an evaluative case study to assess the use of a digital twin for configuration testing of an artificial pancreas system (APS) control algorithm. These systems regulate the blood glucose levels in people with type 1 diabetes mellitus, and so misconfigurations can cause severe hypoglycaemia or hyperglycaemia, which can be life‐threatening. We tested the OpenAPS control algorithm against 156 people's clinical data. We found that our digital twin provided an accurate simulation environment to perform configuration testing and accurately predict blood glucose–insulin behaviour. We evaluated different APS configurations, identifying a potentially unsafe configuration without the risks associated with a physical trial. We identified the challenges associated with modelling clinical data, which could lead to misinterpretations in configuration testing and the reduction of test reliability when modelling stochastic body dynamics.

The practice of testing software systems modelled as Finite State Machines (FSMs) has garnered significant attention owing to its simplicity. In FSM-based testing, the tester derives a test suite from the FSM model representing the system’s specification. Subsequently, this test suite is executed against the implementation, and the tester uses the output to decide whether the implementation conforms to the specification. Often, a test suite generation technique requires input sequences to check whether the FSM is in the intended state. This task is referred to asstate identificationand is often carried out using a set of input sequences called a characterising set. Even though the use of characterising sets simplifies testing, they require a reliable reset or reset sequence and additional transfer sequences. Unfortunately, resetting the underlying system can be costly or may entail manual configuration. In addition, transfer sequences do not directly contribute to testing. This work introduces a class of characterising sets (Ordered Characterising Sets(O-WSets)) that avoid using resets or transfers by design. We show that checking the existence of such a characterising set is NP-complete. We introduce the notion of bounded O-WSets (BO-WSets), which are types of O-WSets that limit transfer usage, and give an algorithm that constructs these. In experiments, on average, the proposed approach led to reductions in the number of resets (95% for real FSMs; 99.73% for synthetic FSMs), the number of transfer inputs (53% for real FSMs; 63.3% for synthetic FSMs) and the number of inputs in state identification sequences (50% for real FSMs; 66.6% for synthetic FSMs). Additionally, the proposed algorithm reduced the time and memory required to derive state identification sequences by 85% and 23%, respectively. Finally, the approach led to test suites with 49.3% fewer sequences and 33.3% fewer inputs on average.

Regression test suites can have a large number of test cases, especially automatically generated ones, and tend to grow in size, making it costly to run the entire test suite. Test suite reduction aims to eliminate some test cases to reduce the test suite size and therefore reduce the cost of running it. In this paper, string distances on the text of the test cases are used as measures of similarity for reduction. A practical benefit of using string distance is that there is no need to run the test cases: the test suite source code is the only requirement, making the approach fast. We reduce test suites generated from Randoop and EvoSuite; two well-known test generation tools of Java programs. We implemented a string-based similarity reduction and compared it against random reduction. In the experiments, mutation scores using reduced test suites based on maximising string dissimilarity of test cases were higher than those for random reduction in over 70% of the test suites generated. Also, the results showed that test suites generated by Randoop can be drastically reduced in one case by 99% using the string-based similarity reduction approach while maintaining the fault-finding capabilities of the original test suite. Finally, on average, the normalised compression distance was found to be the best similarity metric choice in terms of fault-detection.

Causal reasoning is becoming an increasingly popular technique for testing software. In this setting, the tester starts from a simple directed graph that captures their underlying understanding of causal relationships between relevant variables in the program, and this knowledge is then used to reason about causal input-output relationships that are observed during testing. One question that has not yet been addressed in this context is how to measure test adequacy: How do we know whether a causal relationship (or set of relationships) has been properly established by a test set? In this paper we present a metric inspired by Weyuker's notion of inference adequacy. For a given causal relationship, we estimate the causal effect from the test data. The basis of our adequacy metric is then an estimate of the convergence of this estimate, which we calculate using statistical bootstrapping. We evaluate our metric on tests for three diverse computational models. The results show a statistically significant correlation between our metric and a test suite's ability to detect mutants, and also that it is a good indicator of whether a sufficient number of system executions have been observed to trust the outcome of the test.

From simulating galaxy formation to viral transmission in a pandemic, scientific models play a pivotal role in developing scientific theories and supporting government policy decisions that affect us all. Given these critical applications, a poor modelling assumption or bug could have far-reaching consequences. However, scientific models possess several properties that make them notoriously difficult to test, including a complex input space, long execution times, and non-determinism, rendering existing testing techniques impractical. In fields such as epidemiology, where researchers seek answers to challenging causal questions, a statistical methodology known as Causal inference has addressed similar problems, enabling the inference of causal conclusions from noisy, biased, and sparse data instead of costly experiments. This article introduces the causal testing framework: a framework that uses causal inference techniques to establish causal effects from existing data, enabling users to conduct software testing activities concerning the effect of a change, such as metamorphic testing, a posteriori . We present three case studies covering real-world scientific models, demonstrating how the causal testing framework can infer metamorphic test outcomes from reused, confounded test data to provide an efficient solution for testing scientific modelling software.

Testing is a crucial phase in the development of complex systems, and this has led to interest in automated test generation techniques based on state-based models. Many approaches use models that are types of finite state machine (FSM). Corresponding test generation algorithms typically require that certain test components, such as reset sequences (RSs) and preset distinguishing sequences (PDSs), have been produced for the FSM specification. Unfortunately, the generation of RSs and PDSs is computationally expensive, and this affects the scalability of such FSM-based test generation algorithms. This paper addresses this scalability problem by introducing a reinforcement learning framework: the$\mathcal{Q}$-Graph framework for MBT. We show how this framework can be used in the generation of RSs and PDSs and consider both (potentially partial) timed and untimed models. The proposed approach was evaluated using three types of FSMs: randomly generated FSMs, FSMs from a benchmark, and an FSM of an Engine Status Manager for a printer. In experiments, the proposed approach was much faster and used much less memory than the state-of-the-art methods in computing PDSs and RSs.

The state of practice in design and verification of control software for robotics is code centric. The RoboStar framework supports a model-based approach, providing support for modelling and simulation, and techniques for automatic generation of artefacts. Existing results support test generation using a reactive design model; in RoboStar such models can be described using a diagrammatic notation called RoboChart. Here, we describe the challenges involved in using such tests for execution against simulations or cyclic implementations either automatically generated or custom developed. While it is possible to use a cyclic model to generate tests in the first place, reactive models are akin to those normally used by the community. Moreover, by linking design-based tests to the tests executed against the cyclic mechanisms, we support traceability.

Metamorphic testing provides a means by which to generate succinct test oracles that can apply to large input spaces. For this it depends on the formulation of metamorphic relations, which generally require extensive domain expertise and human input. To address this problem, we present a model-based testing approach that can automatically generate metamorphic relations and associated tests. Our approach is motivated by the observation that metamorphic testing is a fundamentally causal task. We show how it is possible to leverage lightweight graph-based modelling techniques from the field of causal inference to specify causal properties of the system-under-test. Through a series of controlled experiments, we find that the proposed approach is robust to misspecification and can test evasive causal relationships (i.e. those that are difficult to exercise and observe) when combined with an appropriate test generation strategy. We also apply the approach to two case studies from the Defects4J framework with known bugs that affect causal behaviour. The results of these case studies suggest that the approach is not only useful for catching bugs affecting causal structure, but also alerting the user to inaccuracies in the specification.

We explore the problem of finding a minimal complete test suite for refusal trace (or failure trace) semantics. Our approach is based on generating a minimal complete set of forbidden refusal traces and utilises several interesting insights into the semantics. In particular, we identify a key class of refusals called fundamental refusals which essentially determine the refusal trace semantics, and the associated equivalence relation. We then propose a small but not necessarily minimal test suite, which can be constructed with a simple algorithm. Subsequently, we provide an enumerative method to remove all redundant traces from our complete test suite, which comes in two variants, depending on whether we wish to retain the highly desirable uniform completeness. We also address a related problem from modal logic, namely the construction of a characteristic formula of a given process with respect to refusal trace semantics, using a variant of Hennessy-Milner logic with recursion.

Cyber–physical systems present a challenge to testers, bringing complexity and scale to safety-critical and collaborative environments. Digital twins enhance these systems through data-driven and simulation based models coupled to physical systems to provide visualisation, predict future states and communication. Due to the coupling between digital and physical worlds, digital twins provide a new perspective into cyber–physical system testing. The objectives of this study are to summarise the existing literature on digital-twin-based testing. We aim to uncover emerging areas of adoptions, the testing techniques used in these areas and identify future research areas. We conducted a systematic literature review which answered the following research questions: What cyber–physical systems are digital twins currently being used to test? How are test oracles defined for cyber–physical systems? What is the distribution of white-box, black-box and grey-box modelling techniques used for digital twins in the context of testing? How are test cases defined and how does this affect test inputs? We uncovered 26 relevant studies from 480 produced by searching with a curated search query. These studies showed an adoption of digital-twin-based testing following the introduction of digital twins in industry as well as the increasing accessibility of the technology. The oracles used in testing are the digital twin themselves and therefore rely on both system specification and data derivation. Cyber–physical systems are tested through passive testing techniques, as opposed to either active testing through test cases or predictive testing using digital twin prediction. This review uncovers the existing areas in which digital twins are used to test cyber–physical systems as well as outlining future research areas in the field. We outline how the infancy of digital twins has affected their wide variety of definitions, emerging specialised testing and modelling techniques as well as the current lack of predictive ability.

The existing testing theories for CSP cater for verification of interaction patterns (traces) and deadlocks, but not time. We address here refinement and testing based on a dialect of CSP, called tock -CSP, which can capture discrete time properties. This version of CSP has been of widespread interest for decades; recently, it has been given a denotational semantics, and model checking has become possible using a well established tool. Here, we first equip tock -CSP with a novel semantics for testing, which distinguishes input and output events: the standard models of ( tock -)CSP do not differentiate them, but for testing this is essential. We then present a new testing theory for timewise refinement, based on novel definitions of test and test execution. Finally, we reconcile refinement and testing by relating timed ioco testing and refinement in tock -CSP with inputs and outputs. With these results, this paper provides, for the first time, a systematic theory that allows both timed testing and timed refinement to be expressed. An important practical consequence is that this ensures that the notion of correctness used by developers guarantees that tests pass when applied to a correct system and, in addition, faults identified during testing correspond to development mistakes.

The increasing complexity and criticality of software systems have led to growing interest in automated test generation. One of the most promising approaches is to use model-based testing (MBT), in which test automation is based on a model of theimplementation under test (IUT), with much of the work concerning finite state machine (FSM) models. Many FSM-based test generation techniques use, possibly adaptive, sequences to check the state of the IUT. Of particular interest are adaptive distinguishing sequences (ADSs) because their use can lead to relatively small tests. However, not all systems possess an ADS. In this work, we generalise the notion of incomplete ADSs to non-deterministic partial and observable FSMs. We show that the problem of checking the existence of a set of$k$incomplete ADSs that separates every pair of states is PSPACE-hard. Further, we generalise the notion of invertible sequences to non-deterministic partial and observable FSMs and show how invertible sequences can be used to derive additional incomplete ADSs. We propose a novel algorithm to generate incomplete ADSs and describe the results of experiments that evaluated its performance. The results indicate that the proposed method can generate sequences to identify states of the IUT and is faster and can process larger FSMs than other existing methods.

Modelling the behaviour of state-based systems can be challenging, especially when the modeller is not entirely certain about its intended interactions with the user or the environment. Currently, it is possible to associate a stated level of uncertainty with a given event by attaching probabilities to transitions (producing ‘Probabilistic State Machines’). This captures the ‘First-order uncertainty’ - the (un-)certainty that a given event will occur. However, this does not permit the modeller to capture their own uncertainty (or lack thereof) about that stated probability - also known as ‘Second-order uncertainty’. In this article we introduce a generalisation of probabilistic finite state machines that makes it possible to incorporate this important additional dimension of uncertainty. For this we adopt a formalism for reasoning about uncertainty called Subjective Logic. We present an algorithm to create these enhanced state machines automatically from a conventional state machine and a set of observed sequences. We show how this approach can be used for reverse-engineering predictive state machines from traces.

This is my last (regular) editorial for STVR. This has been a long association that started when I was contacted by Jeff Offutt in 2011. I was surprised and delighted when Jeff invited me to become joint editor-in-chief. Naturally, I accepted the invitation without hesitation. I have always valued STVR, as a reader and author, and it has been an honour to be involved in this capacity. However, I believe that, after 11 years, it is time for someone else, with fresh ideas, to work with Tao. I also look forward to being able to submit papers to STVR again! Many things have changed during the last 11 years. Many of these have been positive. For example, the electronic facilities have advanced, making processes easier (I hope) for authors and editors. Journal papers now appear on the website soon after acceptance; previously, authors had to wait many months before their paper was accessible. I also like the introduction of journal first sessions in conferences. These provide another dissemination route for the authors of journal papers and additional high-quality presentations for those attending conferences. In some ways, the journal first sessions can be seen as a move towards the approach taken in many other disciplines, in which conferences support discussion and dissemination, while the peer reviewed papers are published in journals. I do wonder whether a move to such an approach would benefit the community—there certainly would be less reviewing! However, I cannot see such a change happening in the near future. Unfortunately, not all changes have been positive. Of particular note has been the increase in number of papers that we desk reject, often because they are simply out of scope. This takes up time for the editors and journal staff, and it must also consume author time. However, this is not a major issue, and I believe that the vast majority of changes have been positive. When I decided to step down, Tao and I discussed what makes a good EiC and who we might approach. We quickly converged upon one name and were delighted when Yves accepted our invitation. I have known Yves for some time and have always been impressed by his integrity and honesty, in addition to the undoubted quality of his research. My only slight regret is that I will not work with him in this capacity, but I am confident that he and Tao will work together well and that STVR is in excellent hands. Finally, I would like to take this opportunity to thank some of the many people who have contributed over the last 11 years. It has been a pleasure to work with Jeff Offutt and, more recently, Tao Xie. Their support and advice have been invaluable, and I have enjoyed discussing matters with two such good-natured and knowledgeable individuals. Many Wiley staff have played a crucial role behind the scenes—too many to list here! The strength of the work published in STVR reflects both the excellent research performed by authors, the feedback from reviewers, and the guidance and support provided by editorial board members. Finally, I would like to thank Yves for accepting our invitation and for his assistance during the hand-over.

This issue contains four papers. The first paper focuses on model checking, the second and third papers focus on testing and the last paper focuses on debugging. The first paper, ‘Model checking C++ programs’ by Felipe R. Monteiro, Mikhail R. Gadelha and Lucas C. Cordeiro, is motivated by memory safety issues and how these have proved to be a source of security vulnerabilities. The authors devised a novel bounded model checking approach. The first step was to encode a number of C++ features in a decidable fragment of first-order logic. SMT solvers were then used to carry out verification. In experiments, the proposed approach was found to outperform state-of-the-art verifiers. The prototype tool also found arithmetic-overflow errors in a commercial application. (Recommended by Professor Pretscher) The second paper, ‘GPU acceleration of finite state machine input execution: Improving scale and performance’, by Vanya Yaneva, Ajitha Rajan and Christophe Dubach looks at the problem of executing a large number of tests on a finite state machine (FSM). The motivation for this work is model validation. The approach devised uses GPUs to allow multiple tests to be run in parallel. The authors built on their previous work, which showed how FSM execution can be performed on a GPU, by addressing a number of limitations. In particular, the authors addressed the data transfer overhead and they also performed experiments with FSMs that were too large to fit into GPU memory. In the experiments, the novel optimisations led to further improvements, with the GPU being over four times faster, on average, than a 16-core CPU. (Recommended by Professor Pretscher) The third paper, ‘Survey on test case generation, selection and prioritization for cyber-physical systems’, by Zahra Sadri-Moshkenani, Justin Bradley and Gregg Rothermel, presents a survey of approaches that generate, select or prioritise test cases for cyber-physical systems. The authors identified 34 related papers (26 papers on test generation, 6 papers on test selection and 7 papers on test prioritisation) and classified them according to 8 properties distilled by the authors from past experience. From the survey results, the authors identified a number of open challenges. To address some of these challenges, existing approaches may be adapted or new approaches may be developed. (Recommended by Professor Phil McMinn) The fourth paper, ‘Effective fault localization and context-aware debugging for concurrent programs’, by Justin Chu, Tingting Yu, Jane Huffman Hayes, Xue Han and Yu Zhao, presents Coadec, an approach for automatically generating interthread control flow paths to diagnose concurrency bugs. Coadec consists of two phases: concurrency fault localization and context-aware debugging. The authors evaluated Coadec on 10 real-world multithreaded Java applications and showed that Coadec outperforms state-of-the-art approaches for localising concurrency faults and that Coadec's context debugging can help developers understand concurrency fault by inspecting a small percentage of code. (Recommended by Marc Roper)

This issue contains two papers. The first paper focuses on combinatorial testing and the second one focuses on model-based testing. The first paper, ‘Combinatorial methods for testing Internet of Things smart home systems’ by Bernhard Garn, Dominik-Philip Schreiber, Dimitris E. Simos, Rick Kuhn, Jeff Voas, and Raghu Kacker, presents an approach for applying combinatorial testing (CT) to the internal configuration and functionality of Internet of Things (IoT) home automation hub systems. The authors first create an input parameter model of an IoT home automation hub system for use with test generation strategies of combinatorial testing and then propose an automated test execution framework and two test oracles for evaluation purposes. The proposed approach makes use of the appropriately formulated model of the hub and generates test sets derived from this model satisfying certain combinatorial coverage conditions. The authors conduct an evaluation of the proposed approach on a real-world IoT system. The evaluation results show that the proposed approach reveals multiple errors in the devices under test, and all approaches under comparison perform nearly equally well (recommended by W. K. Chan). The second paper, ‘Effective grey-box testing with partial FSM models’ by Robert Sachtleben and Jan Peleska, explores the problem of testing from a finite state machine (FSM) and considers the scenario in which an input can be enabled in some states and disabled in other states. There is already a body of work on testing from FSMs in which inputs are not always defined (partial FSMs), but such work typically allows the system under test (SUT) to be such that some inputs are defined in a state of the SUT but are not defined in the corresponding state of the specification FSM (the SUT can be ‘more’ defined). The paper introduces a conformance relation, called strong reduction, that requires that exactly the same inputs are defined in the specification and the SUT. A new test generation technique is given for strong reduction, with this returning test suites that are complete: a test suite is guaranteed to fail if the SUT is faulty and also satisfies certain conditions that place an upper bound on the number of states of the SUT. The overall approach also requires that the tester can determine which inputs are enabled in the current state of the SUT and so testing is grey-box (recommended by Helene Waeselynck).

This issue contains two papers. The first paper focuses on metamorphic testing and the second one focuses on test automation. The first paper, ‘Metamorphic relation prioritization for effective regression testing’ by Madhusudan Srinivasan and Upulee Kanewala, concerns metamorphic testing. Metamorphic testing (MT) is an approach devised to support the testing of software that is untestable in the sense that it is not feasible to determine, in advance, the expected output for a given test input. The basic idea behind MT is that it is sometimes possible to provide a property (metamorphic relation) over multiple test runs that use inputs that are related in some way. A classic example is that we may not know what the cosine of x should be for some arbitrary x but we do know that cos(x) should be the same as cos(−x). Previous work has proposed the use of multiple metamorphic relations (MRs), but the authors explore how one might prioritize (order) such MRs. Prioritization is based on information regarding a previous version of the software under test. The authors propose two approaches: prioritize on coverage or on fault detection. Optimization is achieved using a greedy algorithm that is sometimes called Additional Greedy. (Recommended by Dan Hao). The second paper, ‘Improving test automation maturity: A multivocal literature review’ by Yuqing Wang, Mika V. Mäntylä, Zihao Liu, Jouni Markkula and Päivi Raulamo-jurvanen, presents a multivocal literature review to survey and synthesize the guidelines given in the literature for improving test automation maturity. The authors select and review 81 primary studies (26 academic literature sources and 55 grey literature sources). From these primary studies, the authors extract 26 test automation best practices along with advice on how to conduct these best practices in forms of implementation/improvement approaches, actions, technical techniques, concepts and experience-based opinions. In particular, the literature review results contribute test automation best practices to suggest steps for improving test automation maturity, narrow the gap between practice and research in terms of the industry's need to improve test automation maturity, provide a centralized knowledge base of existing guidelines for test automation maturity improvement and identify related research challenge and opportunities. (Recommended by Dan Hao).

The 80-20 rule is well-known in the real-world. When applied to bugs, it suggests that 80% of bugs arise in just 20% of classes. One research question that has yet to be explored is whether the same rule applies to refactoring activity. In other words, do 20% of classes account for 80% of refactorings applied to a system? In this short paper, we explore this question using data from seven open-source systems drawn from two previous studies. In each case, we explore whether the 80-20 rule applies and suggest why. Results showed limited evidence of an 80-20 rule; in the two systems where it was evident, the refactoring profile implied firstly, a large-scale movement of class fields and methods and, secondly, the deliberate aim of collapsing the class hierarchy using inheritance-based refactorings.

Model-based testing is a structured method to test complex systems. Scaling up model-based testing to large systems requires improving the efficiency of various steps involved in testcase generation and more importantly, in test-execution. One of the most costly steps of model-based testing is to bring the system to a known state, best achieved through synchronising sequences. A synchronising sequence is an input sequence that brings a given system to a predetermined state regardless of system’s initial state. Depending on the structure, the system might be complete, i.e., all inputs are applicable at every state of the system. However, some systems are partial and in this case not all inputs are usable at every state. Derivation of synchronising sequences from complete or partial systems is a challenging task. In this paper, we introduce a novel Q-learning algorithm that can derive synchronising sequences from systems with complete or partial structures. The proposed algorithm is faster and can process larger systems than the fastest sequential algorithm that derives synchronising sequences from complete systems. Moreover, the proposed method is also faster and can process larger systems than the most recent massively parallel algorithm that derives synchronising sequences from partial systems. Furthermore, the proposed algorithm generates shorter synchronising sequences.

We explore the problem of finding a minimal complete test suite for a refusal trace (or failure trace) semantics. Since complete test suites are typically infinite, we consider the setting with a bound ℓ on the length of refusal traces of interest. A test suite T is thus complete if it is failed by all processes that contain a disallowed refusal trace of length at most ℓ.The proposed approach is based on generating a minimal complete set of forbidden refusal traces. Our solution utilises several interesting insights into refusal trace semantics. In particular, we identify a key class of refusals called fundamental refusals which essentially determine the refusal trace semantics, and the associated fundamental equivalence relation. We then propose a small but not necessarily minimal test suite based on our theory, which can be constructed with a simple algorithm. Subsequently, we provide an enumerative method to remove all redundant traces from our complete test suite, which comes in two variants, depending on whether we wish to retain the highly desirable uniform completeness (guarantee of shortest counterexamples).A related problem is the construction of a characteristic formula of a process P, that is, a formula ΦP such that every process which satisfies ΦP refines P. Our test generation algorithm can be used to construct such a formula using a variant of Hennessy-Milner logic with recursion.

This issue includes four papers, covering performance mutation testing, performance regression localization, fault detection and localization, and defect prediction, respectively. The first paper, by Pedro Delgado-Pérez, Ana Belén Sánchez, Sergio Segura and Inmaculada Medina-Bulo, concerns feasibility of applying performance mutation testing (i.e. applying mutation testing to assess performance tests) at the source-code level in general-purpose languages. To successfully apply performance mutation testing, the authors find it necessary to design specific mutation operators and mechanisms to evaluate the outputs. The authors define and evaluate seven new performance mutation operators to model known bug-inducing patterns. The authors report the results of experimental evaluation on open-source C++ programs. (Recommended by Professor Hyunsook Do) The second paper, by Frolin S. Ocariza Jr. and Boyang Zhao, considers the problem of finding the causes of performance regression in software. Here, a performance regression is an increase in response time as a result of changes to the software. The paper describes a design, called ZAM, that automates the process of comparing execution timelines collected from web applications. Such timelines are used as the basis for finding the causes of performance regression. A number of challenges are introduced by the context in which, for example, timing information is typically noisy. The authors report the results of experimental evaluation and also experience in using the approach. (Recommended by Professor T. H. Tse) The third paper, by Rawad Abou Assi, Wes Masri and Chadi Trad, concerns coincidental correctness and its impact on fault detection and localization. The authors consider weak coincidental correctness, in which a faulty statement is executed but this does not lead to an infected state. They also consider strong coincidental correctness, in which the execution of a faulty statement leads to an infected state but does not lead to incorrect output. The authors empirically investigated the effect of coincidental correctness on three classes of technique: spectrum-based fault localization (SBFL), test suite reduction (TSR) and test case prioritization (TCP). Interestingly, there was significant variation with, for example, evidence that coincidental correctness has a greater impact on TSR and TCP than on SBFL. (Recommended by Professor Hyunsook Do) The fourth paper, by Zeinab Eivazpour and Mohammad Reza Keyvanpour, concerns the cost issue when handling the class imbalance problem over the training dataset in software defect prediction. The authors propose the cost-sensitive stacked generalization (CSSG) approach. This approach combines the staking ensemble learning method with cost-sensitive learning, which aims to reduce misclassification costs. In the CSSG approach, the logistic regression classifier and extra randomized trees ensemble method in cost-sensitive learning and cost-insensitive conditions are employed as a final classifier of stacking scheme. The authors report the results of experimental evaluation. (Recommended by Professor Hyunsook Do)

This issue includes three papers, covering software verification, software reliability modelling and performance assessment, respectively. The first paper, ‘Verification algebra for multi-tenant applications in VaaS architecture’, by Kai Hu, Ji Wan, Kan Luo, Yuzhuang Xu, Zijing Cheng and Wei-Tek Tsai, concerns verification in multi-tenant architectures. Multi-tenant architectures support composition of services and so the rapid development of applications. The issue addressed is the potentially massive number of possible applications formed by composing a given set of services. The authors propose a verification algebra that can determine the results of verification of new combinations of property/application on the basis of different combinations of services already verified and/or the verification of different, but related, properties. The overall approach was evaluated through simulations. (Recommended by Professor Paul Strooper) The second paper, ‘Entropy based enhanced particle swarm optimization on multi-objective software reliability modelling for optimal testing resources allocation’, by Pooja Rani and G. S. Mahapatra, concerns the optimum resource allocation problem to obtain the maximum reliability and minimum total cost under the testing effort constraint. The authors formulate a multi-objective software reliability model of testing resources for a new generalized exponential reliability function to characterize dynamic allocation of total expected cost and testing effort. The authors further propose an enhanced particle swarm optimization (EPSO) to maximize software reliability and minimize allocation cost. The authors conduct experiments to demonstrate the potential of the proposed approach to predict software reliability with greater accuracy. (Recommended by Professor Moonzoo Kim) The third paper, ‘Performance assessment based on stochastic differential equation and effort data for edge computing’, by Yoshinobu Tamura and Shigeru Yamada, concerns performance assessment based on the relationship between the cloud and edge services operated by using open-source software. The authors propose a two-dimensional stochastic differential equation model that considers the unique features with uncertainty from big data under the operation of cloud and edge services. The authors analyse actual data to show numerical examples of performance assessments considering the network connectivity as characteristics of cloud and edge services and compare the noise terms of the proposed model for actual data. (Recommended by Professor Min Xie)

This issue contains four papers. The first paper provides a survey of work on testing adaptive and context-aware systems, while the second one concerns testing embedded systems. The remaining two papers explore particular problems associated with an area well known to most STVR readers: mutation testing. The first paper, ‘Testing of adaptive and context-aware systems: Approaches and challenges’, by Bento R. Siqueira, Fabiano C. Ferrari, Kathiani E. Souza, Valter V. Camargo and Rogério de Lemos, introduces a systematic literature review and a thematic analysis of studies to characterize the state of the art in testing adaptive systems (ASs) and context-aware systems (CASs) and discuss approaches, challenges, observed trends and research limitations and directions. The authors discover recurring research concerns related to AS and CAS testing (such as generation of test cases and built-in tests), recurring testing challenges (such as context monitoring and runtime decisions), some trends (such as model-based testing and hybrid techniques) and some little investigated issues (such as uncertainty and prediction of changes). (Recommended by T.Y. Chen) The second paper, ‘Remote embedded devices test framework on the cloud’, by Il-Seok (Benjamin) Choi and Chang-Sung Jeong, introduces a remote embedded device test framework on the cloud named RED-TFC, whose reliability test manager component can automatically perform various tests for evaluating reliability and performance of distributed shared devices by utilizing the cloud concept. RED-TFC includes two major techniques: the adaptive sample scale for reliability test (ASRT) and the mass sample reliability test (MSRT). The authors analyse two Android smartphone models that include many embedded components and show that RED-TFC can help detect a high number of reliability problems in smartphones. (Recommended by Tanja Vos) The third paper, ‘Analysing the combination of cost reduction techniques in Android mutation testing’, by Macario Polo-Usaola and Isyed Rodríguez-Trujillo, concerns the use of mutation testing when testing mobile apps. As the authors note, when testing an app, one typically deploys the app and its mutants on mobile devices or executes them on an emulator. Doing so increases the test execution time. Naturally, it can also significantly increase the cost of mutation testing, especially when there are many mutants. The authors investigate several techniques that have been devised for reducing execution time in mutation testing and produce a mathematical model with the aim of predicting the time taken when some combination of these techniques is used. (Recommended by Mike Papadakis) The final paper is ‘An ensemble-based predictive mutation testing approach that considers impact of unreached mutants’ by Alireza Aghamohammadi and Seyed-Hassan Mirian-Hosseinabadi. This paper also concerns both mutation testing and prediction. However, the authors look at a different prediction problem: that of predicting whether a mutant will be killed. The authors note that previous work did not consider the impact of unreachable mutants: those where the mutation point is not covered by any of the test cases used. It is argued that since many mutation tools exclude unreachable mutants, such mutants should also be removed from any empirical evaluation. The authors report the results of replicating previous studies but also eliminating unreachable mutants, finding that the resultant performance of prediction techniques is far lower than that reported. The authors then propose an alternative prediction model, which is shown to be effective when unreachable mutants are removed. (Recommended by Tanja Vos)

This issue contains four papers. The first and third papers focus on property generation and property verification, respectively, while the second and fourth papers focus on empirical studies of a fault prediction algorithm and test flakiness, respectively. The first paper, “Documentation-based functional constraint generation for library methods,” by Renhe Jiang, Zhengzhao Chen, Yu Pei, Minxue Pan, Tian Zhang, and Xuandong Li, proposes DOC2SMT, an approach that generates functional constraints for library methods based on their documentations. DOC2SMT first translates a method's documentation into candidate constraint clauses, which are then filtered based on static and dynamic validations. The experimental results show the effectiveness and efficiency of DOC2SMT and also show the benefits of the generated constraints for symbolic-execution-based test generation (recommended by Peter Müller). The second paper, “An empirical study of Linespots: A novel past-fault algorithm,” by Maximilian Scholz and Richard Torkar, proposes a new fault prediction algorithm called Linespots. The authors focus on fault prediction based on past faults and refine a previous algorithm (Bugspots). Interestingly, they used a different granularity: line as opposed to file, and this necessitated the development of a benchmark set of experimental subjects. In experiments, Linespots was found to outperform Bugspots (recommended by Xiaoyin Wang). The third paper, “Integrating pattern matching and abstract interpretation for verifying cautions of microcontrollers,” by Thuy Nguyen, Takashi Tomita, Junpei Endo, and Toshiaki Aoki, proposes a semi-automatic approach for verifying cautions, which are hardware-dependent properties described in microcontrollers hardware manuals. For this approach, the authors integrate pattern matching and abstract interpretation, two static program analysis techniques. The experimental results show the feasibility and applicability of the approach (recommended by Marcio Delamaro). The fourth paper, “Empirical analysis of practitioners' perceptions of test flakiness factors,” by Azeem Ahmad, Ola Leifler, and Kristian Sandahl, concerns flaky tests. A flaky test is one where different executions with the same test can lead to different outcomes/verdicts. The authors explore developer perception regarding factors that affect flakiness, concentrating on developers of closed-source software. They also examine two test suites and identify the test smells that lead to flakiness (recommended by Mike Papadakis).

The validation of a cloud system can be complicated by the size of the system, the number of users that can concurrently request services, and the virtualization used to give the illusion of using dedicated machines. Unfortunately, it is not feasible to use conventional testing methods with cloud systems. This article proposes a framework, called TEA-Cloud, that integrates simulation with testing methods for validating cloud system designs. Testing is applied on both functional and nonfunctional aspects of the cloud, like performance and cost. The aim of the framework is to provide a complete methodology to help users to model both software and hardware parts of cloud systems and automatically test the validity of these clouds using a cost-effective approach. Metamorphic testing is used to overcome the lack of an oracle that checks whether the behavior observed in testing is allowed. Metamorphic testing is based on metamorphic relations (MRs). We define three families of MRs, which target issues such as performance, resource provisioning, and cost. TEA-Cloud was evaluated through an empirical study that used fault seeding (mutation) and ten MRs for testing different cloud configurations. The results were promising, with TEA-Cloud finding all seeded faults.

In black-box testing, test sequences may be constructed from systems modelled as deterministic finite-state machines (DFSMs) or, more generally, observable non-deterministic finite state machines (ONFSMs). Test sequences usually contain state identification sequences, with unique input output sequences (UIOs) often being used with DFSMs. This paper extends the notion ofUIOsto ONFSMs. One challenge is that, as a result of non-determinism, the application of an input sequence can lead to exponentially many expected output sequences. To address this scalability problem, we introduce${\mathcal K}$-UIOs:UIOsthat lead to at most${\mathcal K}$output sequences from states of$M$. We show that checking${\mathcal K}$-UIOexistence is PSPACE-Complete if the problem is suitably bounded; otherwise it is in EXPSPACE and PSPACE-Hard. We provide a massively parallel algorithm for constructing${\mathcal K}$-UIOsand the results of experiments on randomly generated and real FSM specifications. The proposed algorithm was able to constructUIOsin cases where the existingUIOgeneration algorithm could not and was able to constructUIOsfrom FSMs with 38K states and 400K transitions.

This editorial was written during a period of extreme difficulty for many individuals, families, and nations in the ongoing COVID-19 outbreak. We can only hope that measures taken are successful and that the situation has improved considerably. We also do not pretend that we have anything to add regarding health, social, or economic issues. However, the crisis has shown the role that Computer Science can play in informing policy. Society requires evidence and computers are often involved in producing such evidence via, for example, simulation. It is here that we, as a community, can contribute through advances in testing, verification, and reliability in areas such as Scientific Computing and Computer Simulations - and maybe also AI/data sciences for helping expedite the process of finding treatment. As a recent example discussed in social media, when commenting on pandemic simulation code used to model control measures against COVID-19, Prof. Guido Salvaneschi said in his tweet: “Ever wondered about the “impact“ of research on programming languages and software engineering? Political decisions affecting hundreds of millions are being taken based on thousands of lines of 13+ years old C code that allegedly nobody understands anymore. #COVID19 #cs” (https://twitter.com/guidosalva/status/1242049884347412482). There is already some truly excellent work for making advances in these areas and we are confident that the community will rise to the challenge. This issue contains two papers. In the first paper, Simons and Lefticaru introduce a new Model-Based Testing approach, which is based on the use of a Stream X-machine (SXM) specification. SXMs provide a state-based formalism and there is a traditional approach to testing from an SXM. This approach typically assumes that the underlying functions/operations have been implemented correctly but these functions may be integrated (into a state machine) in the wrong way. There are a number of automated test generation approaches for SXMs and the authors make two main additional contributions to this area. First, they introduce a number of novel optimisations into test generation. Second, they observe that SXM test generation algorithms return abstract test cases (sequences of functions); the paper shows how corresponding concrete test data can be generated. The approach has been implemented and evaluated on case studies, with the tool also checking that a specification satisfies certain desirable properties. (Recommended by Hyunsook Do). In the second paper, Pouria Derakhshanfar, Xavier Devroey, Gilles Perrouin, Andy Zaidman, and Arie van Deursen introduce behavioural model seeding, a new seeding approach for learning class usages from both the system source code under test and existing test cases. The learned class usages are represented in a state-machine-based behavioural model. The behavioural model is then used to guide search-based crash reproduction, which generates a test case (i.e., objects and sequences of method calls on those objects) to reproduce a crash given its stack trace. This approach is in contrast to the existing seeding strategies, which simply collect and reuse values and object states from the system source code under test and existing test cases without any abstraction. The approach has been implemented in an open-source implementation named the BOTSING toolset and evaluated on 122 crashes from six open-source applications. (Recommended by Phil McMinn).

Due to the ongoing COVID-19 outbreak, conference virtualization has happened, is happening, and will happen for the recent past, ongoing, and upcoming periods, respectively. An ongoing example of conference virtualization is ICSE 2020, the largest conference in software engineering. ACM has recently formed the ACM Presidential Task Force on What Conferences Can Do to Replace Face-to-Face Meetings; in May 2020, this task force released a guide to best practices on virtual conferences (https://www.acm.org/virtual-conferences). The availability of videoconferencing and/or Webinar systems such as Zoom has made online live presentations of accepted conference papers easy and low cost. One may wonder whether the current technology and platform availability for live presentations can facilitate some innovations of disseminating journal papers, going beyond the current common practice of partnership between journals and conferences, e.g., journal-first papers. For example, a journal may consider organizing a virtual journal summit every year or every half of a year for authors of accepted or published papers in that journal to present their papers in an online live manner. Indeed, community discussion is needed before these kinds of innovations are put into action. We welcome your thoughts on possible innovations of disseminating journal papers (especially in the face of conference virtualization), and these innovations' potential pros and cons. This issue contains two papers. In the first paper, Lucas R. Andrade, Patricia D. L. Machado, and Wilkerson. L. Andrade address the problem of predicting the fault detection capability of a test suite. It has previously been observed that although code coverage is often seen as being important, the actual coverage achieved by a test suite is a poor predictor of effectiveness. To address this, recent work has introduced metrics (forms of Operational Coverage) that combine code coverage with information from an operational profile that models the expected usage of the system. This paper reports on the outcomes of a case study that considered 46 versions of a proprietary system. In order to provide an estimate of the effectiveness of a test suite, the authors used the number of post-release bugs reported (the fewer found, the more effective the test suite). Interestingly, it was found that there was a negative correlation between measures of test suite effectiveness with both versions of statement coverage but that the correlation was stronger with operational statement coverage. (Recommended by Lori L. Pollock). In the second paper, Yanqiang Liu, Fangge Yan, Mingyuan Xia, Zhengwei Qi, and Xue Liu present TimelyRep, an efficient and deterministic replay tool for web-enabled mobile applications. TimelyRep achieves deterministic replay of program states and low replay delays in face of the high input rate of mobile interaction. In particular, TimelyRep includes a mechanism for delivering an HTTP response stream with deterministic sequence, contents and latencies, without requiring modification of the browser core or the OS. TimelyRep also includes a mechanism to control replay delays in the JavaScript space, applicable for both the mobile web embeddings and traditional web browsers. This paper reports on an evaluation with two real-world web game applications with complicated non-determinism and intensive user inputs. The evaluation results show that TimelyRep is useful for recreating program bugs and maintaining low delays for touch-intensive web games. (Recommended by Robert Hierons).

This issue of STVR contains two papers that describe automated techniques. Automation has been an important theme in the software engineering research community for many years. In fact, there is an established annual conference (i.e., ASE) devoted to this topic. Many automated techniques have been developed over the years and are likely to remain a major focus of work in software testing, verification, and reliability. It is clear that some problems (e.g., test execution) are more amenable to automation than others (e.g., test generation and correctness-proof construction). However, there has been promising progress in many areas. The increasing importance and popularity of artificial intelligence (AI) has introduced both challenges and opportunities toward automation in software engineering. Systems that use AI often do not have specifications and so it can be difficult to determine whether a behavior is correct (we have no test oracle) or to prove that a piece of software is correct (prove against what?). In addition, we require a model or specification if we are to apply model-based testing techniques, and classical coverage metrics used in many white-box testing techniques appear not to help. It therefore appears that we will need a completely new set of techniques if we are to extend automation to the complete set of AI systems. The good news is that it may be possible to utilize a range of AI techniques, building on work that uses, for example, metaheuristic search or neural networks to automate software testing and formal verification for (non-AI) software. There is already work in this direction, and we look forward to seeing how this area, of using AI to test or verify AI, develops. In the first paper, Sundeuk Kim, Ilhyun Suh, and Yon Dohn Chung present the simulation-based automatic monitoring (SAM) approach for pinpointing web application failures, including those that require browser APIs or client programs. The SAM approach can monitor all three types of web applications: basic, web browser API-added, and client program-based types. The SAM approach includes a DOM-based simulation model using the installation information of browser API-added and client program-based applications (recommended by Sreedevi Sampath). In the second paper, Thomas Walsh, Gregory M. Kapfhammer, and Phil McMinn address a problem in the area of web page layout. The underlying issue is that the layout of web pages, as seen by a user, depends upon the device and browser used. Typically, it is not practical to test with all possible combinations, and in addition, the actual layout is usually manually checked. This paper focuses on regression testing and introduces an automated approach that compares the layout of two pages: the page before a change is made and the page after a change is made. Differences are then reported to the developer (recommended by Marcio Delamaro).

This article addresses refinement and testing based on CSP models, when we distinguish input and output events. In a testing experiment, the tester (or the environment) controls the inputs, and the system under test controls the outputs. The standard models and refinement relations of CSP, however, do not differentiate inputs and outputs and are not, therefore, entirely suitable for testing. Here, we consider an alphabet of events partitioned into inputs and outputs, and we present a novel refusal-testing model for CSP with a notion of input-output refusal-traces refinement. We compare that with the ioco relation often used in testing, and we find that it is more widely applicable and stronger. This means that mistakes found using traditional ioco testing do indicate mistakes in the development. Finally, we provide a CSP testing theory that takes into account inputs and outputs. With our theory, it becomes feasible to develop techniques and tools for automatic generation of realistic and sound tests from CSP models. Our work reconciles the normally disparate areas of refinement and (formal) testing by identifying how ioco testing can be used to inform refinement-based results and vice-versa.

A Software Product Line (SPL) is a set of products built from a number of features, the set of valid products being defined by a feature model. Typically, it does not make sense to test all products defined by an SPL and one instead chooses a set of products to test (test selection) and, ideally, derives a good order in which to test them (test prioritisation). Since one cannot know in advance which products will reveal faults, test selection and prioritisation are normally based on objective functions that are known to relate to likely effectiveness or cost. This article introduces a new technique, the grid-based evolution strategy (GrES), which considers several objective functions that assess a selection or prioritisation and aims to optimise on all of these. The problem is thus a many-objective optimisation problem. We use a new approach, in which all of the objective functions are considered but one (pairwise coverage) is seen as the most important. We also derive a novel evolution strategy based on domain knowledge. The results of the evaluation, on randomly generated and realistic feature models, were promising, with GrES outperforming previously proposed techniques and a range of many-objective optimisation algorithms.

This paper investigates the problem of testing implementations of uniformity statistics. In this paper, we used metamorphic testing to address the oracle problem of checking the output of one or more test executions, for uniformity statistics. We defined a partial oracle that uses regression analysis (a regression model–based metamorphic relation). We investigated the effectiveness of our partial oracle. We found that the technique can achieve mutation scores ranging from 77.78 to 100% and tends towards higher mutation scores in this range. These results are promising and suggest that the regression model–based metamorphic relation approach is a viable method of alleviating the oracle problem in implementations of uniformity statistics, and potentially other classes of statistics, e.g. correlation statistics.

This issue is the first issue of STVR since Jeff Offutt stood down as joint Editor-in-Chief. Jeff was Editor-in-Chief and then joint Editor-in-Chief from 2007 to 2019. This has been an interesting and challenging period for academic journals, with many changes to how journals operate. During this period, Jeff significantly strengthened the journal and has been at the forefront of developments within the field. As Jeff mentioned in the last editorial, there are still many challenges, but Jeff has left STVR in an excellent position. I also hope that we will soon start receiving his papers again! On a personal note, I was honoured when Jeff invited me to be joint EiC, and I welcomed the opportunity to work with him. I accepted immediately and have never regretted the decision. It has been a pleasure to work with Jeff: not only is he a major figure in the field, he is also charming and humble. Jeff also genuinely cares about the discipline and those working within it. As an example, he has spent a significant amount of time providing invaluable advice to junior researchers and students. Although I was sad to see Jeff step down, I am really pleased to be able to welcome Professor Tao Xie as joint Editor-in-Chief of STVR. I first met Tao at a conference (some years ago), and I was immediately impressed by him as a person but also by the work of his that we discussed. This work addressed a real problem in a practical manner but was also based on sound intuition and theory. He has since become a leading figure in the field. Jeff and I were convinced that Tao was the right person to take over and were delighted when he accepted our invitation. Tao has already shown great energy and enthusiasm, and in his upcoming editorial, he will say a little more about some of the ideas of his that we will be implementing. This issue contains two papers. Our first paper is “An Improved Software Reliability Prediction Model by Using High Precision Error Iterative Analysis Method” by Gul Jabeen, Ping Luo and Wasif Afzal (recommended by Min Xie). This concerns a classical problem, which is that of trying to model how the reliability of a piece of software will change during development. Techniques that achieve this can, for example, be used to help plan the software release. The authors use neural networks to help model the error and so make a model more accurate. One of the benefits of the approach is that it can potentially be used with any parametric software reliability prediction model. The second paper is “An End-user-centric Test Generation Methodology for Performance Evaluation of Mobile Networked Applications” by Mustafa Al-tekreeti, Atef Abdrabou and Kshirasagar Naik (recommended by Jane Hayes). The paper concerns the testing of mobile network applications, with a focus on performance (waiting time delay) and its impact on user experience. The authors introduce new test coverage criteria associated with two types of delays and also use metamorphic testing to address the oracle problem.

No abstract available.

The terms “Oracle Problem” and “Non-testable system” interchangeably refer to programs in which the application of test oracles is infeasible. Test oracles are an integral part of conventional testing techniques; thus, such techniques are inoperable in these programs. The prevalence of the oracle problem has inspired the research community to develop several automated testing techniques that can detect functional software faults in such programs. These techniques include N-Version testing, Metamorphic Testing, Assertions, Machine Learning Oracles, and Statistical Hypothesis Testing. This paper presents a Mapping Study that covers these techniques. The Mapping Study presents a series of discussions about each technique, from different perspectives, e.g. effectiveness, efficiency, and usability. It also presents a comparative analysis of these techniques in terms of these perspectives. Finally, potential research opportunities within the non-testable systems problem domain are highlighted within the Mapping Study. We believe that the aforementioned discussions and comparative analysis will be invaluable for new researchers that are attempting to familiarise themselves with the field, and be a useful resource for practitioners that are in the process of selecting an appropriate technique for their context, or deciding how to apply their selected technique. We also believe that our own insights, which are embedded throughout these discussions and the comparative analysis, will be useful for researchers that are already accustomed to the field. It is our hope that the potential research opportunities that have been highlighted by the Mapping Study will steer the direction of future research endeavours.

In the distributed test architecture, the system under test (SUT) interacts with its environment at multiple physically distributed ports and the local testers at these ports do not synchronize their actions. This presents many challenges and, in particular, apparently incorrect behaviors can be the consequence of an erroneous assumption about the exact order in which actions were performed at different ports. In previous work, we defined a conformance relation for the distributed test architecture. Essentially, the SUT is faulty if we observe a trace σ such that no admissible reordering of the actions in σ could have been produced by the specification. However, this notion can be weak if the compared traces might betoodifferent. This paper introduces conformance relations where, for a given metric, a reordering is only considered if the distance between the two traces is at most a certain boundk. We introduce two different metrics and provide algorithms to construct finite automata accepting theseclose, with respect to each metric, sequences. We also study the computational complexity of the two main problems associated with the new framework: deciding whether a trace is accepted by the new automaton and deciding whether one system conforms to a specification with respect to the new conformance relation.

There has been long-standing interest in automatically generating test sequences from a finite state machine (FSM) and more recently this has been extended to the case where there are multiple physically distributed testers and so we are testing from a multi-port FSM. This paper explores the problem of generating a controllable preset distinguishing sequence (PDS) from a multi-port FSM, motivated by the fact that many FSM-based test generation algorithms use PDSs. We prove that it is generally undecidable whether a multi-port FSM has a controllable PDS but provide a class of multi-port FSMs for which the problem is decidable. We also consider the important case where there is an upper bound ` on the length of PDSs of interest, proving that controllable PDS existence is PSPACE-hard and in EXPSPACE. In practice the upper bound ` is likely to be a polynomial in terms of the size of the multi-port FSM and in this case controllable PDS existence is NP- Complete.

How to manage a conference

A distinguishing sequence (DS) for a finite-state machine (FSM) is an input sequence that distinguishes every pair of states of the FSM. There are techniques that generate a test sequence with guaranteed fault detection power, and it has been found that shorter test sequences can be produced if DSs are used. Despite these benefits, however, until recently the only published DS generation algorithms have been for deterministic FSMs. This article develops a massively parallel algorithm, which can be used in Graphics Processing Units (GPUs) Computing, to generate DSs from partial observable non-deterministic FSMs. We also present the results of experiments using randomly generated FSMs and some benchmark FSMs. The results are promising and indicate that the proposed algorithm can derive DSs from partial observable non-deterministic FSMs with 32,000 states in an acceptable amount of time.

This paper concerns the problem of testing from a partial, possibly non-deterministic, finite state machine (FSM) S. Two notions of correctness (quasi-reduction and quasi-equivalence) have previously been defined for partial FSMs but these, and the corresponding test generation techniques, only apply to FSMs that have harmonised traces. We show how quasi-reduction and quasi-equivalence can be generalised to all partial FSMs. We also consider the problem of generating an m-complete test suite from a partial FSM S: a test suite that is guaranteed to determine correctness as long as the system under test has no more than m states. We prove that we can complete S to form a completely-specified non-deterministic FSM S' such that any m-complete test suite generated from S' can be converted into an m-complete test suite for S. We also show that there is a correspondence between test suites that are reduced for S and S' and also that are minimal for S and S'.

Quiescent consistency is a notion of correctness for a concurrent object that gives meaning to the object's behaviours in quiescent states, i.e., states in which none of the object's operations are being executed. The condition enables greater flexibility in object design by allowing more behaviours to be admitted, which in turn allows the algorithms implementing quiescent consistent objects to be more efficient (when executed in a multithreaded environment).

CSP is well established as a process algebra for refinement. Most refinement relations for CSP do not differentiate between inputs and outputs, and so are unsuitable for testing. This paper provides CSP with a denotational semantics based on suspension traces; it gives the traditional CSP operators a novel view, catering for the differences between inputs and outputs. We identify healthiness conditions for the suspension-traces model and include a treatment of termination not contemplated in the context of input-output labelled transition systems. Using our suspension-traces semantics, we provide for CSP a characterisation of the conformance relation ioco, which is widely used in testing. Finally, we propose a strategy to mechanise the verification of conformance according to ioco and suspension-trace refinement using CSP tools. This work provides the basis for a theory of testing for CSP with inputs and outputs, and opens up the possibility of studying algebraic laws and compositional reasoning techniques based on ioco. Ultimately, it contributes to making CSP models useful for both design and testing of systems.

There has been significant interest in distributed testing from an input–output transition system. Previous work introduced an implementation relation $\\bf{dioco}$ that was defined in terms of an equivalence relation on traces (sequences of observations). This paper considers an alternative approach in which an observation made in testing is a tuple of local traces, one for each tester. This paper defines such an implementation relation $\\bf{dioco}_{o}$ in terms of the possible observations regarding the system under test and the specification. It shows that $\\bf{dioco}_{o}$ is strictly weaker than $\\bf{dioco}$ but is equivalent to $\\bf{dioco}$ if processes cannot be output-divergent. Interestingly, this shows that the previous definition of $\\bf{dioco}$ is too strong for output-divergent processes. We also prove that the Oracle problem is NP-complete but can be solved in polynomial time if there is an upper bound on the number of local testers.

This paper concerns the problem of testing from a finite state machine (FSM) M modelling a system that interacts with its environment at multiple physically distributed interfaces, called ports. We assume that the distributed test architecture is used: there is a local tester at each port, the tester at port p only observes events at p, and the testers do not interact during testing. This paper formalises the notion of an adaptive test strategy and what it means for an adaptive test strategy to be controllable. We provide algorithms to check whether a global strategy is controllable and to generate a controllable adaptive distinguishing sequence (ADS). We prove that controllable ADS existence is PSPACE-hard and that the problem of deciding whether M has a controllable ADS with length l is NP-hard. In practice, there is likely to be a polynomial upper bound on the length of ADS in which we are interested and for this case the decision problem is NP-complete.

After months of carefully developing a paper, one submits it to a journal and 2 weeks later it is rejected without review (a ‘desk reject’). Most of us have experienced this scenario; I certainly have. What has happened, and why? Unfortunately, the ‘desk reject’ is part of the journal editor's job, and I suspect most do not enjoy it. Papers are desk rejected for three main reasons. The first is simply that the paper does not fit with the journal's scope. The second is that the paper appears to have deficiencies that mean that it is not worth sending out to review. This might be a result of weaknesses in the research or in the presentation (usually the standard of English). With both reasons, all benefit from the decision: reviewer time is saved, and authors receive faster feedback. The final reason is plagiarism, which was the topic of a previous editorial. Authors can do certain things to make a desk reject less likely. Does the research fit with the journal's scope and, if so, is this clear from the paper? Is the standard of English acceptable? Is the work of a similar standard to, or better than, other papers in the journal? I find that one of the best ways of determining the latter is simply by reading many relevant papers from the journal – and if there are not relevant papers then this might say something about scope! Naturally, there is also the need to assess the overall contribution of the research: is the work novel and potentially significant; is it developed rigorously; and is there a good evaluation. Finally, we can all benefit from discussing these things with our peers – and maybe then the desk reject will become a thing of the past. This issue contains three papers that are related to two important topics that are often considered by quite different communities: regression testing and fault localisation. The first paper concerns regression testing, and the second paper combines the two themes: the authors generalize a fault localisation method (delta debugging) and evaluate this in the context of regression testing. The third paper explores fault localisation for JavaScript. Ghaith et al.explore the regression testing process when carrying out performance testing. Such regression testing aims to find performance anomalies in which there is a significant change in time taken or resource utilisation. This paper is motivated by two practical issues. First, there is a need for automation. Second, the time taken by a transaction depends on the system workload, such as what other transactions are taking place, and there is a need to factor out any changes in workload. The authors propose an automated technique that is based on a queuing network model and is independent of the workload. In this approach, the detection of performance anomalies is based on a metric called the transaction profile: the time taken by a transaction if no other transactions are being carried out. The value of transaction profile is estimated on the basis of the queuing network model and the observed transaction response time and resource utilisation. The work was evaluated through an industrial case study (Recommended by A. Pretschner). Delta debugging is a well-known technique for taking a failing-test case and producing a simplified (failing) test case, the motivation being that this should simplify the debugging process. Groce et al.generalize delta debugging to cause reduction in which a test case is simplified while retaining a property of interest such as coverage. The authors note that standard delta debugging algorithms can be adapted for use in cause reduction. The approach is evaluated in the context of regression testing, where the aim is to reduce the execution time of a regression test suite while preserving code coverage. The results of an empirical study are promising, with the reduced test suites being significantly more efficient while having similar effectiveness. (Recommended by G. Fraser and D. Marinov). Ocariza et al. look at automated fault localisation for JavaScript. The paper focuses on DOM-related faults, pointing to evidence that these are relatively common and arguing that they are also particularly difficult to fix. They develop an approach that uses dynamic backward slicing and have implemented their technique in a tool (AUTOFLOX). They also applied AUTOFLOX to a number of case studies, with it being able to locate 96% of the seeded faults and 20 real faults in real-world applications. (Recommended by L. Zhang).

This issue contains two papers that have a number of significant differences but also some common themes. The differences include the problem addressed (debugging vs. notions of test coverage for regression testing) and the type of entity analysed (model vs. source code). However, one thing that they do have in common is that they both explore alternatives regarding what is observed or monitored. They thus fit into a significant tranche of work that investigates different notions of observation and how these affect software engineering problems. Our first paper, Simulink fault localization: an iterative statistical debugging approach, by Bing Liu, Lucia, Shiva Nejati, Lionel C. Briand and Thomas Bruckmann, looks at debugging based on Simulink models (recommended by Tse). Simulink is widely used in the development of embedded systems, with code being auto-generated from a Simulink model. The motivation for the work described in this paper is that developers deal with Simulink models, and test such models, and so there is a need for debugging techniques that operate at this level. The authors adapt spectrum-based debugging techniques for use with Simulink, leading to what they call the SimFL technique. This ranks blocks from the model according to how ‘suspicious’ they are — based on passing and failing tests. One issue that has to be considered, when reasoning about testing or debugging, is what one considers to be an output. A Simulink model will typically contain multiple blocks, with outputs from some blocks acting as inputs to others. The authors observe that the developer might note that some such outputs are correct, while others are faulty. The authors propose a method that generates a dynamic slice for each output considered; the spectrum-based approach utilizes these slices. The authors also take advantage of the hierarchical nature of Simulink models to produce an iterative version of their approach (iSimFL). The results of empirical studies, using three industrial systems, were promising, with developer only having to consider between 1.3% and 4.4% of model blocks for iSimFL. The second paper, UCov: a user-defined coverage criterion for test case intent verification, by Rawad Abou Assi, Wes Masri and Fadi Zaraket, introduces a new notion of test coverage (recommended by Harman). Most traditional coverage criteria are based on particular syntactic features of a program or model. The authors argue that instead one might consider a notion of intent, as expressed as test requirements. When the system under test is run with a test input there is a resultant execution trace and test requirements refer to properties of this execution trace. Test requirements can refer to structural aspects, such as branches followed, and also behavioural aspects, such as properties of the values of program variables. The authors argue that a potential advantage of using test requirements is that this might be more robust to changes and so suitable for regression testing. For example, the approach is capable of discovering situations in which a test case is still valid for software that has changed but no longer satisfies the corresponding test requirement. The authors propose that if a test case finds a fault then the tester should add a new test requirement that represents why the test case found the fault. If this is done and a later change leads to the test requirement not being satisfied, then the tester can be warned and there is the potential to add a new test case that does satisfy the intent.

Many automated finite state machine (FSM) based test generation algorithms require that a characterising set or a set of harmonised state identifiers is first produced. The only previously published algorithms for partial FSMs were brute-force algorithms with exponential worst case time complexity. This paper presents polynomial time algorithms and also massively parallel implementations of both the polynomial time algorithms and the brute-force algorithms. In the experiments the parallel algorithms scaled better than the sequential algorithms and took much less time. Interestingly, while the parallel version of the polynomial time algorithm was fastest for most sizes of FSMs, the parallel version of the brute-force algorithm scaled better due to lower memory requirements.

A feature model specifies the sets of features that define valid products in a software product line. Recent work has considered the problem of choosing optimal products from a feature model based on a set of user preferences, with this being represented as a many-objective optimization problem. This problem has been found to be difficult for a purely search-based approach, leading to classical many-objective optimization algorithms being enhanced either by adding in a valid product as a seed or by introducing additional mutation and replacement operators that use an SAT solver. In this article, we instead enhance the search in two ways: by providing a novel representation and by optimizing first on the number of constraints that hold and only then on the other objectives. In the evaluation, we also used feature models with realistic attributes, in contrast to previous work that used randomly generated attribute values. The results of experiments were promising, with the proposed (SIP) method returning valid products with six published feature models and a randomly generated feature model with 10,000 features. For the model with 10,000 features, the search took only a few minutes.

This paper describes an efficient parallel algorithm that uses many-core GPUs for automatically deriving Unique Input Output sequences (UIOs) from Finite State Machines. The proposed algorithm uses the global scope of the GPU's global memory through coalesced memory access and minimises the transfer between CPU and GPU memory. The results of experiments indicate that the proposed method yields considerably better results compared to a single core UIO construction algorithm. Our algorithm is scalable and when multiple GPUs are added into the system the approach can handle FSMs whose size is larger than the memory available on a single GPU.

Given a Finite State Machine (FSM) M, a Distinguishing Sequence (DS) is a test that identifies the state of M. While there are two types of DSs, preset DSs (PDSs) and adaptive DSs (ADSs), not all FSMs possess a DS. In this paper, we examine the problem of finding incomplete PDSs and ADSs, exploring associated optimisation problems: finding a largest set of states that has a DS and finding a smallest set of DSs that, between them, distinguish all of the states. We also propose a greedy algorithm to produce a small set of incomplete ADSs and use experiments to compare this with two previously published algorithms for generating state identifiers. We show that the optimisation problems related to incomplete ADSs and PDSs are PSPACE-Complete as are corresponding approximation problems. In the experiments we found that incomplete ADSs produced by the proposed greedy algorithm led to relatively compact state identifiers.

This special issue concerns a range of issues related to the development of concurrent programs. This is an important topic, because many systems are now either multi-threaded or distributed, and it is well known that concurrency makes testing, analysis and debugging significantly more complicated. Essentially, the alternative interleavings of events can lead to different behaviours, and so any analysis, debugging or testing technique must consider these interleavings. The interest in this topic is reflected in the larger than normal issue, which contains five papers. The papers fall into three groups: we start with a paper on debugging, then have two on static analysis techniques and finally have two on testing. All papers were reviewed in the normal way.

A test suite is m-complete for finite state machine (FSM) M if it distinguishes between M and all faulty FSMs with m states or fewer. While there are several algorithms that generate m-complete test suites, they cannot be directly used in distributed testing since there can be additional controllability and observability problems. Indeed, previous results show that there is no general method for generating an m-complete test suite for distributed testing and so the focus has been on conditions under which this is possible. This paper takes a different approach, which is to generate what we call cm-complete test suites: controllable test suites that distinguish an FSM N with no more than m states from M if this is possible in controllable testing. Thus, under the hypothesis that the system under test has no more than m states, a cm-complete test suite achieves as much as is possible given the restriction that testing should be controllable. We show how the problem of generating a cm-complete test suite can be mapped to the problem of generating an m-complete test suite for a partial FSM. Thus, standard test suite generation methods can be adapted for use in distributed testing.

Failed error propagation (FEP) is known to hamper software testing, yet it remains poorly understood. We introduce an information theoretic formulation of FEP that is based on measures of conditional entropy. This formulation considers the situation in which we are interested in the potential for an incorrect program state at statement s to fail to propagate to incorrect output. We define five metrics that differ in two ways: whether we only consider parts of the program that can be reached after executing s and whether we restrict attention to a single program path of interest .We give the results of experiments in which it was found that on average one in 10 tests suffered from FEP, earlier studies having shown that this figure can vary significantly between programs. The experiments also showed that our metrics are well-correlated with FEP. Our empirical study involved 30 programs, for which we executed a total of 7,140,000 test cases. The results reveal that the metrics differ in their performance but the Spearman rank correlation with failed error propagation is close to 0.95 for two of the metrics. These strong correlations in an experimental setting, in which all information about both FEP and conditional entropy is known, open up the possibility in the longer term of devising inexpensive information theory based metrics that allow us to minimise the effect of FEP.

Message sequence charts (MSCs) form a popular language in which scenario-based specifications and models can be written. There has been significant interest in automating aspects of testing from MSCs. This paper concerns the Oracle Problem, in which we have an observation made in testing and wish to know whether this is consistent with the specification. We assume that there is an MSC specification and consider the case where we have entirely independent local testers (local observability) and where the observations of the local testers are logged and brought together (tester observability). It transpires that, under local observability, the Oracle Problem can be solved in low-order polynomial time if we use sequencing, loops and choices, but becomes NP-complete if we also allow parallel components; if we place a bound on the number of parallel components, then it again can be solved in polynomial time. For tester observability, the problem is NP-complete when we have either loops or choices. However, it can be solved in low-order polynomial time if we have only one loop, no choices and no parallel components. If we allow parallel components, then the Oracle Problem is NP-complete for tester observability even if we restrict to the case where there are at most two processes.

Many systems interact with their environment at distributed interfaces (ports) and sometimes it is not possible to place synchronised local testers at the ports of the system under test (SUT). There are then two main approaches to testing: having independent local testers or a single centralised tester that interacts asynchronously with the SUT. The power of using independent testers has been captured using implementation relation dioco. In this article, we define implementation relation diococ for the centralised approach and prove that dioco and dioco c are incomparable. This shows that the frameworks detect different types of faults and so we devise a hybrid framework and define an implementation relation diocos for this. We prove that the hybrid framework is more powerful than the distributed and centralised approaches. We then prove that the Oracle problem is NP-complete for diococ and diocos but can be solved in polynomial time if we place an upper bound on the number of ports. Finally, we consider the problem of deciding whether there is a test case that is guaranteed to force a finite state model into a particular state or to distinguish two states, proving that both problems are undecidable for the centralised and hybrid frameworks.

This paper addresses refinement and testing based on CSP models, when we distinguish input and output events. From a testing perspective, there is an asymmetry: the tester (or the environment) controls the inputs, and the system under test controls the outputs. The standard models and refinement relations of CSP are, therefore, not entirely suitable for testing. Here, we adapt the CSP stable-failures model, resulting in the notion of input-output failures refinement. We compare that with the ioco relation often used in testing.Finally, we adapt the CSP testing theory, and show that some tests become unnecessary. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

This paper concerns testing from an input–output transition system (IOTS) model of a system under test that interacts with its environment through asynchronous first in first out (FIFO) channels. It explores methods for analysing an IOTS without modelling the channels. If IOTS M produces sequence σ, then, since communications are asynchronous, output can be delayed and so a different sequence might be observed. Thus, M defines a language Tr(M) of sequences that can be observed when interacting with M through FIFO channels. We define implementation relations and equivalences in terms of Tr(M): an implementation relation says how IOTS N must relate to IOTS M in order for N to be a correct implementation of M. It is important to use an appropriate implementation relation since otherwise the verdict from a test run might be incorrect and also because it influences test generation. It transpires that it is undecidable whether IOTS N conforms to IOTS M and so also whether there is a test case that can distinguish between two IOTSs. We also investigate the situation in which we have a finite automaton P and either wish to know whether Tr(M) ∩ L(P) is empty or whether Tr(M) ∩ Tr(P) is empty and prove that these are undecidable. In addition, we give conditions under which conformance and intersection are decidable.

This paper concerns state-based systems that interact with their environment at physically distributed interfaces, called ports. When such a system is used a projection of the global trace, a local trace, is observed at each port. As a result the environment has reduced observational power: the set of local traces observed need not define the global trace that occurred. We consider the previously defined implementation relation ⊆sand prove that it is undecidable whether N ⊆sM and so it is also undecidable whether testing can distinguishing two states or FSMs. We also prove that a form of model-checking is undecidable when we have distributed observations and give conditions under which N ⊆sM is decidable. We then consider implementation relation ⊆skthat concerns input sequences of length κ or less. If we place bounds on κ and the number of ports then we can decide N ⊆skM in polynomial time but otherwise this problem is NP-hard.

Slicing is useful for many software engineering applications and has been widely studied for three decades, but there has been comparatively little work on slicing extended finite state machines (EFSMs). This paper introduces a set of dependence-based EFSM slicing algorithms and an accompanying tool. We demonstrate that our algorithms are suitable for dependence-based slicing. We use our tool to conduct experiments on 10 EFSMs, including benchmarks and industrial EFSMs. Ours is the first empirical study of dependence-based program slicing for EFSMs. Compared to the only previously published dependence-based algorithm, our average slice is smaller 40 percent of the time and larger only 10 percent of the time, with an average slice size of 35 percent for termination insensitive slicing.

Testing real-time systems is a non-trivial validation task, especially after adding time as a new dimension to its complexity. In previous research, we introduced a 'priority-based' approach which tested the logical and timing behaviour of real-time systems modelled formally as UPPAAL Timed Automata (UTA). In this paper, we validate the 'priority-based' approach with a comparison to four well-known timed testing approaches based on a Timed Automata (TA) formalism using Specification Mutation Analysis (SMA). We introduce a set of timed and functional mutation operators based on TA. Three case studies are used to run the mutation analysis and mutants are generated according to the proposed mutation operators. The effectiveness of timed testing approaches are determined and contrasted according to the mutation score; we show that our testing approach achieves high mutation adequacy score when compared with others.

Semantic Mutation Testing (SMT) is a technique that aims to capture errors caused by possible misunderstandings of the semantics of a description language. This paper focuses on the use of SMT to represent possible problems caused by the use of Floating Point Comparison (FPC) since this feature of programming languages can lead to subtle errors. We describe six FPC semantic mutation operators that have been implemented in a C SMT tool. These operators mutate a C program by introducing tolerances using three different algorithms. The paper reports on the results of experiments that explored the proposed mutation operators. It was found that random test suites were not good at killing the resultant mutants, suggesting also that random test suites are poor at revealing FPC problems. We therefore devised a new approach to generate test data to kill these mutants. The manually generated test suites produced using the new approach were more effective in killing FPC mutants. In addition, the random test suites and manual test suites killed different sets of FPC mutants. The impact of using three different algorithms in FPC mutation was also investigated with no dominates relationships being found between the three types of FPC operators. Finally, we ran the same experiments on a computer with a different configuration. We found that slightly different sets of mutants were killed on the two computers, indicating that portability problems can be introduced by FPC.

Semantic Mutation Testing (SMT) is a technique that aims to capture errors caused by possible misunderstandings of the semantics of a description language. It is intended to target a class of errors which is different from those captured by traditional Mutation Testing (MT). This paper describes our experiences in the development of an SMT tool for the C programming language: SMT-C. In addition to implementing the essential requirements of SMT (generating semantic mutants and running SMT analysis) we also aimed to achieve the following goals: weak MT/SMT for C, good portability between different configurations, seamless integration into test routines of programming with C and an easy to use front-end.

In testing systems with distributed interfaces/ports, we may place a separate tester at each port. It is known that this approach can introduce controllability problems which have received much attention in testing from finite state machines. Message sequence charts (MSCs) form an alternative, commonly used, language for modelling distributed systems. However, controllability problems in testing from MSCs have not been thoroughly investigated. In this paper, controllability problems in MSC test cases are analysed with three notions of observability: local, tester and global. We identify two types of controllability problem in MSC-based testing. It transpires that each type of controllability problem is related to a type of MSC pathology. Controllability problems of timing are caused by races but not every race causes controllability problems; controllability problems of choice are caused by non-local choices and not every non-local choice causes controllability problems. We show that some controllability problems of timing are avoidable and some controllability problems of choice can be overcome when testers have better observational power. Algorithms are provided to tackle both types of controllability problems. Finally, we show how one can overcome controllability problems using a coordination service with status messages based on algorithms developed in this paper.

Abstract Formal methods are one of the most important approaches to increasing the confidence in the correctness of software systems. A formal specification can be used as an oracle in testing since one can determine whether an observed behaviour is allowed by the specification. This is an important feature of formal testing: behaviours of the system observed in testing are compared with the specification and ideally this comparison is automated. In this paper we study a formal testing framework to deal with systems that interact with their environment at physically distributed interfaces, called ports, and where choices between different possibilities are probabilistically quantified. Building on previous work, we introduce two families of schedulers to resolve nondeterministic choices among different actions of the system. The first type of schedulers, which we call global schedulers , resolves nondeterministic choices by representing the environment as a single global scheduler. The second type, which we call localised schedulers , models the environment as a set of schedulers with there being one scheduler for each port. We formally define the application of schedulers to systems and provide and study different implementation relations in this setting.

The problem of deciding whether one point in a program is data dependent upon another is fundamental to program analysis and has been widely studied. In this article we consider this problem at the abstraction level of program schemas in which computations occur in the Herbrand domain of terms and predicate symbols, which represent arbitrary predicate functions, are allowed. Given a vertex l in the flowchart of a schema S having only equality (variable copying) assignments, and variables v , w , we show that it is PSPACE-hard to decide whether there exists an execution of a program defined by S in which v holds the initial value of w at at least one occurrence of l on the path of execution, with membership in PSPACE holding provided there is a constant upper bound on the arity of any predicate in S . We also consider the ‘dual’ problem in which v is required to hold the initial value of w at every occurrence of l , for which the analogous results hold. Additionally, the former problem for programs with nondeterministic branching (in effect, free schemas) in which assignments with functions are allowed is proved to be polynomial-time decidable provided a constant upper bound is placed upon the number of occurrences of the concurrency operator in the schemas being considered. This result is promising since many concurrent systems have a relatively small number of threads (concurrent processes), especially when compared with the number of statements they have.

The problem of deciding whether an observed behavior is acceptable is the oracle problem. When testing from a finite state machine (FSM), it is easy to solve the oracle problem and so it has received relatively little attention for FSMs. However, if the system under test has physically distributed interfaces, called ports, then in distributed testing, we observe a local trace at each port and we compare the set of local traces with the set of allowed behaviors (global traces). This paper investigates the oracle problem for deterministic and nondeterministic FSMs and for two alternative definitions of conformance for distributed testing. We show that the oracle problem can be solved in polynomial time for the weaker notion of conformance (⊆w) but is NP-hard for the stronger notion of conformance (⊆), even if the FSM is deterministic. However, when testing from a deterministic FSM with controllable input sequences, the oracle problem can be solved in polynomial time and similar results hold for nondeterministic FSMs. Thus, in some cases, the oracle problem can be efficiently solved when using ⊆sand where this is not the case, we can use the decision procedure for ⊆was a sound approximation.

There are several industries in which Message Sequence Charts (MSCs) and the corresponding UML notation (Sequence Diagrams) are used to describe requirements. However, most work on model based testing has looked at testing from other languages such as input output transition systems and finite state machines. This paper explores the problem of testing on the basis of an MSC specification. We develop a formal test framework and explore the notion of a test hypothesis in this context. It transpires that there are several possible test architectures and each defines the observational power of the tester(s) and so we describe a flexible test architecture. In this paper we explore these alternatives and define corresponding implementation relations, explaining how verdicts can be produced for these relations. We then show how test suites can be generated and executed and define test coverage criteria.

This paper aims to construct an evolutionary system, based on genetic algorithms, to solve the problem of univocally reaching a target state in a non-deterministic Finite State Machine. Our approach proposes the creation of an adaptive sequence, which is a tree of input and outputs that contains the possible behaviors of the non-deterministic Finite State Machine, through a Genetic Algorithm. Essentially, we will characterize the DNA of the individuals as an adaptive sequence and allow the population to evolve until a solution is found. To assure the validity of our approach, we compare it with other methodologies such as hillclimbing and random. We show that the Genetic Algorithm obtains a higher rate of success in creating the adaptive sequences.

Given a program, a quotient can be obtained from it by deleting zero or more statements. The field of program slicing is concerned with computing a quotient of a program that preserves part of the behaviour of the original program. All program slicing algorithms take account of the structural properties of a program, such as control dependence and data dependence, rather than the semantics of its functions and predicates, and thus work, in effect, with program schemas. The dynamic slicing criterion of Korel and Laski requires only that program behaviour is preserved in cases where the original program follows a particular path, and that the slice/quotient follows this path. In this paper we formalise Korel and Laski's definition of a dynamic slice as applied to linear schemas, and also formulate a less restrictive definition in which the path through the original program need not be preserved by the slice. The less restrictive definition has the benefit of leading to smaller slices. For both definitions, we compute complexity bounds for the problems of establishing whether a given slice of a linear schema is a dynamic slice and whether a linear schema has a non-trivial dynamic slice, and prove that the latter problem is NP-hard in both cases. We also give an example to prove that minimal dynamic slices (whether or not they preserve the original path) need not be unique.

SUMMARY Distributed systems are usually composed of several distributed components that communicate with their environment through specific ports. When testing such a system we separately observe sequences of inputs and outputs at each port rather than a global sequence and potentially cannot reconstruct the global sequence that occurred. Typically, the users of such a system cannot synchronize their actions during use or testing. However, the use of the system might correspond to a sequence of scenarios, where each scenario involves a sequence of interactions with the system that, for example, achieves a particular objective. When this is the case there is the potential for a significant delay between two scenarios and this effectively allows the users of the system to synchronize between scenarios. If we represent the specification of the global system by using a state‐based notation, we say that ait scenario is any sequence of events that happens between two of these operations. We can encode scenarios in two different ways. The first approach consists of marking some of the states of the specification to denote these synchronization points. It transpires that there are two ways to interpret such models and these lead to two implementation relations. The second approach consists of adding a set of traces to the specification to represent the traces that correspond to scenarios. We show that these two approaches have similar expressive power by providing an encoding from marked states to sets of traces. In order to assess the appropriateness of our new framework, we show that it represents a conservative extension of previous implementation relations defined in the context of the distributed test architecture: if we consider that all the states are marked then we simply obtain ioco (the classical relation for single‐port systems) while if no state is marked then we obtain dioco (our previous relation for multi‐port systems). Finally, we concentrate on the study of controllable test cases, that is, test cases such that each local tester knows exactly when to apply inputs. We give two notions of controllable test cases, define an implementation relation for each of these notions and relate them. We also show how we can decide whether a test case satisfies these conditions. Copyright © 2011 John Wiley & Sons, Ltd.

This special issue contains extended versions of three papers from the first IEEE International Conference on Software Testing Verification and Validation (ICST 2008). These three papers were selected based on reviews from members of the program committee and subsequently subjected to another round of review and revision. All three papers focus on automated test generation and include significant empirical evaluation. However, they apply very different approaches to automation: model based, random, and white-box. The first paper by Ciupa, Pretschner, Oriol, Leitner, and Meyer offers an empirical investigation of a variant of random testing applied to object-oriented software. The nature of object-oriented systems complicates random testing since there is a need to introduce objects as well as to randomly generate input. The authors applied an approach in which an object was produced using a constructor call followed by routines that changed the object's state. This has the advantage of only generating valid objects. The (Eiffel) software to which random testing was applied contained contracts and these provided the oracle. The authors performed multiple runs of the same duration and examined the faults found. Interestingly, they found that the actual number of faults found did not vary too much but that different runs found different faults. The authors also classified faults and investigated the faults found by manual testing, random testing, and those in user incident reports. They discovered that these processes found different types of faults and hence are complementary. The second paper, by Bardin and Herrmann, investigates automated testing based on machine code rather than, for example, source code. One of the main motivations for this work is that often source code is not available, especially if parts of development have been outsourced. An additional motivation is that the machine code is closer, than the source code, to the physical system that actually runs. The authors observe that machine code is more difficult to analyse than source code in structured programming languages since, for example, the control flow is not explicit. However, they show that path-based approaches can be adapted and describe a tool (OSMOSE) that achieves this. The approach essentially can be seen as finding the path predicate (precondition) for a suitable path through the machine code and then solving this to find test input. The tool combines static and dynamic analysis in a manner inspired by concolic execution. Finally, they report on the results of experiments using OSMOSE. Our final paper by Grieskamp, Kicillof, Stobie, and Braberman discusses the development of interoperability documentation for Windows protocols within Microsoft and the use of test-driven approaches to verify that the documents accurately represent the protocols. The approaches used not only include manual testing but also a significant amount of model-based testing (MBT) using Microsoft's tool Spec Explorer. Vendors in India and China carried out the testing. A major focus of the paper is the use of MBT in this project. There are two main positive messages regarding MBT. First, it was found that the testers were able to apply MBT after an initial training course. Second, MBT was found to scale and to be significantly more efficient than manual testing. On a final note, we would like to express our gratitude to the many able and hard working people who were involved in the organization of ICST 2008 and this special issue. The steering committee members provided valuable advice and we were assisted by industry chairs Robert Eschbach, Per Runeson, and Clay Williams, student papers chairs Henry Muccini and Tao Xie, and by the general chair Lionel Briand. The success of ICST 2008 and also this special issue is testament to the efforts of these individuals as well as those who reviewed the papers for ICST 2008 and the special issue in a thorough and timely manner. We are also indebted to the ICST 2008 publicity chairs Harita Bhaskar, Yvan Labiche, Yves Le Traon, and T.H. Tse and the web chair Sudipto Ghosh. Finally, we thank all the authors who spent valuable time in preparing papers for ICST 2008 and this special issue.

Some systems have physically distributed interfaces, called ports, at which they interact with their environment. We place a tester at each port and if the testers cannot directly communicate and there is no global clock then we are using the distributed test architecture. It is known that this test architecture introduces controllability problems when testing from a deterministic finite state machine. This paper investigates the problem of testing from a nondeterministic finite state machine in the distributed test architecture and explores controllability. It shows how we can decide in polynomial time whether an input sequence is controllable. It also gives an algorithm for generating such an input sequence \bar{x} and shows how we can produce testers that implement \bar{x}.

A Feature Model (FM) is a compact representation of all the products of a software product line. The automated extraction of information from FMs is a thriving research topic involving a number of analysis operations, algorithms, paradigms and tools. Implementing these operations is far from trivial and easily leads to errors and defects in analysis solutions. Current testing methods in this context mainly rely on the ability of the tester to decide whether the output of an analysis is correct. However, this is acknowledged to be time-consuming, error-prone and in most cases infeasible due to the combinatorial complexity of the analyses. In this paper, we present a set of relations (so-called metamorphic relations) between input FMs and their set of products and a test data generator relying on them. Given an FM and its known set of products, a set of neighbour FMs together with their corresponding set of products are automatically generated and used for testing different analyses. Complex FMs representing millions of products can be efficiently created applying this process iteratively. The evaluation of our approach using mutation testing as well as real faults and tools reveals that most faults can be automatically detected within a few seconds.

A number of issues, such as non-local choice and implied scenarios, that arise in Message Sequence Charts (MSCs) have been investigated in the past. However, existing research on these two issues show disagreements regarding how they are related. In this paper, we analyse the relations among existing conditions for non-local choice free and Closure Conditions (CCs) for implied scenarios. On the basis of this, we propose a new definition for non-local choice and a non-local choice free condition derived from CCs of implied scenarios. Compared to existing conditions, we argue that the new condition covers more non-local choices that satisfy the informal idea of non-local choice. We formally show that the existence of non-local choices in an MSC specification results in implied scenarios and the appearance of implied scenarios according to corresponding CCs means there are non-local choices in the specification.

Some systems interact with their environment at physically distributed interfaces, called ports, and in testing such a system it is normal to place a tester at each port. Each tester observes only the events at its port and it is known that this limited observational power introduces additional controllability and observability problems into testing. Given a multiport finite state machine (FSM) M, we consider the problems of defining strategies for the testers either to reach a given state of M or to distinguish two states of M. These are important problems since most techniques for testing from a single-port FSM use sequences that reach and distinguish states. Both problems can be solved in low-order polynomial time for single-port FSMs but we prove that the corresponding decision problems are undecidable for multiport FSMs. However, we also show that they can be solved in low-order polynomial times for deterministic FSMs if we restrict our attention to controllable tests. These results have important ramifications for testing from a multiport FSM since they suggest that methods for testing from a single-port FSM cannot be easily adapted. In addition, two FSMs can be distinguished if and only if their initial states can be distinguished and so the results suggest that, in contrast to single-port FSMs, we cannot expect to produce general complete test generation methods for multiport FSMs.

The two most important aspects of any image based steganographic system are the imperceptibility and the capacity of the stego image. This paper evaluates the performance and efficiency of using optimized quantization tables instead of default JPEG tables within JPEG steganography. We found that using optimized tables significantly improves the quality of stego-images. Moreover, we used this optimization strategy to generate a 16x16 quantization table to be used instead of that suggested. The quality of stego-images was greatly improved when these optimized tables were used. This led us to suggest a new hybrid steganographic method in order to increase the embedding capacity. This new method is based on both and Jpeg-Jsteg methods. In this method, for each 16 x 16 quantized DCT block, the least two significant bits (2-LSBs) of each middle frequency coefficient are modified to embed two secret bits. Additionally, the Jpeg-Jsteg embedding technique is used for the low frequency DCT coefficients without modifying the DC coefficient. Our experimental results show that the proposed approach can provide a higher information-hiding capacity than the other methods tested. Furthermore, the quality of the produced stego-images is better than that of other methods which use the default tables.

The problem of testing from an extended finite state machine (EFSM) can be expressed in terms of finding suitable paths through the EFSM and then deriving test data to follow the paths. A chosen path may be infeasible and so it is desirable to have methods that can direct the search for appropriate paths through the EFSM towards those that are likely to be feasible. However, generating feasible transition paths (FTPs) for model based testing is a challenging task and is an open research problem. This paper introduces a novel fitness metric that analyzes data flow dependence among the actions and conditions of the transitions of a path in order to estimate its feasibility. The proposed fitness metric is evaluated by being used in a genetic algorithm to guide the search for FTPs.

Methods for testing from finite state machine-based specifications often require the existence of a preset distinguishing sequence for constructing checking sequences. It has been shown that an adaptive distinguishing sequence is sufficient for these methods. This result is significant because adaptive distinguishing sequences are strictly more common and up to exponentially shorter than preset ones. However, there has been no study on the actual effect of using adaptive distinguishing sequences on the length of checking sequences. This paper describes experiments that show that checking sequences constructed using adaptive distinguishing sequences are almost consistently shorter than those based on preset distinguishing sequences. This is investigated for three different checking sequence generation methods and the results obtained from an extensive experimental study are given.

In this paper we define simulation relations for distributed systems. Taking as starting point our previous work on the distributed testing architecture, we introduce novel simulation relations that can be used to define, given a specification, what a good implementation is. We approach the problem from two different perspectives. First, we consider that different ports of the system cannot share information. Thus, the decision to consider whether a system is correct has to be based only on local observations. We give some examples to show that this relation is very weak and propose a new one where we allow the different ports to {\it partially communicate}. Specifically, we do not implement a complex synchronization mechanism but allow entities to combine whole traces to obtain a verdict.

In state-based testing, it is common to include verdicts within test cases, the result of the test case being the verdict reached by the test run. In addition, approaches that reason about test effectiveness or produce tests that are guaranteed to find certain classes of faults are often based on either a fault domain or a set of test hypotheses. This article considers how the presence of a fault domain or test hypotheses affects our notion of a test verdict. The analysis reveals the need for new verdicts that provide more information than the current verdicts and for verdict functions that return a verdict based on a set of test runs rather than a single test run. The concepts are illustrated in the contexts of testing from a nondeterministic finite state machine and the testing of a datatype specified using an algebraic specification language but are potentially relevant whenever fault domains or test hypotheses are used.

The two most important aspects of any image-based steganographic system are the quality of the stego-image and the capacity of the cover image. This paper proposes a novel and high capacity steganographic approach based on Discrete Cosine Transformation (DCT) and JPEG compression. JPEG technique divides the input image into non-overlapping blocks of 8times8 pixels and uses the DCT transformation. However, our proposed method divides the cover image into non- overlapping blocks of 16times16 pixels. For each quantized DCT block, the least two-significant bits (2-LSBs) of each middle frequency coefficient are modified to embed two secret bits. Our aim is to investigate the data hiding efficiency using larger blocks for JPEG compression. Our experiment result shows that the proposed approach can provide a higher information- hiding capacity than Jpeg-Jsteg and Chang et al. methods based on the conventional blocks of 8times8 pixels. Furthermore, the produced stego-images are almost identical to the original cover images.

Stream X-machines are a kind of extended finite state machine used to specify real systems where communication between the components is modeled by using a shared memory.In this paper we introduce an extension of the Stream X-machines formalism in order to specify delays/timeouts.The time spent by a system waiting for the environment to react has the capability of affecting the set of available outputs of the system. So, a relation focusing on functional aspects must explicitly take into account the possible timeouts.We also propose a formal testing methodology allowing to systematically test a system with respect to a specification. Finally, we introduce a test derivation algorithm. Given a specification, the derived test suite is sound and complete, that is, a system under test successfully passes the test suite if and only if this system conforms to the specification.

There has been much interest in testing from finite-state machines (FSMs). If the system under test can be modelled by the (minimal) FSM N then testing from an (minimal) FSM M is testing to check that N is isomorphic to M. In the distributed test architecture, there are multiple interfaces/ports and there is a tester at each port. This can introduce controllability/synchronization and observability problems. This paper shows that the restriction to test sequences that do not cause controllability problems and the inability to observe the global behaviour in the distributed test architecture, and thus relying only on the local behaviour at remote testers, introduces fundamental limitations into testing. There exist minimal FSMs that are not equivalent, and so are not isomorphic, and yet cannot be distinguished by testing in this architecture without introducing controllability problems. Similarly, an FSM may have non-equivalent states that cannot be distinguished in the distributed test architecture without causing controllability problems: these are said to be locally s-equivalent and otherwise they are locally s-distinguishable. This paper introduces the notion of two states or FSMs being locally s-equivalent and formalizes the power of testing in the distributed test architecture in terms of local s-equivalence. It introduces a polynomial time algorithm that, given an FSM M, determines which states of M are locally s-equivalent and produces minimal length input sequences that locally s-distinguish states that are not locally s-equivalent. An FSM is locally s-minimal if it has no pair of locally s-equivalent states. This paper gives an algorithm that takes an FSM M and returns a locally s-minimal FSM M′ that is locally s-equivalent to M.

Abstract A stream X-machine (SXM) is a type of extended finite state machine with an associated development approach that consists of building a system from a set of trusted components. One of the great benefits of using SXMs for the purpose of specification is the existence of test generation techniques that produce test suites that are guaranteed to determine correctness as long as certain well-defined conditions hold. One of the conditions that is traditionally assumed to hold is controllability: this insists that all paths through the SXM are feasible. This restrictive condition has recently been weakened for testing from a deterministic SXM. This paper shows how controllability can be replaced by a weaker condition when testing a deterministic system against a non-deterministic SXM. This paper therefore develops a new, more general, test generation algorithm for testing from a non-deterministic SXM.

The mechanics of seventy-two different Java refactorings are described fully in Fowler's text. In the same text, Fowler describes seven categories of refactoring, into which each of the seventy-two refactorings can be placed. A current research problem in the refactoring and XP community is assessing the likely time and testing effort for each refactoring, since any single refactoring may use any number of other refactorings as part of its mechanics and, in turn, can be used by many other refactorings. In this paper, we draw on a dependency analysis carried out as part of our research in which we identify the 'Use' and 'Used By' relationships of refactorings in all seven categories. We offer reasons why refactorings in the 'Dealing with Generalisation' category seem to embrace two distinct refactoring sub-categories and how refactorings in the 'Moving Features between Objects' category also exhibit specific characteristics. In a wider sense, our meta-analysis provides a developer with concrete guidelines on which refactorings, due to their explicit dependencies, will prove problematic from an effort and testing perspective.

The sequence diagram is one of the most popular behaviour modelling languages which offers an intuitive and visual way of describing expected behaviour of object-oriented software. Much research work has investigated ways of providing a formal semantics for sequence diagrams. However, these proposed semantics may not properly interpret sequence diagrams when lifelines do not correspond to threads of controls. In this paper, we address this problem and propose a thread-tag based sequence diagram as a solution. A formal, partially ordered multiset based semantics for the thread-tag based sequence diagrams is proposed.

Abstract When testing from finite state machines, a failure observed in the implementation under test (IUT) is called a symptom. A symptom could have been caused by an earlier state transfer failure. Transitions that may be used to explain the observed symptoms are called diagnosing candidates. Finding strategies to generate an optimal set of diagnosing candidates that could effectively identify faults in the IUT is of great value in reducing the cost of system development and testing. This paper investigates fault diagnosis when testing from finite state machines and proposes heuristics for fault isolation and identification. The proposed heuristics attempt to lead to a symptom being observed in some shorter test sequences, which helps to reduce the cost of fault isolation and identification. The complexity of the proposed method is analysed. A case study is presented, which shows how the proposed approach assists in fault diagnosis. Copyright © 2006 John Wiley & Sons, Ltd.

Regression testing is an expensive, but important, process. Unfortunately, there may be insufficient resources to allow for the reexecution of all test cases during regression testing. In this situation, test case prioritization techniques aim to improve the effectiveness of regression testing by ordering the test cases so that the most beneficial are executed first. Previous work on regression test case prioritization has focused on Greedy Algorithms. However, it is known that these algorithms may produce suboptimal results because they may construct results that denote only local minima within the search space. By contrast, metaheuristic and evolutionary search algorithms aim to avoid such problems. This paper presents results from an empirical study of the application of several greedy, metaheuristic, and evolutionary search algorithms to six programs, ranging from 374 to 11,148 lines of code for three choices of fitness metric. The paper addresses the problems of choice of fitness metric, characterization of landscape modality, and determination of the most suitable search technique to apply. The empirical results replicate previous results concerning Greedy Algorithms. They shed light on the nature of the regression testing search space, indicating that it is multimodal. The results also show that Genetic Algorithms perform well, although Greedy approaches are surprisingly effective, given the multimodal nature of the landscape.

This paper describes a method for automatically generating unique input output (UIO) sequences for FSM conformance testing. UIOs are used in conformance testing to verify the end state of a transition sequence. UIO sequence generation is represented as a search problem and genetic algorithms are used to search this space. Empirical evidence indicates that the proposed method yields considerably better (up to 62% better) results compared with random UIO sequence generation.

No abstract available.

A checking sequence, generated from a finite state machine, is a test sequence that is guaranteed to lead to a failure if the system under test is faulty and has no more states than the specification. The problem of generating a checking sequence for a finite state machine M is simplified if M has a distinguishing sequence: an input sequence D~ with the property that the output sequence produced by M in response to D is different for the different states of M. Previous work has shown that, where a distinguishing sequence is known, an efficient checking sequence can be produced from the elements of a set A of sequences that verify the distinguishing sequence used and the elements of a set /spl gamma/ of subsequences that test the individual transitions by following each transition t by the distinguishing sequence that verifies the final state of t. In this previous work, A is a predefined set and /spl gamma/ is defined in terms of A. The checking sequence is produced by connecting the elements of /spl gamma/ and A to form a single sequence, using a predefined acyclic set E/sub c/ of transitions. An optimization algorithm is used in order to produce the shortest such checking sequence that can be generated on the basis of the given A and E/sub c/. However, this previous work did not state how the sets A and E/sub c/ should be chosen. This paper investigates the problem of finding appropriate A and E/sub c/ to be used in checking sequence generation. We show how a set A may be chosen so that it minimizes the sum of the lengths of the sequences to be combined. Further, we show that the optimization step, in the checking sequence generation algorithm, may be adapted so that it generates the optimal E/sub c/. Experiments are used to evaluate the proposed method.

In partition analysis we divide the input domain to form subdomains on which the system's behaviour should be uniform. Boundary value analysis produces test inputs near each subdomain's boundaries to find failures caused by incorrect implementation of the boundaries. However, boundary value analysis can be adversely affected by coincidental correctness---the system produces the expected output, but for the wrong reason. This article shows how boundary value analysis can be adapted in order to reduce the likelihood of coincidental correctness. The main contribution is to cases of automated test data generation in which we cannot rely on the expertise of a tester.

No abstract available.

Program slicing is an automated source code extraction technique that has been applied to a number of problems including testing, debugging, maintenance, reverse engineering, program comprehension, reuse and program integration. In all these applications the size of the slice is crucial; the smaller the better. It is known that statement minimal slices are not computable, but the question of dataflow minimal slicing has remained open since Weiser posed it in 1979. This paper proves that static slicing algorithms produce dataflow minimal end slices for programs which can be represented as schemas which are free and liberal.

Test data generation by hand is a tedious, expensive and error-prone activity, yet testing is a vital part of the development process. Several techniques have been proposed to automate the generation of test data, but all of these are hindered by the presence of unstructured control flow. This paper addresses the problem using testability transformation. Testability transformation does not preserve the traditional meaning of the program, rather it deals with preserving test-adequate sets of input data. This requires new equivalence relations which, in turn, entail novel proof obligations. The paper illustrates this using the branch coverage adequacy criterion and develops a branch adequacy equivalence relation and a testability transformation for restructuring. It then presents a proof that the transformation preserves branch adequacy.

Abstract Program slicing and concept assignment have both been proposed as source code extraction techniques. Unfortunately, each has a weakness that prevents wider application. For slicing, the extraction criterion is expressed at a very low level; constructing a slicing criterion requires detailed code knowledge which is often unavailable. The concept assignment extraction criterion is expressed at the domain level. However, unlike a slice, the extracted code is not executable as a separate subprogram in its own right. This paper introduces a unification of slicing and concept assignment which exploits their combined advantages, while overcoming these two individual weaknesses. Our ‘concept slices’ are executable programs extracted using high‐level criteria. The paper introduces four techniques that combine slicing and concept assignment and algorithms for each. These algorithms were implemented in two separate tools used to illustrate the application of the concept slicing algorithms in two very different case studies. The first is a commercially‐written COBOL module from a large financial organization, the second is an open source utility program written in C. Copyright © 2005 John Wiley & Sons, Ltd.

Validating our findingsIf we come up with a new approach such as a new testing technique how do we know that it is any good?In other words, how do we evaluate our research?This is a surprisingly controversial topic in software testing and, indeed, in software engineering as a whole.One of the many nice things about this issue of STVR is the variety of evaluation methods used.At one extreme, the authors of the first paper formally define the problem they are aiming to solve, give two new testing methods and evaluate these by proving that they have the required properties.Naturally, a strength of this theoretical approach is that (assuming the proofs are correct!)we know that the results always hold.However, many other problems are not amenable to this method of evaluation and our other papers both use one of the main alternatives: empirical investigations.Of particular note here is the third paper whose authors replicate a previous study using a different sample of programs.It is extremely encouraging to see this: replication of experiments is common practice in the physical sciences but has been much less usual in software engineering.Hopefully this will become a trend and we will see many more replicated experiments in the future.Turning in more detail to the contents of this issue, the first paper, by Manuel Núñez, Ismael Rodríguez and Fernando Rubio, considers the problem of testing the behaviour of an e-commerce agent that has been specified as a 'utility state machine'.A utility state machine is like a standard extended finite state machine with the addition of time and a utility function for each state.In essence, the utility function for a state represents what the agent is trying to achieve in this state; when in this state, the agent can exchange resources with other agents if such exchanges increase its utility.State transitions occur under specified conditions and can be seen as moving the agent to a new state representing a different objective when the current objective is achieved.The authors describe two forms of testing such an agent: active testing in which we introduce a tester as another agent to interact with the agent being tested; and passive testing in which we observe the behaviour of the agent acting in its context.To complement the formal validation mentioned in the first paragraph above, the authors have also presented a case study whereby the formalism was applied to a system called Kasbah: a pioneering multi-agent e-commerce system for buying and selling goods.The second paper, by Daniel Hoffman, Paul Strooper and Sarah Wilkin, describes a new tool, JUnitDoc, which is based on the tools JUnit and Javadoc.The key idea is that Javadoc comments are used in order to embed test cases in the code.These test cases assist in documenting the code since they are examples of expected behaviour and Javadoc can be used to extract them as HTML documentation.They can also be extracted in order to produce JUnit test drivers.The authors suggest that test cases are placed as high as possible in the inheritance hierarchy in order to generate a test hierarchy that mirrors the inheritance hierarchy.A detailed example demonstrates the benefits for testing and, in addition, a small controlled experiment was conducted to compare the readability of the JUnitDoc documentation to formal specifications written in Object-Z.The results of this evaluation

Abstract Conditioned slicing is a source code extraction technique. The extraction is performed with respect to a slicing criterion which contains a set of variables and conditions of interest. Conditioned slicing removes the parts of the original program which cannot affect the variables at the point of interest, when the conditions are satisfied. This produces a conditioned slice, which preserves the behaviour of the original with respect to the slicing criterion. Conditioned slicing has applications in source code comprehension, reuse, restructuring and testing. Unfortunately, implementation is not straightforward because the full exploitation of conditions requires the combination of symbolic execution, theorem proving and traditional static slicing. Hitherto, this difficultly has hindered development of fully automated conditioning slicing tools. This paper describes the first fully automated conditioned slicing system, CONSIT, detailing the theory that underlies it, its architecture and the way it combines symbolic execution, theorem proving and slicing technologies. The use of CONSIT is illustrated with respect to the applications of testing and comprehension. Copyright © 2003 John Wiley & Sons, Ltd.

Methods and Testing

The problem of generating a checking experiment from a nondeterministic finite state machine has been represented in terms of state counting. However, test techniques that use state counting traditionally produce preset test suites. We extend the notion of state counting in order to allow the input/output sequences observed in testing to be utilized: Adaptive state counting is introduced. The main benefit of the proposed approach is that it may result in a reduction in the size of the test suite used. An additional benefit is that, where a failure is observed, it is possible to terminate test generation at this point.

A testability transformation is a source-to-source transformation that aims to improve the ability of a given test generation method to generate test data for the original program. We introduce testability transformation, demonstrating that it differs from traditional transformation, both theoretically and practically, while still allowing many traditional transformation rules to be applied. We illustrate the theory of testability transformation with an example application to evolutionary testing. An algorithm for flag removal is defined and results are presented from an empirical study which show how the algorithm improves both the performance of evolutionary test data generation and the adequacy level of the test data so-generated.

Automated software module clustering is important for maintenance of legacy systems written in a 'monolithic format' with inadequate module boundaries. Even where systems were originally designed with suitable module boundaries, structure tends to degrade as the system evolves, making re-modularization worthwhile. This paper focuses upon search-based approaches to the automated module clustering problem, where hitherto, the local search approach of hill climbing has been found to be most successful. In the paper we show that results from a set of multiple hill climbs can be combined to locate good 'building blocks' for subsequent searches. Building blocks are formed by identifying the common features in a selection of best hill climbs. This process reduces the search space, while simultaneously 'hard wiring' parts of the solution. The paper reports the results of an empirical study that show that the multiple hill climbing approach does indeed guide the search to higher peaks in subsequent executions. The paper also investigates the relationship between the improved results and the system size.

This paper considers the problem of testing a deterministic system against a non-deterministic finite-state machine. An adaptive test process, with two phases, is proposed. The paper focuses on the first stage which involves testing to generate a candidate deterministic finite-state machine. This candidate has the property that, under the test hypotheses used, the implementation is correct if and only if it is equivalent to the candidate. A test may then be derived from the candidate.

Testing in the large through the small?We are frequently told that computer systems are becoming increasingly complex.Assuming this is the case, does this make testing more difficult?We are also told that computer systems are becoming increasingly significant.Does this make it even more important that our testing is effective?If the answer to both of these questions is 'yes' then we seem to have a real problem.This might help explain the results of a recent study by the National Institute of Standards and Technology [1].This concluded that the cost to the U.S. economy, of poor testing, was in the order of 59.5 billion dollars a year.I am sure that such problems are not restricted just to the U.S.!So, what is the solution?If I had the answer to this question it is just possible that I would currently be in rather more luxurious surroundings.However, I hope that the contents of this issue point to one approach that can help and illustrates links between a number of approaches.This issue's three papers relate to a theme: how can we test 'large/complex' systems by testing 'small/simple' systems?Naturally, this is an important issue-system complexity continues to increase and we all know that many of our favourite testing/verification techniques struggle beyond some level of complexity.This problem is exacerbated by the development of distributed state-based systems: here the number of states of the overall system grows exponentially as the number of components increases.The papers all approach this problem by using some of the scientist's favourite tools.Specifically, they use at least one of abstraction (abstract away details to simplify the problem) and reductionism (break the problem into sub-problems and tackle these).Reductionism is applied through the identification and testing of components.In their paper entitled 'Test suite minimization for testing in context', Anido et al. consider the problem of testing a single component embedded within a context that is known to be correct.Thus, rather than considering the testing of the entire system, they look at the testing of the single component (it is possible that the user/environment cannot send test input directly to this component and cannot receive test output directly from this component).They show that a given test suite may be reduced by considering how each test sequence within it contributes to the testing of the suspect component.Assuming the context is correct, this process is guaranteed to preserve the test suite's effectiveness.By contrast, Rusu, in his paper entitled 'Combining formal verification and conformance testing for validating reactive systems', extracts components from the specification and tests on the basis of these.The papers of Anido et al. and Rusu have another common element: compositionality.So, how do these papers apply abstraction?De Francesco and Lettieri, in their paper entitled 'Checking security properties by model checking', show that a program may be simplified, through abstraction, if we want to verify that certain security problems do not exist.Once this abstraction has been applied, model-checking techniques are used, through the Symbolic Model Verifier (SMV) tool, to determine whether these security problems exist.Importantly, if the abstracted model does not have

Formal methods have traditionally been used for specification and development of software. However there are potential benefits for the testing stage as well. The panel session associated with this paper explores the usefulness or otherwise of formal methods in various contexts for improving software testing. A number of different possibilities for the use of formal methods are explored and questions raised. The contributors are all members of the UK FORTEST Network on formal methods and testing. Although the authors generally believe that formal methods are useful in aiding the testing process, this paper is intended to provoke discussion. Dissenters are encouraged to put their views to the panel or individually to the authors.

The problem of testing from an extended finite state machine (EFSM) is complicated by the presence of infeasible paths. This paper considers the problem of expanding an EFSM in order to bypass the infeasible path problem. The approach is developed for the specification language SDL but, in order to aid generality, the rewriting process is broken down into two phases: producing a normal form EFSM (NF-EFSM) from an SDL specification and then expanding this NF-EFSM.

Evolutionary testing is a search based approach to the automated generation of systematic test data, in which the search is guided by the test data adequacy criterion. Two problems for evolutionary testing are the large size of the search space and structural impediments in the implementation of the program which inhibit the formulation of a suitable fitness function to guide the search. In this paper we claim that slicing can be used to narrow the search space and transformation can be applied to the problem of structural impediments. The paper presents examples of how these two techniques have been successfully employed to make evolutionary testing both more efficient and more effective.

Side-effects are widely believed to impede program comprehension and have a detrimental effect upon software maintenance. This paper introduces an algorithm for side-effect removal which splits the side-effects into their pure expression meaning and their state-changing meaning. Symbolic execution is used to determine the expression meaning, while transformation is used to place the state-changing part in a suitable location in a transformed version of the program. This creates a program which is semantically equivalent to the original but guaranteed to be free from side-effects. The paper also reports the results of an empirical study which demonstrates that the application of the algorithm causes a significant improvement in program comprehension.

Abstract This paper describes the use of conditioned slicing to assist partition testing, illustrating this with a case study. The paper shows how a conditioned slicing tool can be used to provide confidence in the uniformity hypothesis for correct programs, to aid fault detection in incorrect programs and to highlight special cases. Copyright © 2001 John Wiley & Sons, Ltd

Here, the method proposed by Ural, Wu and Zhang (1997) for constructing minimal-length checking sequences based on distinguishing sequences is improved. The improvement is based on optimizations of the state recognition sequences and their use in constructing test segments. It is shown that the proposed improvement further reduces the length of checking sequences produced from minimal, completely specified, and deterministic finite state machines.

A number of authors have considered the problem of comparing test sets and criteria. Ideally test sets are compared using a preorder with the property that test set T 1 is at least as strong as T 2 if whenever T 2 determines that an implementation p is faulty, T 1 will also determine that p is faulty. This notion can be extended to test criteria. However, it has been noted that very few test sets and criteria are comparable under such an ordering; instead orderings are based on weaker properties such as subsumes. This article explores an alternative approach, in which comparisons are made in the presence of a test hypothesis or fault domain. This approach allows strong statements about fault detecting ability to be made and yet for a number of test sets and criteria to be comparable. It may also drive incremental test generation.

Th paper shows how analysis of programs in terms of pre- and postconditions can be improved using a generalisation of conditioned program slicing called pre/post conditioned slicing. Such conditions play an important role in program comprehension, reuse, verification and reengineering. Fully automated analysis is impossible because of the inherent undecidability of pre- and post- conditions. The method presented reformulates the problem to circumvent this. The reformulation is constructed so that programs which respect the pre- and post-conditions applied to them have empty slices. For those which do not respect the conditions, the slice contains statements which could potentially break the conditions. This separates the automatable part of the analysis from the human analysis.

Conditioned slicing is a powerful generalisation of static and dynamic slicing which has applications to many problems in software maintenance and evolution, including reuse, reengineering and program comprehension. However there has been relatively little work on the implementation of conditioned slicing. Algorithms for implementing conditioned slicing necessarily involve reasoning about the values of program predicates in certain sets of states derived from the conditioned slicing criterion, making implementation particularly demanding. The paper introduces ConSIT, a conditioned slicing system which is based upon conventional static slicing, symbolic execution and theorem proving. ConSIT is the first fully automated implementation of conditioned slicing. An implementation of ConSIT is available for experimentation at http://www.mcs.gold.ac.uk//spl tilde/mas01sd/consit.html.

Abstract. Stream X-machines have been used in order to specify a range of systems. One of the strengths of this approach is that, under certain well-defined conditions, it is possible to produce a finite test that is guaranteed to determine the correctness of the implementation under test (IUT). Initially only deterministic stream X-machines were considered in the literature. This is largely because the standard test algorithm relies on the stream X-machine being deterministic. More recently the problem of testing to determine whether the IUT is equivalent to a non-deterministic stream X-machine specification has been tackled. Since non-determinism can be important for specifications, this is an extremely useful extension. In many cases, however, we wish to test for a weaker notion of correctness called conformance . This paper considers a particular form of non-determinism, within stream X-machines, that will be called quasi-non-determinism. It then investigates the generation of tests that are guaranteed to determine whether the IUT conforms to a quasi-non-deterministic stream X-machine specification. The test generation algorithm given is a generalisation of that used for testing from a deterministic stream X-machine.

While mutation testing has proved to be an effective way of finding software faults, currently it is only applied to relatively small programs. One of the main reasons for this is the human analysis required in detecting equivalent mutants. Here program slicing is used to simplify this problem. Progam slicing is also used to reduce the number of equivalent mutants produced. Copyright © 1999 John Wiley & Sons, Ltd.

A number of authors have looked at the problem of deriving a checking experiment from a nondeterministic finite state machine that models the required behaviour of a system. We show that these methods can be extended if it is known that the implementation is equivalent to some (unknown) deterministic finite state machine. When testing a deterministic implementation, the test output provides information about the implementation under test and can thus guide future testing. The use of an adaptive test process is thus proposed.

When testing a system modelled as a finite state machine it is desirable to minimize the effort required. It has been demonstrated that it is possible to utilize test sequence overlap in order to reduce the test effort and this overlap has been represented by using invertible transitions. In this paper invertibility will be extended to sequences in order to reduce the test effort further and encapsulate a more general type of test sequence overlap. It will also be shown that certain properties of invertible sequences can be used in the generation of state identification sequences.

This paper looks at the formal analysis of Z specifications in order to enhance the testing process. An algorithm is given that rewrites the specification to a form from which both a partition of the input domain and the states of a finite state automaton model can be derived. Test cases can be derived from the former and an automated system to control the testing process can be based upon the latter. © 1997 by John Wiley & Sons, Ltd.

Failure rate, given an operational profile, is a common measure of reliability. A number of approaches to estimating failure rate are described and it is demonstrated that, under certain conditions, a functional partition can provide a better estimator than random-testing-based estimators. © 1997 John Wiley & Sons, Ltd.

Finite state automata can be used to model a system; in particular they can be used to model the control section of a communications protocol. A number of authors have produced algorithms that represent the problem of minimizing the testing against a finite state automaton model as a max flow/min cost problem for an associated network. We extend this work by introducing the use of invertibility to utilize test sequence overlap.