Summary With the ever‐growing Android graphical user interface (GUI) application market, there have been many studies on automated test generation for Android GUI applications. These studies successfully demonstrate how to detect fatal exceptions and achieve high coverage with fully automated test generation engines. However, it is unclear how many GUI functions these engines manage to test. The current best practice for the functional testing of Android GUI applications is to design user interface (UI) test scenarios with a non‐technical and human‐readable language such as Gherkin and implement Java/Kotlin methods for every statement of all the UI test scenarios. Writing tests for UI test scenarios is hard, especially when some scenario statements are high‐level and declarative, so it is not clear what actions should the generated test perform. We propose the Fully Automated Reinforcement LEArning‐Driven specification‐based test generator for Android (FARLEAD‐Android). FARLEAD‐Android first translates the UI test scenario to a GUI‐level formal specification as a linear‐time temporal logic (LTL) formula. The LTL formula guides the test generation and acts as a specified test oracle. By dynamically executing the application under test (AUT), and monitoring the LTL formula, FARLEAD‐Android learns how to produce a witness for the UI test scenario, using reinforcement learning (RL). Our evaluation shows that FARLEAD‐Android is more effective and achieves higher performance in generating tests for UI test scenarios than three known engines: Random, Monkey and QBEa. To the best of our knowledge, FARLEAD‐Android is the first fully automated mobile GUI testing engine that uses formal specifications.

Deep Learning (DL) systems are key enablers for engineering intelligent applications due to their ability to solve complex tasks such as image recognition and machine translation. Nevertheless, using DL systems in safety- and security-critical applications requires to provide testing evidence for their dependable operation. Recent research in this direction focuses on adapting testing criteria from traditional software engineering as a means of increasing confidence for their correct behaviour. However, they are inadequate in capturing the intrinsic properties exhibited by these systems. We bridge this gap by introducing DeepImportance, a systematic testing methodology accompanied by an Importance-Driven (IDC) test adequacy criterion for DL systems. Applying IDC enables to establish a layer-wise functional understanding of the importance of DL system components and use this information to assess the semantic diversity of a test set. Our empirical evaluation on several DL systems, across multiple DL datasets and with state-of-the-art adversarial generation techniques demonstrates the usefulness and effectiveness of DeepImportance and its ability to support the engineering of more robust DL systems.

Deep Neural Networks (DNNs) are increasingly deployed in safety-critical applications including autonomous vehicles and medical diagnostics. To reduce the residual risk for unexpected DNN behaviour and provide evidence for their trustworthy operation, DNNs should be thoroughly tested. The DeepFault whitebox DNN testing approach presented in our paper addresses this challenge by employing suspiciousness measures inspired by fault localization to establish the hit spectrum of neurons and identify suspicious neurons whose weights have not been calibrated correctly and thus are considered responsible for inadequate DNN performance. DeepFault also uses a suspiciousness-guided algorithm to synthesize new inputs, from correctly classified inputs, that increase the activation values of suspicious neurons. Our empirical evaluation on several DNN instances trained on MNIST and CIFAR-10 datasets shows that DeepFault is effective in identifying suspicious neurons. Also, the inputs synthesized by DeepFault closely resemble the original inputs, exercise the identified suspicious neurons and are highly adversarial.

In system-on-chip design, resources for verification is limited by time-to-market and cost. In order to allocate verification resources effectively, managers need to rely on their experience backed by design related metrics. However, often there are also other aspects of development process, such as bug history and developer information that can improve the effectiveness of verification. Software bug prediction is a machine learning (ML)-based technique which predicts whether a given software module is bug-prone by using product and process metrics of the module. Therefore, it can help direct verification effort, reduce costs, and improve the quality of software. Although there is a plethora of work in software bug prediction, no such work exists for SystemC. We propose an ML-based software bug prediction solution for verification of SystemC models used in virtual prototypes that takes into account system level design metrics and demonstrate its effectiveness on several open source system level designs. We find that 96% of modules could be correctly predicted as buggy or clean.

GUI testing of mobile applications gradually became a very important topic in the last decade with the growing mobile application market. We propose Test Case Mutation (TCM) which mutates existing test cases to produce richer test cases. These mutated test cases detect crashes that are not previously detected by existing test cases. TCM differs from the well-known Mutation Testing (MT) where mutations are inserted in the source code of an Application Under Test (AUT) to measure the quality of test cases. Whereas in TCM, we modify existing test cases and obtain new ones to increase the number of detected crashes. Android applications take the largest portion of the mobile application market. Hence, we evaluate TCM on Android by replaying mutated test cases of randomly selected $$100$$ AUTs from F-Droid benchmarks. We show that TCM is effective at detecting new crashes in a given time budget.

Android applications are used extensively around the world. Many of these applications contain potential crashes. Black-box testing of Android applications has been studied over the last decade to detect these crashes. In this paper, we propose QLearning-Based Exploration (QBE), a fully automated black-box testing methodology, which explores GUI actions using a well-known reinforcement learning technique called QLearning. QBE performs automata learning to obtain a model of the AUT, and generates replayable test suites. Specifically, QBE learns from a set of existing applications the kinds of actions that are most useful in order to reach a particular objective such as detecting crashes or increasing activity coverage. To the best of our knowledge, ours is the first machine learning based approach in Android GUI Testing. We conduct experiments on a test set of 100 AUTs obtained from the commonly used F-Droid benchmarks to show the effectiveness of QBE. We show that QBE performs better than all compared black-box tools in terms of activity coverage and number of distinct detected crashes. We make QBE and our experimental data available online.

In this study, we investigate the effect of EC on the defect-proneness of large industrial software systems and explain why the effects vary.

Programming of multicore architectures with large number of cores is a huge burden on the programmer. Parallel patterns ease this burden by presenting the developer with a set of predefined programming patterns that implement best practices in parallel programming. Since the behavior of patterns is well-known and understood they can also lower the burden for verification. In this work, we present a toolset, MINIME-Validator, for generating synthetic parallel testcases from a newly defined Parallel Pattern Markup Language (PPML) that uses the concept of parallel patterns. Our testcases mimic the behavior of real customer applications while being much smaller and can be used to generate traffic and validate e.g. inter-processor communication architectures. Experiments show that synthetic testcases can be used for finding representative hardware communication problems. To the best of our knowledge, this is the first time synthetic testcases using parallel programming patterns are used for hardware validation.

Abstract Evolutionary coupling (EC) is defined as the implicit relationship between 2 or more software artifacts that are frequently changed together. Changing software is widely reported to be defect‐prone. In this study, we investigate the effect of EC on the defect proneness of large industrial software systems and explain why the effects vary. We analysed 2 large industrial systems: a legacy financial system and a modern telecommunications system. We collected historical data for 7 years from 5 different software repositories containing 176 thousand files. We applied correlation and regression analysis to explore the relationship between EC and software defects, and we analysed defect types, size, and process metrics to explain different effects of EC on defects through correlation. Our results indicate that there is generally a positive correlation between EC and defects, but the correlation strength varies. Evolutionary coupling is less likely to have a relationship to software defects for parts of the software with fewer files and where fewer developers contributed. Evolutionary coupling measures showed higher correlation with some types of defects (based on root causes) such as code implementation and acceptance criteria. Although EC measures may be useful to explain defects, the explanatory power of such measures depends on defect types, size, and process metrics.

We introduce MINIME-GPU, a novel automated benchmark synthesis framework for graphics processing units (GPUs) that serves to speed up architectural simulation of modern GPU architectures. Our framework captures important characteristics of original GPU applications and generates synthetic GPU benchmarks using the Open Computing Language (OpenCL) library from those applications. To the best of our knowledge, this is the first time synthetic OpenCL benchmarks for GPUs are generated from existing applications. We use several characteristics, including instruction throughput, compute unit occupancy, and memory efficiency, to compare the similarity of original applications and their corresponding synthetic benchmarks. The experimental results show that our synthetic benchmark generation framework is capable of generating synthetic benchmarks that have similar characteristics with the original applications from which they are generated. On average, the similarity (accuracy) is 96% and the speedup is 541 ×. In addition, our synthetic benchmarks use the OpenCL library, which allows us to obtain portable human readable benchmarks as opposed to using assembly-level code, and they are faster and smaller than the original applications from which they are generated. We experimentally validated that our synthetic benchmarks preserve the characteristics of the original applications across different architectures.

We present a novel automated multicore benchmark synthesis framework with characterization and generation components. Our framework uses parallel patterns in capturing important characteristics of multi-threaded applications and generates synthetic multicore benchmarks from those applications. The resulting synthetic benchmarks are small, fast, portable, human-readable, and they accurately reflect microarchitecture dependent and independent characteristics of the original multicore applications. Also, they can use either Pthreads or MCA libraries. We implement our techniques in the MINIME tool and generate synthetic benchmarks from PARSEC, Rodinia, and EEMBC MultibenchTM benchmarks on x86 and Power Architecture®platforms. We show that synthetic benchmarks are representative across a range of multicore machines with different architectures, while being on average 21× faster and 14× smaller than original benchmarks.

We present a framework that automatically generates system level synthetic benchmarks from traditional benchmarks. Synthetic benchmarks have similar performance behavior as the original benchmarks that they are generated from and they can run faster. Synthetics can also be used as proxies where original applications are not available in source form. In experiments we observe that not only are our system level benchmarks much smaller than the real benchmarks that they are generated from but they are also much faster. For example, when we generate synthetic benchmarks from the well-known multicore benchmark suite, PARSEC, our benchmarks have an average speedup of 149x over PARSEC benchmarks. We also observe that the performance behavior of synthetics have more than 85% similarity to the real benchmarks.

Evolutionary coupling is defined as the implicit relationship between two or more software artifacts that are frequently changed together. In this study we investigate the effect of evolutionary coupling on defect proneness of a large financial legacy software in an industrial software development environment. We collected historical data for 5 years from 3 different software repositories containing 150 thousand files on 274 modules. Our results indicate that there is a positive correlation between evolutionary coupling and defect measures. Furthermore, we built linear and logistic regression models by using evolutionary coupling measures in order to explain defects. Although regression analysis results show that evolutionary coupling measures can be useful to explain defects, especially for modules in which high correlation is detected, explanatory power decreases dramatically with the decreasing correlation.

Data races are one of the most common problems in concurrent programs. As SystemC standard allows nondeterministic scheduling of processes, this leads to data races. Hence, different executions of the same concurrent program may lead to unexpected results due to race conditions. We develop a hybrid dynamic data race detection algorithm for SystemC/TLM designs that adopts the well-studied dynamic race detection algorithms; lockset and happens-before. Experiments show that our solution has fewer false positives than lockset and fewer false negatives than happens-before algorithms. Our implementation uses dynamic binary instrumentation allowing us to work on designs for which source codes may not be available such as pre-compiled IPs.

Assertion-based methodology is gaining popularity in analog and mixed-signal (AMS) verification. Early AMS assertion languages are built on digital assertion languages. This results in limited native support to express most low-level aspects of AMS properties. We present three analog layer extensions to increase analog expressiveness in AMS assertion languages. We first describe the concept of haloes, an implicit way to handle tolerance values of analog signals in assertions. Then, booleanization of analog signals using dual-threshold is introduced to solve problems caused by fluctuations on signals. Finally, we integrate analog measurement operators into assertions. We validate our extensions using our prototype tool on a 10-bit two-stage pipelined analog-to-digital converter design.

Verification of embedded multicore applications is crucial as these applications are deployed in many safety critical systems. Verification task is complicated by concurrency inherent in such applications. We use mutation testing to obtain a quantitative verification coverage metric for mullticore applications developed using the new Multicore Communication API (MCAPI) standard. MCAPI is a lightweight API that targets heterogeneous multicore embedded systems. We developed a mutation coverage tool and performed several experiments on MCAPI applications. Our experiments show that mutation coverage is useful in measuring and improving the quality of the test suites and ultimately the quality of the multicore application.

This work presents a synthesis framework that generates a formally verifiable RTL from a high level language. We develop an estimation model for area, delay and power metrics of arithmetic components for Xilinx Spartan 3 FPGA family. Our estimation model works 300 times faster than Xilinx's toolchain with an average error of 6.57\% for delay and 3.76\% for area estimations. Our framework extracts CDFGs from ANSI-C, LRH(+) [1] and VHDL. CDFGs are verified using the symbolic model checker NuSMV [2] with temporal logic properties. This method guarantees detection of hardware redundancy and word-length mismatch related bugs by static code checking.

Recently, new technologies have emerged in industrial automation platforms. A rapid modeling and simulation environment is required to integrate these new technologies with existing devices and platforms to reduce the design effort and time to market. System-level modeling is a popular design technique that provides early simulation, verification, and architectural exploration. However, integration of real devices with system models is quite challenging due to synchronization and hard real-time constraints in industrial automation. SystemC is the most commonly used system-level language in hardware-software codesign. However, SystemC lacks interfaces for the integration of system (virtual) models with real (physical) devices. We introduce the hybrid channel concept to clearly define the integration interface. Hybrid channel incorporates both real-to-virtual and virtual-to-real communication functions by solving synchronization issues while satisfying the real-time constraints. We successfully demonstrated the usability of our framework in industrial systems that utilize BACNet and Ethernet. We also developed a mathematical model that correctly estimates the results of our experiments. To the best of our knowledge, this is the first framework and mathematical model for SystemC in industrial automation domain.

We describe verification and coverage methods for multicore software that uses message passing libraries for communication. Specifically, we provide techniques to improve reliability of software using the new industry standard MCAPI by the Multicore Association. We develop dynamic predictive verification techniques that allow us to find actual and potential errors in a multicore software. Some of these error types are deadlocks, race conditions, and violation of temporal assertions. We complement our verification techniques with a mutation-testing-based coverage metric. Coverage metrics enable measuring the quality of verification tests. We implemented our techniques in tools and validated them on several multicore programs that use the MCAPI standard. We implement our techniques in tools and experimentally show the effectiveness of our approach. We find errors that are not found using traditional dynamic verification techniques and we can potentially explore execution schedules different than the original program with our coverage tool. This is the first time such predictive verification and coverage metrics have been developed for MCAPI.

Correct concurrent System-on-Chips (SoCs) are very hard to design and reason about. In this work, we develop an automated framework complete with concurrency-oriented verification and coverage techniques for system-level designs. Our techniques are different from traditional simulation-based reliability techniques, since concurrency information is often lost in traditional techniques. We preserve concurrency information to obtain unique verification techniques that allow us to predict potential errors (formulated as transaction-level assertions) from error-free simulations. In order to do this, we exploit the inherent concurrency in the designs to generate and analyze novel partial-order simulation traces. Additionally, to evaluate the confidence on verification results and the gauge progress of verification, we develop novel mutation testing based on concurrent coverage metrics. Mutation testing is a fault insertion-based simulation technique that has been successfully applied in software testing. We present a comprehensive list of mutation operators for SystemC, similar to behavioral fault models, and show the effectiveness of these operators by relating them to actual bug patterns. We have successfully applied our verification and coverage techniques on industrial systems and demonstrated that current verification test suites need to be improved for concurrent designs, and we have found errors in systems that were tested previously.

Graphics Processing Units (GPUs) are gaining popularity for parallelization of general purpose applications. GPUs are massively parallel processors with huge performance in a small and readily available package. At the same time, the emergence of general purpose programming environments for GPUs such as CUDA shorten the learning curve of GPU programming. We present a GPU-based parallelization of logic simulation algorithm for electronic designs. Logic simulation is a crucial component of verification of electronic designs that allows one to check whether the design behaves according to the specifications. Verification of electronic designs consumes more than 60% of the overall design cycle. Any attempts to speedup the verification process (and logic simulation) results in great savings and shorter time-to-market. We develop a parallel cycle-based logic simulation algorithm that uses And Inverter Graphs (AIGs) as design representations and exploits the massively parallel GPU architecture. We demonstrate several orders of speedups on benchmarks using our system.

Concurrent interaction of multi-processor systems result in errors which are difficult to find. Traditional simulation-based verification techniques remove the concurrency information by arbitrary schedulings. We present a novel simulation-based technique for SystemC that preserves and exploits concurrency information. Our approach is unique in that we can detect potential errors in an observed execution, even if the error does not actually occur in that execution. We identify synchronization constructs in SystemC and develop predictive techniques for temporal assertion verification and deadlock detection. Our automated potential deadlock detection algorithm works on SystemC programs with semaphores, locks, wait and notify synchronizations and has less overhead compared with assertion verification. We patched SystemC kernel to implement our solution and obtained favorable results on industrial designs.

Concurrent and distributed systems, such as system-on-chips (SoCs), present an immense challenge for verification due to their complexity and inherent concurrency. Traditional approaches for eliminating errors in concurrent and distributed systems include formal methods and simulation. We present an approach toward combining formal methods and simulation in a technique called predicate detection (aka runtime verification), while avoiding the complexity of formal methods and the pitfalls of ad hoc simulation. Our technique enables efficient formal verification on execution traces of actual scalable systems. Traditional simulation methodologies are woefully inadequate in the presence of concurrency and subtle synchronization. The bug in the system may appear only when the ordering of concurrent events is different from the ordering in the simulation trace. We use a partial order trace model rather than the traditional total order trace model and we get the benefit of properly dealing with concurrent events and especially of detecting errors from analyzing successful total order traces. Surprisingly, checking properties, even on a finite partial order trace, is NP-complete in the size of the trace description (aka state-explosion problem). Our approach to ameliorating state explosion in partial order trace model uses two techniques: 1) slicing and 2) exploiting the structure of the property itself-by imposing restrictions-to evaluate its value efficiently for a given execution trace. Intuitively, the slice of a trace with respect to a property is a subtrace that contains all of the global states of the trace that satisfy the property such that it is computed efficiently (without traversing the state space) and represented concisely (without explicit representation of individual states). We present temporal slicing algorithms with respect to properties in temporal logic RCTL+. We show how to use the slicing algorithms for efficient predicate detection of design properties. We have developed a prototype system, partial order trace analyzer (POTA), which implements our algorithms. We verify several scalable and industrial protocols, including CORBA's general inter-ORB protocol, PCI-based system-on-chip, ISO's asynchronous transfer mode ring, cache coherence, and mutual exclusion. Our experimental results indicate that slicing can lead to exponential reduction over existing techniques, such as the ones in SPIN model checker, both in time and space

Given a distributed computation and a global predicate, predicate detection involves determining whether there exists at least one consistent cut (or global state) of the computation that satisfies the predicate. On the other hand, computation slicing is concerned with computing the smallest subcomputation (with the least number of consistent cuts) that contains all consistent cuts of the computation satisfying the predicate. In this paper, we investigate the relationship between predicate detection and computation slicing and show that the two problems are actually equivalent. Specifically, given an algorithm to detect a predicate b in a computation C, we derive an algorithm to compute the slice of C with respect to b. The time complexity of the (derived) slicing algorithm is O(n|E|T), where n is the number of processes, E is the set of events, and O(T) is the time complexity of the detection algorithm. We discuss how the "equivalence" result of this paper can be utilized to derive a faster algorithm for solving the general predicate detection problem in many cases. Slicing algorithms described in our earlier papers are all offline in nature. In this paper, we also present two online algorithms for computing the slice. The first algorithm can be used to compute the slice for a general predicate. Its amortized time complexity is O(n(c + n)T) per event, where c is the average concurrency in the computation and O(T) is the time complexity of the detection algorithm. The second algorithm can be used to compute the slice for a regular predicate. Its amortized time complexity is only O(n2) per event.

Summary form only given. Given a distributed computation and a global predicate, predicate detection involves determining whether there exists at least one consistent cut (or global state) of the computation that satisfies the predicate. On the other hand, computation slicing is concerned with computing the smallest sub-computation - with the least number of consistent cuts - that contains all consistent cuts of the computation satisfying the predicate. We investigate the relationship between predicate detection and computation slicing and show that the two problems are equivalent. Specifically, given an algorithm to detect a predicate b in a computation C, we derive an algorithm to compute the slice of C with respect to b. The time-complexity of the (derived) slicing algorithm is O(n|E|) times the time-complexity of the detection algorithm, where n is the number of processes and E is the set of events. We discuss how the "equivalence " result can be utilized to derive a faster algorithm for solving the general predicate detection problem. Slicing algorithms described in our earlier papers are all off-line in nature. We also give an online algorithm for computing the slice for a predicate that can be detected efficiently. The amortized time-complexity of the algorithm is O(n(c + n)) times the time-complexity of the detection algorithm, where c is the average concurrency in the computation.

Formal verification of systems-on-chips (SoCs) is an immense challenge to current industrial practice. Most existent formal verification techniques are extremely computation intensive and produce good results only when used on individual sub-components of SoCs. Without major modifications they are of little effectiveness in the SoC world. We attack the problem of SoC verification using an elegant abstraction mechanism, called computation slicing, and show that it enables effective temporal property verification on large designs. The technique targets a set of execution sequences, that is exhaustive with respect to an intended subset of system level properties, and automatically finds counter-example execution sequences in case of errors in the design. We have obtained exponential gains in reducing the global state space using a polynomial-time algorithm, and also applied a polynomial-time algorithm for checking global liveness and safety properties. We have successfully applied the technique to verify properties on two high level transaction based designs - the MSI cache coherence protocol and an admittedly academic SoC having a bus arbiter and a parameterizable number of devices connected to a PCI bus backbone.