Static analysis has profoundly improved software quality over the past decades, evolving from compiler-integrated optimizations and simple linting to sophisticated analyses for bug detection, security, and program understanding. In contrast, static analysis for hardware remains underexploited, resembling the early state of software analysis. Most existing hardware static analyses are confined to compiler optimizations and linting, lacking the sophistication needed to uncover complex design flaws. Furthermore, we observe that many hardware bugs reported in recent literature could have been identified by sophisticated static analyses that account for hardware-specific semantics and data flow; however, such bug detection analyses are absent today. To exploit the untapped potential of sophisticated hardware analysis, we present a series of bug detection analyses for Verilog, the predominant hardware description language (HDL). Moreover, these analyses are built upon our fundamental analyses that capture essential hardware-specific characteristics---such as bit-vector arithmetic, register synchronization, and digital component concurrency---and enable the examination of hardware data and control flows. Together, these analyses form a well-organized analysis suite with a modular design, in which diverse fundamental analyses combine to support bug detection, hardware understanding, and other potential clients. To implement these analyses, we further offer dedicated infrastructure, including a Verilog front end, an intermediate representation (IR) for analysis, and an analysis manager. To validate the utility of our analyses, we applied them to real-world hardware projects. Unlike software, real-world hardware projects tend to contain fewer but harder-to-detect bugs, as they typically undergo extensive simulation and rigorous verification to prevent the prohibitive costs of hardware defects. Despite this, our preliminary experimental results are highly promising: applying these proposed analyses to popular real-world Verilog projects (averaging 1.5K+ GitHub stars) uncovered nine previously unknown bugs, all confirmed by developers; moreover, we successfully identified a total of 18 bugs beyond the capabilities of existing static analyses for Verilog bug detection (i.e., linters). These results underscore the transformative potential of sophisticated static analysis in hardware design. Our analysis suite and infrastructure are also highly reusable: on average, each bug-detection client built on our analysis suite requires about 270 LoC, compared to 5,700 LoC when developed from scratch. By open-sourcing the entire system, involving substantial engineering effort (100K+ LoC), we aim to encourage further innovation and applications of sophisticated static analysis for hardware, hopefully fostering a similarly vibrant ecosystem that software analysis enjoys.

This paper presents our experience specifying and verifying the correctness of ZooKeeper, a complex and evolving distributed coordination system. We use TLA+ to model finegrained behaviors of ZooKeeper and use the TLC model checker to verify its correctness properties; we also check conformance between the model and code. The fundamental challenge is to balance the granularity of specifications and the scalability of model checking---fine-grained specifications lead to state-space explosion, while coarse-grained specifications introduce model-code gaps. To address this challenge, we write specifications with different granularities for composable modules, and compose them into mixed-grained specifications based on specific scenarios. For example, to verify code changes, we compose fine-grained specifications of changed modules and coarse-grained specifications that abstract away details of unchanged code with preserved interactions. We show that writing multi-grained specifications is a viable practice and can cope with model-code gaps without untenable state space, especially for evolving software where changes are typically local and incremental. We detected six severe bugs that violate five types of invariants and verified their code fixes; the fixes have been merged to ZooKeeper. We also improve the protocol design to make it easy to implement correctly.

Large language models (LLMs) can prove mathematical theorems formally by generating proof steps (\textit{a.k.a.} tactics) within a proof system. However, the space of possible tactics is vast and complex, while the available training data for formal proofs is limited, posing a significant challenge to LLM-based tactic generation. To address this, we introduce a neuro-symbolic tactic generator that synergizes the mathematical intuition learned by LLMs with domain-specific insights encoded by symbolic methods. The key aspect of this integration is identifying which parts of mathematical reasoning are best suited to LLMs and which to symbolic methods. While the high-level idea of neuro-symbolic integration is broadly applicable to various mathematical problems, in this paper, we focus specifically on Olympiad inequalities (Figure~1). We analyze how humans solve these problems and distill the techniques into two types of tactics: (1) scaling, handled by symbolic methods, and (2) rewriting, handled by LLMs. In addition, we combine symbolic tools with LLMs to prune and rank the proof goals for efficient proof search. We evaluate our framework on 161 challenging inequalities from multiple mathematics competitions, achieving state-of-the-art performance and significantly outperforming existing LLM and symbolic approaches without requiring additional training data.

Satisfiability Modulo Theories (SMT) solvers are crucial in many applications, yet their performance is often a bottleneck. This paper introduces SIRISMT, a novel framework that employs machine learning techniques for the automatic synthesis of efficient SMT-solving strategies. Specifically, SIRISMT targets at Z3 and consists of three key stages. First, given a set of training SMT formulas, SIRISMT simulates the solving process by leveraging reinforcement learning to guide its exploration within the strategy space. Next, SIRISMT refines the collected strategies by pruning redundant tactics and generating augmented strategies based on the subsequence structure of the learned strategies. These refined strategies are then fed back into the reinforcement learning model. Finally, the refined and optimized strategies are integrated into one strategy, which can be directly plugged into modern SMT solvers. Extensive evaluations show the superior performance of SIRISMT over the baseline methods. For example, compared to the default Z3, it solves 26.8% more formulas and achieves up to an 86.3% improvement in the Par-2 score on benchmark datasets. Additionally, we show that the synthesized strategy can improve the code coverage by up to 11.8% in a downstream symbolic execution benchmark.

The phase ordering problem, which aims to find suitable pass sequences for a given program on a target architecture, is critical in compiler optimization.One key challenge of this problem lies in the complex interplay among different passes within the vast optimization space of possible pass sequences.To better explore the interplay among passes, this paper proposes a new concept called booster pass chain (BPC), and presents a novel approach that identifies and leverages the BPCs to optimize the code size.Specifically, a BPC is a sequence of passes with positive interplay that, when presented as a whole, may exhibit significant optimization effects for certain programs.We then propose an iterative algorithm to extract BPCs, based on which we build a candidate set of pass sequences.For a given program, we also train a neural network to predict the suitable pass sequences from the candidate set.Experimental evaluations on 16 datasets containing 6,186 programs demonstrate the effectiveness of the proposed approach.That is, the candidate set achieves an average of 9.9% improvement compared to the LLVM -Oz flag in code size reduction, and selecting the top-3 pass sequences using the neural network predictor achieves 6.9% improvement.Our code and results are available at https://github.com/SoftWiser-group/EBPC4CPO.

Autonomous Driving Systems (ADS) are advancing rapidly due to progress in deep learning, yet critical challenges remain, particularly in the realm of safety verification.As safety-critical systems, ADS must undergo rigorous testing across diverse scenarios.Realworld data, while valuable, are inherently inflexible for interaction and scenario customization.In contrast, simulator-generated synthetic scenarios provide a platform that enables interaction, control, editability, and adaptability to specific needs.However, current simulation approaches are limited-either relying on costly, manually crafted, overly templated scenarios or generating unconditioned trivial behaviors based on learned distributions.In this work, we introduce LASER, an innovative framework that leverages large language models (LLMs) to conduct traffic simulations based on natural language inputs.The framework operates in two phases.First, it generates scripts from user-provided descriptions.Second, it executes these scripts by guiding autonomous agents within the CARLA simulator to perform tasks in real-time.This method effectively decomposes tasks, allocates controls, and integrates interactive elements to create dynamic and scalable simulations that align with user requirements.By using LASER, we overcome the rigid constraints of traditional simulation methods, enabling the creation of complex, diverse, flexible and on-demand driving scenarios.The approach significantly enhances the process of generating ADS training and testing data, addressing the scalability and diversity issues associated with previous simulation models.The code and all demos are available anonymously at https://njudeepengine.

Commit messages are valuable resources for describing why code changes are committed to repositories in version control systems (e.g., Git).They effectively help developers understand code changes and better perform software maintenance tasks.Unfortunately, developers often neglect to write high-quality commit messages in practice.Therefore, a growing body of work is proposed to generate commit messages automatically.These works all demonstrated that how to organize and represent code changes is vital in generating good commit messages, including the use of fine-grained graphs or embeddings to better represent code changes.In this study, we choose an alternative way to condense code changes before generation, i.e., proposing brief yet concise text templates consisting of the following three parts: (1) summarized code changes, (2) elicited comments, and (3) emphasized code identifiers.Specifically, we first condense code changes by using our proposed templates with the help of a heuristic-based tool named ChangeScribe, and then fine-tune CodeLlama-7B on the pairs of our proposed templates and corresponding commit messages.Our proposed templates better utilize pre-trained language models, while being naturally brief and readable to complement generated commit messages for developers.

Software testing plays a crucial role in software engineering, ensuring the reliability and correctness of evolving systems. Well-maintained test suites are essential for ensuring software quality. However, in modern development cycles that emphasize rapid feature iteration, the co-evolution of test suites often lags behind, leading to more appearance of obsolete tests. To this end, automated approaches for updating obsolete test code have been proposed, and recent approaches have achieved the state-of-the-art performance with the support of large language models (LLMs). This paper presents COMMITUP, a new approach that leverages LLMs to effectively automate method-level obsolete test code updates. COMMITUP mimics how humans solve the problem, first comprehending the code modifications, searching for similar examples to imitate, and finally performing the update. We evaluate COMMITUP on a curated dataset from real-world Java projects. The results demonstrate the superior performance of COMMITUP, achieving 96.4%, 94.4%, 93.1% success rates for generating compilable, runtime failure-free, and full coverage updates, respectively. We believe our study can provide new insight into LLM-based test code update. The dataset and code are available at https://github.com/SoftWiser-group/CommitUp.

Test-time scaling seeks to improve the reasoning performance of large language models (LLMs) by adding computational resources. A prevalent approach within the field is *sampling-based test-time scaling methods*, which enhance reasoning by generating multiple reasoning paths for a given input during inference. However, despite its practical success, the theoretical foundations remain underexplored. In this paper, we provide the first theoretical framework for analyzing sampling-based test-time scaling methods, grounded in the perspective of confidence estimation. Based on the framework, we analyze two dominant paradigms: self-consistency and perplexity, and reveal key limitations: self-consistency suffers from high estimation error while perplexity exhibits substantial modeling error and possible degradation of the estimation error convergence. To address these limitations, we introduce RPC, a hybrid method that leverages our theoretical insights through two key components: *Perplexity Consistency* and *Reasoning Pruning*. *Perplexity Consistency* combines the strengths of self-consistency and perplexity, boosting the convergence rate of estimation error from linear to exponential while preserving model error. *Reasoning Pruning* prevents degradation by eliminating low-probability reasoning paths. Both theoretical analysis and empirical results across seven benchmark datasets demonstrate that RPC has a strong potential for reducing reasoning error. Notably, RPC achieves reasoning performance comparable to self-consistency while not only enhancing confidence reliability but also reducing sampling costs by 50%. The code and resources are available at https://wnjxyk.github.io/RPC.

Database-backed applications form the backbone of modern software, yet their complexity poses significant challenges for static analysis. These applications involve intricate interactions among application code, diverse database frameworks such as JDBC, Hibernate, and Spring Data JPA, and languages like Java and SQL. In this paper, we introduce DBridge, the first pointer analysis specifically designed for Java database-backed applications, capable of statically constructing comprehensive Java-to-database value flows. DBridge unifies application code analysis, database access specification modeling, SQL analysis, and database abstraction within a single pointer analysis framework, capturing interactions across a wide range of database access APIs and frameworks. Additionally, we present DB-Micro, a new micro-benchmark suite with 824 test cases crafted to systematically evaluate static analysis for database-backed applications. Experiments on DB-Micro and large, complex, real-world applications demonstrate DBridge’s effectiveness, achieving high recall and precision in building Java-to-database value flows efficiently and outperforming state-of-the-art tools in SQL statement identification. To further validate DBridge’s utility, we develop three client analyses for security and program understanding. Evaluation on these real-world applications reveals 30 Stored XSS attack vulnerabilities and 3 horizontal broken access control vulnerabilities, all previously undiscovered and real, as well as a high detection rate in impact analysis for schema changes. By open-sourcing DBridge (14K LoC) and DB-Micro (22K LoC), we seek to help advance static analysis for modern database-backed applications in the future.

Implementation-level distributed system model checkers (DMCKs) have proven valuable in verifying the correctness of real distributed systems. However, they primarily focus on state space reduction, and often have a bottleneck on another crucial dimension: exploration speed. To scale DMCK, we introduce SandTable, a technique for lifting state-space exploration from the implementation level to the specification level, and confirming bugs at the implementation level. We made SandTable practical through a methodology consisting of four essential parts: (1) writing specifications that adhere to the implementation, (2) checking conformance to enhance specification quality and reduce false positives and false negatives, (3) exploring the state space with heuristics for effectiveness and efficiency, and (4) confirming bugs and verifying their fixes in the implementation.

Traceability allows stakeholders to extract and comprehend the trace links among software artifacts introduced across the software life cycle, to provide significant support for software engineering tasks. Despite its proven benefits, software traceability is challenging to recover and maintain manually. Hence, plenty of approaches for automated traceability have been proposed. Most rely on textual similarities among software artifacts, such as those based on Information Retrieval (IR). However, artifacts in different abstraction levels usually have different textual descriptions, which can greatly hinder the performance of IR-based approaches (e.g., a requirement in natural language may have a small textual similarity to a Java class). In this work, we leverage the consensual biterms and transitive relationships (i.e., inner- and outer-transitive links) based on intermediate artifacts to improve IR-based traceability recovery. We first extract and filter biterms from all source, intermediate, and target artifacts. We then use the consensual biterms from the intermediate artifacts to enrich the texts of both source and target artifacts, and finally deduce outer and inner-transitive links to adjust text similarities between source and target artifacts. We conducted a comprehensive empirical evaluation based on five systems widely used in other literature to show that our approach can outperform four state-of-the-art approaches in Average Precision over 15% and Mean Average Precision over 10% on average.

Data persistence is a critical foundation for Internet of Things (IoT), it provides the capability of data collection from IoT devices and pulls out these data by queries for applications to consume. In most cases, both the relationship between devices and the metrics on devices are required, so polyglot persistence systems consisting of graph databases and time series databases are deployed for data persistence. However, as the scale of IoT device network continues to grow, polyglot persistence finds it hard to achieve the need of real-time queries demanded by query-bound applications like artificial intelligence in IoT, which is where multi-model database be proficient in.

Treating programs as graphs and employing graph learning techniques to analyze them have been widely adopted in many software engineering tasks. A recent progress in this vein is to apply graph neural networks (GNNs) to model program graphs, which is built upon the homophily assumption, i.e., similar nodes tend to connect each other. However, this assumption is not always valid in program graphs, as various edges such as AST edges and token occurrence edges may connect dissimilar nodes with quite different properties. Such phenomenon is termed as the heterophily of program graphs. In this paper, we propose a new heterophily-aware graph convolutional network (HAGCN) to better handle the heterophilic program graphs. Specifically, we first introduce the subtraction operation into the message passing mechanism of GNNs, which allows HAGCN to push apart dissimilar nodes in the representation space. Then, HAGCN separately encodes each type of edges, and uses a global relation-aware attention mechanism to fuse messages from different edge types. Moreover, we also theoretically analyze the expressive power of HAGCN from the perspective of convolution filters and contrast the differences between HAGCN and other GNNs. Finally, we take type inference as an example to evaluate the effectiveness of the proposed approach. Experimental results demonstrate that HAGCN significantly outperforms the existing non-heterophilic competitors, as well as the existing state-of-the-art graph-based type inference approaches.

Traceability plays a vital role in facilitating various software development activities by establishing the traces between different types of artifacts (e.g., issues and commits in software repositories). Among the explorations for automated traceability recovery, the IR (Information Retrieval)-based approaches leverage textual similarity to measure the likelihood of traces between artifacts and show advantages in many scenarios. However, the globalization of software development has introduced new challenges, such as the possible multilingualism on the same concept (e.g., "[SEE PDF]" vs. "attribute") in the artifact texts, thus significantly hampering the performance of IR-based approaches. Existing research has shown that machine translation can help address the term inconsistency in bilingual projects. However, the translation can also bring in synonymous terms that are not consistent with those in the bilingual projects (e.g., another translation of "[SEE PDF]" as "property"). Therefore, we propose an enhancement strategy called AVIATE that exploits translation variants from different translators by utilizing the word pairs that appear simultaneously across the translation variants from different kinds artifacts (a.k.a. consensual biterms). We use these biterms to first enrich the artifact texts, and then to enhance the calculated IR values for improving IR-based trace-ability recovery for bilingual software projects. The experiments on 17 bilingual projects (involving English and 4 other languages) demonstrate that AVIATE significantly outperformed the IR-based approach with machine translation (the state-of-the-art in this field) with an average increase of 16.67 in Average Precision (31.43%) and 8.38 (11.22%) in Mean Average Precision, indicating its effectiveness in addressing the challenges of multilingual traceability recovery.

Loop invariant inference, a key component in program verification, is a challenging task due to the inherent undecidability and complex loop behaviors in practice. Recently, machine learning based techniques have demonstrated impressive performance in generating loop invariants automatically. However, these methods highly rely on the labeled training data, and are intrinsically random and uncertain, leading to unstable performance. In this paper, we investigate a synergy of large language models (LLMs) and bounded model checking (BMC) to address these issues. The key observation is that, although LLMs may not be able to return the correct loop invariant in one response, they usually can provide all individual predicates of the correct loop invariant in multiple responses. To this end, we propose a "query-filter-reassemble" strategy, namely, we first leverage the language generation power of LLMs to produce a set of candidate invariants, where training data is not needed. Then, we employ BMC to identify valid predicates from these candidate invariants, which are assembled to produce new candidate invariants and checked by off-the-shelf SMT solvers. The feedback is incorporated into the prompt for the next round of LLM querying. We expand the existing benchmark of 133 programs to 316 programs, providing a more comprehensive testing ground. Experimental results demonstrate that our approach significantly outperforms the state-of-the-art techniques, successfully generating 309 loop invariants out of 316 cases, whereas the existing baseline methods are only able to tackle 219 programs at best. The code is publicly available at https://github.com/SoftWiser-group/LaM4Inv.git.

Autoformalization, the task of automatically translating natural language descriptions into a formal language, poses a significant challenge across various domains, especially in mathematics. Recent advancements in large language models (LLMs) have unveiled their promising capabilities to formalize even competition-level math problems. However, we observe a considerable discrepancy between pass@1 and pass@k accuracies in LLM-generated formalizations. To address this gap, we introduce a novel framework that scores and selects the best result from k autoformalization candidates based on two complementary self-consistency methods: symbolic equivalence and semantic consistency. Elaborately, symbolic equivalence identifies the logical homogeneity among autoformalization candidates using automated theorem provers, and semantic consistency evaluates the preservation of the original meaning by informalizing the candidates and computing the similarity between the embeddings of the original and informalized texts. Our extensive experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy, achieving up to 0.22-1.35x relative improvements across various LLMs and baseline methods.

A critical question about Large Language Models (LLMs) is whether their apparent deficiency in mathematical reasoning is inherent, or merely a result of insufficient exposure to high-quality mathematical data. To explore this, we developed an automated method for generating high-quality, supervised mathematical datasets. The method carefully mutates existing math problems, ensuring both diversity and validity of the newly generated problems. This is achieved by a neuro-symbolic data generation framework combining the intuitive informalization strengths of LLMs, and the precise symbolic reasoning of math solvers along with projected Markov chain Monte Carlo sampling in the highly-irregular symbolic space. Empirical experiments demonstrate the high quality of data generated by the proposed method, and that the LLMs, specifically LLaMA-2 and Mistral, when realigned with the generated data, surpass their state-of-the-art counterparts.

Symbolic execution is a powerful program analysis technique. External environment construction and internal path explosion are two long-standing problems which may affect the effectiveness and performance of symbolic execution on complex programs. The intrinsic challenge is to achieve a sufficient understanding of the program context to construct a set of execution environments which can guide the selection of symbolic states. In this paper, we propose a novel program-context-guided symbolic execution framework LangSym based on program’s instruction/user manual. Leveraging the capabilities of natural language understanding and code generation in large language models (LLMs), LangSym can automatically extract the knowledge related to the functionality of the program, and generate adequate test cases and the corresponding environments as the prior knowledge for symbolic execution. We instantiate LangSym in KLEE, a widely adopted symbolic execution engine, to build a pipeline that could automatically leverage LLMs to boost the symbolic execution. We evaluate LangSym on almost all GNU Coreutils programs and considerable large-scale programs, showing that LangSym outperforms the existing strategies in KLEE with at least a 10% increase for line coverage.

Abstract Internet‐scale distributed systems often replicate data at multiple geographic locations to provide low latency and high availability, despite node and network failures. According to the CAP theorem, low latency and high availability can only be achieved at the cost of accepting weak consistency. The conflict‐free replicated data type (CRDT) is a framework that provides a principled approach to maintaining eventual consistency among data replicas. CRDTs have been notoriously difficult to design and implement correctly. Subtle deep bugs lie in the complex and tedious handling of all possible cases of conflicting data updates. We argue that the CRDT design should be formally specified and model checked, to uncover deep bugs which are beyond human reasoning. The implementation further needs to be systematically tested. On the one hand, the testing needs to inherit the exhaustive nature of the model checking and ensures the coverage of testing. On the other hand, the testing is expected to find coding errors which cannot be detected by design level verification. Toward the challenges above, we propose the model‐checking‐driven explorative testing ( MET ) framework. At the design level, MET uses TLA+ to specify and model check CRDT designs. At the implementation level, MET conducts model‐checking‐driven explorative testing, in the sense that the test cases are automatically generated from the model‐checking traces. The system execution is controlled to proceed deterministically, following the model‐checking trace. The explorative testing systematically controls and permutes all nondeterministic choices of message reorderings. We apply MET in our practical development of CRDTs. The bugs in both designs and implementations of CRDTs are found. As for bugs which can be found by traditional testing techniques, MET greatly reduces the cost of fixing the bugs. Moreover, MET can find subtle deep bugs which cannot be found by existing techniques at a reasonable cost. Based on our practical use of MET , we discuss how MET provides us with sufficient confidence in the correctness of our CRDT designs and implementations. Conflict‐free replicated data type (CRDT) is a framework that provides a principled approach to maintaining eventual consistency among data replicas in distributed systems. CRDTs have been notoriously difficult to design and implement correctly. We propose model‐checking‐driven explorative testing ( MET ) framework for dealing with such problem. We apply MET in our practical development of CRDTs. MET successfully finds subtle deep bugs and provides us with sufficient confidence in the correctness of our CRDT designs and implementations.

The reuse and integration of existing code is a common practice for efficient software development. Constantly updated Python interpreters and third-party packages introduce many challenges to Python runtime environment inference. Existing knowledge-based approaches have achieved good performance but still suffer from several limitations in the real world, especially from incomplete domain knowledge. In this paper, we propose ReadPyE, a realistic and adaptive approach to Python runtime environment inference. To leverage the rich code information, we present an automated approach to the construction and maintenance of our designed Python ecosystem knowledge graph (KG). Moreover, we are the first to handle real-world challenges such as complex dependency specifications and incomplete domain knowledge. Specifically, we define a naming similarity measure to match candidate packages for unknown modules and set priorities for multiple candidate packages. ReadPyE solves the optimization problems of candidate package selection and generates compatible runtime environments step by step based on the current Python environment. The inferred environments are iteratively validated and adjusted by matched exception templates in the validation logs. The evaluation results on three real-world datasets show the superior effectiveness and good efficiency of our ReadPyE compared to the existing knowledge-based approaches. ReadPyE solves the environment-related exceptions for 79.75% single-file code snippets, 93% Python projects, and 63.34% program pairs for code integration. We believe ReadPyE can help programmers reduce the time spent on inferring Python runtime environments and facilitate automated software configuration management.

Regression errors of Deep Neural Network (DNN) models refer to the case that predictions were correct by the old-version model but wrong by the new-version model. They frequently occur when upgrading DNN models in production systems, causing disproportionate user experience degradation. In this paper, we propose a lightweight regression error reduction approach with two goals: 1) requiring no model retraining and even data, and 2) not sacrificing the accuracy. The proposed approach is built upon the key insight rooted in the unmanaged model uncertainty, which is intrinsic to DNN models, but has not been thoroughly explored especially in the context of quality assurance of DNN models. Specifically, we propose a simple yet effective ensemble strategy that estimates and aligns the two models' uncertainty. We show that a Pareto improvement that reduces the regression errors without compromising the overall accuracy can be guaranteed in theory and largely achieved in practice. Comprehensive experiments with various representative models and datasets confirm that our approaches significantly outperform the state-of-the-art alternatives.

Machine learning methods have achieved great success in many software engineering tasks. However, as a data-driven paradigm, how would the data quality impact the effectiveness of these methods remains largely unexplored. In this paper, we explore this problem under the context of just-in-time obsolete comment detection. Specifically, we first conduct data cleaning on the existing benchmark dataset, and empirically observe that with only 0.22% label corrections and even 15.0% fewer data, the existing obsolete comment detection approaches can achieve up to 10.7% relative accuracy improvement. To further mitigate the data quality issues, we propose an adversarial learning framework to simultaneously estimate the data quality and make the final predictions. Experimental evaluations show that this adversarial learning framework can further improve the relative accuracy by up to 18.1% compared to the state-of-the-art method. Although our current results are from the obsolete comment detection problem, we believe that the proposed two-phase solution, which handles the data quality issues through both the data aspect and the algorithm aspect, is also generalizable and applicable to other machine learning based software engineering tasks.

Internet-scale distributed systems often rely on replication to achieve fault-tolerance and load distribution. To provide low latency and high availability, the systems are often required to accept updates on one replica immediately and then propagate the updates among replicas asynchronously. Conflict-free Replicated Data Type (CRDT) is a principled approach to addressing the challenge for these systems to resolve conflicts among concurrent updates. Although many CRDTs have been studied, little research has been done on Conflict-free Replicated Priority Queue (CRPQ), which is a collection of elements that focuses on maintaining element orderings based on their priority values, and can be used in many applications scenarios such as task scheduling and network routing. In this work, we discuss the design rationales of CRPQs and introduce two CRPQ designs: Add-Win CRPQ and Remove-Win CRPQ. The correctness of the designs is formally verified using TLA+. We also demonstrate the effectiveness of our designs by implementing them over Redis. Our evaluation shows that both CRPQs perform well in terms of data consistency and memory overhead.

API migration is an essential step for code migration between libraries or programming languages, and it is a challenging task as it requires detailed comprehension of both source and target APIs. The existing work either recommends mapped API names only and requires developers to select specific parameters and return value, or uses encoder-decoder models to directly “translate” the source API code into the target API code without considering the characteristics of APIs. In this paper, we propose a hybrid approach that combines small API mapping models with Large Language Models (LLMs). Specifically, the small API mapping model is employed to embed API semantics through their usages and declarations, enabling accurate inference of API mappings across different libraries and programming languages. The inferred mappings are subsequently used as part of the prompts to guide LLMs to generate the target API code corresponding to the source API code. Experimental evaluations demonstrate the effectiveness of our approach in comparison to existing approaches w.r.t. both cross-library and cross-language API migration.

Neuro-symbolic systems combine the abilities of neural perception and logical reasoning. However, end-to-end learning of neuro-symbolic systems is still an unsolved challenge. This paper proposes a natural framework that fuses neural network training, symbol grounding, and logical constraint synthesis into a coherent and efficient end-to-end learning process. The capability of this framework comes from the improved interactions between the neural and the symbolic parts of the system in both the training and inference stages. Technically, to bridge the gap between the continuous neural network and the discrete logical constraint, we introduce a difference-of-convex programming technique to relax the logical constraints while maintaining their precision. We also employ cardinality constraints as the language for logical constraint learning and incorporate a trust region method to avoid the degeneracy of logical constraint in learning. Both theoretical analyses and empirical evaluations substantiate the effectiveness of the proposed framework.

With the increasing need to apply modern software techniques to hardware design, Verilog, the most popular Hardware Description Language (HDL), plays an infrastructure role. However, Verilog has several semantic pitfalls that often confuse software and hardware developers. Although prior research on formal semantics for Verilog exists, it is not comprehensive and has not fully addressed these issues. In this work, we present a novel scheme inspired by previous work on defining core languages for software languages like JavaScript and Python. Specifically, we define the formal semantics of Verilog using a core language called λ V , which captures the essence of Verilog using as few language structures as possible. λ V not only covers the most complete set of language features to date, but also addresses the aforementioned pitfalls. We implemented λ V with about 27,000 lines of Java code, and comprehensively tested its totality and conformance with Verilog. As a reliable reference semantics, λ V can detect semantic bugs in real-world Verilog simulators and expose ambiguities in Verilog’s standard specification. Moreover, as a useful core language, λ V has the potential to facilitate the development of tools such as a state-space explorer and a concolic execution tool for Verilog.

Over the past decades, context sensitivity has been considered as one of the most effective ideas for improving the precision of pointer analysis for Java. Different from the extremely fast context-insensitivity approach, context sensitivity requires every program method to be analyzed under different contexts for separating the static abstractions of different dynamic instantiations of the method’s variables and heap objects, and thus reducing spurious object flows introduced by method calls. However, despite great precision benefits, as each method is equivalently cloned and analyzed under each context, context sensitivity brings heavy efficiency costs. Recently, numerous selective context-sensitive approaches have been put forth for scaling pointer analysis to large and complex Java programs by applying contexts only to the selected methods while analyzing the remaining ones context-insensitively; however, because the selective approaches do not fundamentally alter the primary methodology of context sensitivity (and do not thus remove its efficiency bottleneck), they produce much improved but still limited results. In this work, we present a fundamentally different approach called Cut-Shortcut for fast and precise pointer analysis for Java. Its insight is simple: the main effect of cloning methods under different contexts is to filter spurious object flows that have been merged inside a callee method; from the view of a typical pointer flow graph (PFG), such effect can be simulated by cutting off (Cut) the edges that introduce precision loss to certain pointers and adding Shortcut edges directly from source pointers to the target ones circumventing the method on PFG. As a result, we can achieve the effect of context sensitivity without contexts. We identify three general program patterns and develop algorithms based on them to safely cut off and add shortcut edges on PFG, formalize them and formally prove the soundness. To comprehensively validate Cut-Shortcut’s effectiveness, we implement two versions of Cut-Shortcut for two state-of-the-art pointer analysis frameworks for Java, one in Datalog for the declarative Doop and the other in Java for the imperative Tai-e, and we consider all the large and complex programs used in recent literatures that meet the experimental requirements. The evaluation results are extremely promising: Cut-Shortcut is even able to run faster than context insensitivity for most evaluated programs while obtaining high precision that is comparable to context sensitivity (if scalable) in both frameworks. This is for the first time that we have been able to achieve such a good efficiency and precision trade-off for those hard-to-analyze programs, and we hope Cut-Shortcut could offer new perspectives for developing more effective pointer analysis for Java in the future.

Greetings and welcome to the third issue of IEEE TRANSACTIONS ON COMPUTATIONAL SOCIAL SYSTEMS (TCSS) for 2023. The authors are delighted to share some exciting news with our esteemed readership.

Software information sites (e.g., Jira, Stack Overflow) are now wide-ly used in software development. These online platforms for collaborative development preserve a large amount of Software Engineering (SE) texts. These texts enable researchers to detect developers’ attitudes toward their daily development by analyzing the sentiments expressed in the texts. Unfortunately, recent works reported that neither off-the-shelf tools nor SE-specified tools for sentiment analysis on SE texts can provide satisfying and reliable results. In this paper, we propose to incorporate pre-trained transformer models into the sentence-classification oriented deep learning framework named TextCNN to better capture the unique expression of sentiments in SE texts. Specifically, we introduce an optimized BERT model named RoBERTa as the word embedding layer of TextCNN, along with additional residual connections between RoBERTa and TextCNN for better cooperation in our training framework. An empirical evaluation based on four datasets from different software information sites shows that our training framework can achieve overall better accuracy and generalizability than the four baselines.

Traceability approves trace links among software artifacts based on whether two artifacts are related by system functionalities. The traces are valuable for software development, but are difficult to obtain manually. To cope with the costly and fallible manual recovery, automated approaches are proposed to recover traces through textual similarities among software artifacts, such as those based on Information Retrieval (IR). However, the low quality & quantity of artifact texts negatively impact the calculated IR values, thus greatly hindering the performance of IR-based approaches. In this study, we propose to extract co-occurred word pairs from the text structures of both requirements and code (i.e., consensual biterms) to improve IR-based traceability recovery. We first collect a set of biterms based on the part-of-speech of requirement texts, and then filter them through the code texts. We then use these consensual biterms to both enrich the input corpus for IR techniques and enhance the calculations of IR values. A nine-system-based evaluation shows that in general, when solely used to enhance IR techniques, our approach can outperform pure IR-based approaches and another baseline by 21.9% & 21.8% in AP, and 9.3% & 7.2% in MAP, respectively. Moreover, when used to collaborate with another enhancing strategy from different perspectives, it can outperform this baseline by 5.9% in AP and 4.8% in MAP.

Effective quality assurance methods for autonomous driving systems ADS have attracted growing interests recently. In this paper, we report a new testing platform ADEPT, aiming to provide practically realistic and comprehensive testing facilities for DNN-based ADS. ADEPT is based on the virtual simulator CARLA and provides numerous testing facilities such as scene construction, ADS importation, test execution and recording, etc. In particular, ADEPT features two distinguished test scenario generation strategies designed for autonomous driving. First, we make use of real-life accident reports from which we leverage natural language processing to fabricate abundant driving scenarios. Second, we synthesize physically-robust adversarial attacks by taking the feedback of ADS into consideration and thus are able to generate closed-loop test scenarios. The experiments confirm the efficacy of the platform.

Learning fair representations is an essential task to reduce bias in data-oriented decision making. It protects minority subgroups by requiring the learned representations to be independent of sensitive attributes. To achieve independence, the vast majority of the existing work primarily relaxes it to the minimization of the mutual information between sensitive attributes and learned representations. However, direct computation of mutual information is computationally intractable, and various upper bounds currently used either are still intractable or contradict the utility of the learned representations. In this paper, we introduce distance covariance as a new dependence measure into fair representation learning. By observing that sensitive attributes (e.g., gender, race, and age group) are typically categorical, the distance covariance can be converted to a tractable penalty term without contradicting the utility desideratum. Based on the tractable penalty, we propose FairDisCo, a variational method to learn fair representations. Experiments demonstrate that FairDisCo outperforms existing competitors for fair representation learning.

Consensus protocols are widely used in building reliable distributed software systems and their correctness is of vital importance. TLA+ is a lightweight formal specification language which enables precise specification of system design and exhaustive checking of the design without any human effort. The features of TLA+ make it widely used in the specification and model checking of consensus protocols, both in academia and in industry. However, the application of TLA+ is limited by the state explosion problem in model checking. Though compositional model checking is essential to tame the state explosion problem, existing compositional checking techniques do not sufficiently consider the characteristics of TLA+. In this work, we propose the Interaction-Preserving Abstraction (IPA) framework, which leverages the features of TLA+ and enables practical and efficient compositional model checking of consensus protocols specified in TLA+. In the IPA framework, system specification is partitioned into multiple modules, and each module is divided into the internal part and the interaction part. The basic idea of the interaction-preserving abstraction is to omit the internal part of each module, such that another module cannot distinguish whether it is interacting with the original module or the coarsened abstract one. We apply the IPA framework to the compositional checking of the TLA+ specifications of two consensus protocols Raft and ParallelRaft. Raft is a consensus protocol which was originally developed in academia and then widely used in industry. ParallelRaft is the replication protocol in PolarFS, the distributed file system for the commercial database Alibaba PolarDB. We demonstrate that the IPA framework is easy to use in realistic scenarios and at the same time significantly reduces the model checking cost.

Developers often need to use appropriate APIs to program efficiently, but it is usually a difficult task to identify the exact one they need from a vast list of candidates. To ease the burden, a multitude of API recommendation approaches have been proposed. However, most of the currently available API recommenders do not support the effective integration of user feedback into the recommendation loop. In this paper, we propose a framework, BRAID (BoostingRecommendAtion withImplicit FeeDback), which leverages learning-to-rank and active learning techniques to boost recommendation performance. By exploiting user feedback information, we train a learning-to-rank model to re-rank the recommendation results. In addition, we speed up the feedback learning process with active learning. Existing query-based API recommendation approaches can be plugged into BRAID. We select three state-of-the-art API recommendation approaches as baselines to demonstrate the performance enhancement of BRAID measured by Hit@k (Top-k), MAP, and MRR. Empirical experiments show that, with acceptable overheads, the recommendation performance improves steadily and substantially with the increasing percentage of feedback data, comparing with the baselines.

There is an increasing demand for evolving software systems to deliver continuous services of no restart. Dynamic software update (DSU) aims to achieve this goal by patching the system state on the fly but is currently hindered from practice due to non-trivial cross-version object state transformations. This paper revisits this problem through an in-depth empirical study of over 190 class changes from Tomcat 8. The study produced an important finding that most non-trivial object state transformers can be constructed by reassembling existing old/new version code snippets. This paper presents a domain-specific language and an efficient algorithm for synthesizing non-trivial object transformers over code reuse. We experimentally evaluated our tool implementation PASTA with real-world software systems, reporting PASTA's effectiveness in succeeding in 7.5X non-trivial object transformation tasks compared with the best existing DSU techniques.

Sentiment analysis on software engineering (SE) texts has been widely used in the SE research, such as evaluating app reviews or analyzing developers' sentiments in commit messages. To better support the use of automated sentiment analysis for SE tasks, researchers built an SE-domain-specified sentiment dictionary to further improve the accuracy of the results. Unfortunately, recent work reported that current mainstream tools for sentiment analysis still cannot provide reliable results when analyzing the sentiments in SE texts. We suggest that the reason for this situation is because the way of expressing sentiments in SE texts is largely different from the way in social network or movie comments. In this paper, we propose to improve sentiment analysis in SE texts by using sentence structures, a different perspective from building a domain dictionary. Specifically, we use sentence structures to first identify whether the author is expressing her sentiment in a given clause of an SE text, and to further adjust the calculation of sentiments which are confirmed in the clause. An empirical evaluation based on four different datasets shows that our approach can outperform two dictionary-based baseline approaches, and is more generalizable compared to a learning-based baseline approach.

Control-based approaches to self-adaptive software-intensive systems (SASs) are hailed for their optimal performance and theoretical guarantees on the reliability of adaptation behavior. However, in practice the guarantees are often threatened by model deviations occurred at runtime. In this paper, we propose a Model-guided Deviation Detector (MoD2) for timely and accurate detection of model deviations. To ensure reliability, a SAS can switch a control-based optimal controller for a mandatory controller once an unsafe model deviation is detected. MoD2 achieves both high timeliness and high accuracy through a deliberate fusion of parameter deviation estimation, uncertainty compensation, and safe region quantification. Empirical evaluation with three exemplar systems validated the efficacy of MoD2 (93.3% shorter detection delay, 39.4% lower FN rate, and 25.2% lower FP rate), as well as the benefits of the adaptation-switching mechanism (abnormal rate dropped by 29.2%).

Traditional context-sensitive pointer analysis is hard to scale for large and complex Java programs. To address this issue, a series of selective context-sensitivity approaches have been proposed and exhibit promising results. In this work, we move one step further towards producing highly-precise pointer analyses for hard-to-analyze Java programs by presenting the Unity-Relay framework, which takes selective context sensitivity to the next level. Briefly, Unity-Relay is a one-two punch: given a set of different selective context-sensitivity approaches, say S = S1, . . . , Sn, Unity-Relay first provides a mechanism (called Unity)to combine and maximize the precision of all components of S. When Unity fails to scale, Unity-Relay offers a scheme (called Relay) to pass and accumulate the precision from one approach Si in S to the next, Si+1, leading to an analysis that is more precise than all approaches in S. As a proof-of-concept, we instantiate Unity-Relay into a tool called Baton and extensively evaluate it on a set of hard-to-analyze Java programs, using general precision metrics and popular clients. Compared with the state of the art, Baton achieves the best precision for all metrics and clients for all evaluated programs. The difference in precision is often dramatic — up to 71% of alias pairs reported by previously-best algorithms are found to be spurious and eliminated.

In the era of Internet and big data, contemporary workflows become increasingly large in scale and complex in structure, introducing greater challenges for workflow modeling. Workflows are not with maximized concurrency and block-structuredness in terms of control flow, though languages supporting block-structuredness (e.g., BPEL) are employed. Existing workflow refactoring approaches mostly focus on maximizing concurrency according to dependences between activities, but do not consider the block-structuredness of the refactored workflow. It is easier to comprehend and analyze a workflow that is block-structured and to transform it into BPEL-like processes. In this paper, we aim at maximizing both concurrency and block-structuredness. Nevertheless, not all workflows can be refactored with a block-structured representation, and it is intractable to make sure that the refactored workflows are as block-structured as possible. We first define a well-formed dependence pattern of activities. The control flow among the activities in this pattern can be represented in block-structured forms with maximized concurrency. Then, we propose a greedy heuristics-based graph reduction approach to recursively find such patterns. In this way, the resulting workflow is with maximized concurrency and its block-structuredness approximates optimality. We show the effectiveness and efficiency of our approach with real-world scientific workflows.

Data-aware executable processes are an effective and efficient means to build service-oriented applications. However, since the services involved are loosely-coupled and self-managed, the process is flexible by nature and it executions may deviate from their specifications. In contrast to existing approaches that focus on control flow deviations, we leverage activity dependences for data-aware process conformance checking. To analyze the conformance of a process instance to its process definition, we seek a process reference trace “best-fitting” the instance trace such that the conformance degree of the input trace to the process equals the consistency degree of both traces. We measure the consistency between two traces based on their activity dependences. Since finding the reference trace is NP-hard, we resort to heuristics based on process decomposition and trace replaying to determine the trace. Our approach can identify conformance decrease caused by activity dependence deviations, thus, complementing existing approaches. We implement our approach as a ProM plugin. Experimental results on 102 real-world WS-BPEL processes and 26,880 synthetic input traces confirm the effectiveness and efficiency of our approach.

Many applications use contexts to understand their environments and make adaptation. However, contexts are often inaccurate or even conflicting with each other (a.k.a. context inconsistency). To prevent applications from behaving abnormally or even failing, one promising approach is to deploy constraint checking to detect context inconsistencies. A variety of constraint checking techniques have been proposed, based on different incremental or parallel mechanisms for the efficiency. They are commonly deployed with the strategy that schedules constraint checking immediately upon context changes. This assures no missed inconsistency, but also limits the detection efficiency. One may break the limit by grouping context changes for checking together, but this can cause severe inconsistency missing problem (up to 79.2 percent). In this article, we propose a novel strategy GEAS to isolate latent interferences among context changes and schedule constraint checking with adaptive group sizes. This makes GEAS not only improve the detection efficiency, but also assure no missed inconsistency with theoretical guarantee. We experimentally evaluated GEAS with large-volume real-world context data. The results show that GEAS achieved significant efficiency gains for context inconsistency detection by 38.8-566.7 percent (or 1.4x-6.7x). When enhanced with an extended change-cancellation optimization, the gains were up to 2,755.9 percent (or 28.6x).

Generating high-quality system call sequences is not only important to testing file system implementations, but also challenging due to the astronomically large input space. This paper introduces a new approach to the workload generation problem by building layered models and abstract workloads refinement. This approach is instantiated as a three-layer file system model for file system workload generation. In a short-period experiment run, sequential workloads (system call sequences) manifested over a thousand crashes in mainline Linux Kernel file systems, with 12 previously unknown bugs being reported. We also provide evidence that such workloads benefit other domain-specific testing techniques including crash consistency testing and concurrency testing.

Deep learning (DL) applications are becoming increasingly popular. Their reliabilities largely depend on the performance of DL models integrated in these applications as a central classifying module. Traditional techniques need to retrain the models or rebuild and redeploy the applications for coping with unexpected conditions beyond the models' handling capabilities. In this paper, we take a fault tolerance approach, Dissector, to distinguishing those inputs that represent unexpected conditions (beyond-inputs) from normal inputs that are still within the models' handling capabilities (within-inputs), thus keeping the applications still function with expected reliabilities. The key insight of Dissector is that a DL model should interpret a within-input with increasing confidence, while a beyond-input would probably cause confused guesses in the prediction process. Dissector works in an application-specific way, adaptive to DL models used in applications, and extremely efficiently, scalable to large-size datasets from complex scenarios. The experimental evaluation shows that Dissector outperformed state-of-the-art techniques in the effectiveness (AUC: avg. 0.8935 and up to 0.9894) and efficiency (runtime overhead: only 3.3--5.8 milliseconds). Besides, it also exhibited encouraging usefulness in defensing against adversarial inputs (AUC: avg. 0.9983) and improving a DL model's actual accuracy in use (up to 16% for CIFAR-100 and 20% for ImageNet).

Android apps demand high-quality test inputs, whose generation remains an open challenge. Existing techniques fall short on exploring complex app functionalities reachable only by a long, meaningful, and effective test input. Observing that such test inputs can usually be decomposed into relatively independent short use cases, this paper presents ComboDroid, a fundamentally different Android app testing framework. ComboDroid obtains use cases for manifesting a specific app functionality (either manually provided or automatically extracted), and systematically enumerates the combinations of use cases, yielding high-quality test inputs.

Self-adaptation is a promising approach to enable software systems to address the challenge of uncertainty. Different from traditional reactive adaptation mechanisms that focus on the system’s current environment state only, proactive adaptation mechanisms predict the potential environmental changes and make better adaptation plan accordingly. Proactive Latency-aware Adaptation (PLA for shot) and Control-based Requirements-oriented Adaptation (CobRA for short) are two representative approaches to build proactive self-adaptation mechanisms. Despite their different design and implementation details, PLA and CobRA are reported to have a very similar performance in supporting self-adaptation. In this paper, we conduct an in-depth comparison between these two approaches, trying to explain their effectiveness. We separate a proactive self-adaptation mechanism into three modules, namely system modelling, environment predicting, and uncertainty filtering. We identify the design choices of PLA and CobRA approaches, in terms of these three modules. We performed an ablation study on the three modules of PLA and compared their performance with CobRA. Our study reveals the very important role of uncertainty filtering in supporting self-adaptation, as well as the huge impact of a fluctuant environment on a self-adaptation mechanism. Based on this observation, we briefly discuss a conceptual self-adaptation mechanism, MAPE-U (monitoring, analyzing, planning, executing with uncertainty).

Dynamic software update (DSU) can patch programs without stopping them. The updating process includes replacing changed code, transforming stale objects with object transformers, and resuming the execution of the updated program. However, flawed object transformers currently hinder DSU from the wide application, since they may introduce the inconsistencies between the transformed objects with expected new ones, that are created by the new program executing from scratch with the same inputs. To detect such inconsistencies, our approach first utilizes fuzzing testing to explore test inputs, then executes them over the old and new versions of a program within our specially designed parallel executor. Any inconsistency and the corresponding test will be issued. The evaluation over default transformer in 50 updates (14 of them have the inconsistency problem) showed that our approach discovered inconsistency in 16 updates, with 5 false positives and 3 false negatives. We also optimized the seed selection strategy in fuzzing process and improved the efficiency by 25.0%.

Trained DNN models are increasingly adopted as integral parts of software systems, but they often perform deficiently in the field. A particularly damaging problem is that DNN models often give false predictions with high confidence, due to the unavoidable slight divergences between operation data and training data. To minimize the loss caused by inaccurate confidence, operational calibration, i.e., calibrating the confidence function of a DNN classifier against its operation domain, becomes a necessary debugging step in the engineering of the whole system.

Software systems assisted with deep neural networks (DNNs) are gaining increasing popularities. However, one outstanding problem is to judge whether a given application scenario suits a DNN model, whose answer highly affects its concerned system's performance. Existing work indirectly addressed this problem by seeking for higher test coverage or generating adversarial inputs. One pioneering work is SynEva, which exactly addressed this problem by synthesizing mirror programs for scenario suitableness evaluation of general machine learning programs, but fell short in supporting DNN models. In this paper, we propose VISION to eValuatIng Scenario suItableness fOr DNN models, specially catered for DNN characteristics. We conducted experiments on a real-world self-driving dataset Udacity, and the results show that VISION was effective in evaluating scenario suitableness for DNN models with an accuracy of 75.6-89.0% as compared to that of SynEva, 50.0-81.8%. We also explored different meta-models in VISION, and found out that the decision tree logic learner meta-model could be the best one for balancing VISION's effectiveness and efficiency.

Widely used commercial Android applications (apps) turn to be of complex GUIs and hundreds of activities. Testing this kind of apps is challenging. Existing automated testing tools cannot complete the testing of these complex apps in a short time. However, scaling these tools for parallelism to accelerate the testing is not straightforward. In this paper, we borrow the basic concepts from parallel computing, and introduce the parallel testing platform ParaAim. ParaAim partitions an app testing job into a set of tasks at the activity granularity. Starting from a specific entrance activity, ParaAim explores the UI-states of the app and each newly discovered activity spawns a new task. ParaAim dispatches the new task to an idle device and sets it up to the entrance by replaying an event sequence. In this manner, the independent parts of the app are explored simultaneously. We focus on the efficiency of this parallel GUI exploration schema. ParaAim assigns the tasks that have more possibility to find new activities with high priority for better performance. Event sequence minimization is also studied to reduce the time cost of replay, and we design widget fuzzy match technique to handle the state inconsistency issue. We evaluated ParaAim with 20 popular commercial apps on different settings of Android device cluster. The results show that ParaAim scales well and evidently increases the average speed of exploration to nearly 2 times with two devices, and 3 times with four devices, than a single device.

This paper introduces a new, fully automated modelbased approach for effective testing of Android apps. Different from existing model-based approaches that guide testing with a static GUI model (i.e., the model does not evolve its abstraction during testing, and is thus often imprecise), our approach dynamically optimizes the model by leveraging the runtime information during testing. This capability of model evolution significantly improves model precision, and thus dramatically enhances the testing effectiveness compared to existing approaches, which our evaluation confirms.We have realized our technique in a practical tool, APE. On 15 large, widely-used apps from the Google Play Store, APE outperforms the state-of-the-art Android GUI testing tools in terms of both testing coverage and the number of detected unique crashes. To further demonstrate APE's effectiveness and usability, we conduct another evaluation of APE on 1,316 popular apps, where it found 537 unique crashes. Out of the 38 reported crashes, 13 have been fixed and 5 have been confirmed.

A typical generate-and-validate automatic program repair (APR) tool needs to repeatedly run the same test suite to validate each generated patch. This procedure is expensive when the number of patches is huge. Additionally, to scale to large programs, a program repair tool has to consider a small patch space in practice and thus may sacrifice the capability to find potential correct repairs. In this work, we propose to speed up automatic program repair to mitigate the above issues. One the one hand, we found that restarting processes to load patched code consumes the majority of total validation time. This problem is even severe when the program is running in a managed runtime such as Java virtual machine (JVM). On the other hand, dynamic software updating (DSU) can load and execute new code without restarting. To this end, we propose to use DSU techniques to speed up automatic program repair and present an empirical study in this paper. Within our study, DSU can bring up to 66.3 times speedup in comparison with the traditional restart approach. However, DSU may not be able to handle all patches and can also incur unknown side effects that lead to inconsistent validation results. We then further study the feasibility and consistency of applying DSU to speed up APR. Our results show that 1) less than 1% patches cannot be dynamically updated using the builtin DSU ability of JVM, and 2) DSU based validation leads to potentially harmful inconsistency in only 16 of 1,897,518 patches.

Deep neural networks (DNNs) have achieved impressive performance in many difficult tasks. However, DNN models are essentially uninterpretable to humans, and unfortunately prone to adversarial attacks, which hinders their adoption in security and safety-critical scenarios. The robustness of a DNN model, which measures its stableness against adversarial attacks, becomes an important topic in both the machine learning and the software engineering communities. Analytical evaluation of DNN robustness is difficult due to the high-dimensionality of inputs, the huge amount of parameters, and the nonlinear network structure. In practice, the degree of robustness of DNNs is empirically approximated with adversarial searching, which is computationally expensive and cannot be applied in resource constrained settings such as embedded computing. In this paper, we propose to predict the robustness of a DNN model for each input with another DNN model, which takes the output of neurons of the former model as input. We train a regression model to encode the connections between output of the penultimate layer of a DNN model and its robustness. With this trained model, the robustness for an input can be predicted instantaneously. Experiments with MNIST and CIFAR10 datasets and LeNet, VGG and ResNet DNN models were conducted to evaluate the efficacy of the proposed approach. The results indicated that our approach achieved 0.05-0.21 mean absolute errors and significantly outperformed confidence and surprise adequacy-based approaches.

Traceability recovery allows developers to extract and comprehend the trace links among software artifacts (e.g., requirements and code). These trace links can provide important support to software maintenance and evolution tasks. Information Retrieval (IR) is now widely accepted as the key technique of semi-automatic tools to recover candidate trace links based on textual similarities among artifacts. However, the vocabulary mismatch problem between different artifacts hinders the performance of these IR-based approaches. Thus, a growing body of enhancing strategies were proposed based on user feedback. They allow to adjust the textual similarities of candidate links after users accept or reject part of these links. Recently, several approaches successfully used this strategy to improve the performance of IR-based traceability recovery. However, these approaches require a large amount of user feedback, which is infeasible in practice. In this paper, we propose to improve IR-based traceability recovery by introducing only a small amount of user feedback into the closeness analysis on call and data dependencies in code. Specifically, our approach iteratively asks users to verify a chosen candidate link based on the quantified functional similarity for each code dependency (called closeness) and the generated IR values. The verified link is then used as the input to re-rank the unverified candidate links. An empirical evaluation based on five real-world systems shows that our approach can outperform four baseline approaches by using only a small amount of user feedback.

Spreadsheets are widely used but subject to various defects. In this paper, we present SGuard to effectively detect spreadsheet defects. SGuard learns spreadsheet features to cluster cells with similar computational semantics, and then refines these clusters to recognize anomalous cells as defects. SGuard well balances the trade-off between the precision (87.8%) and recall rate (71.9%) in the defect detection, and achieves an F-measure of 0.79, exceeding existing spreadsheet defect detection techniques. We introduce the SGuard implementation and its usage by a video presentation (https://youtu.be/gNPmMvQVf5Q), and provide its public download repository (https://github.com/sheetguard/sguard).

Spreadsheets are widely used, but subject to various defects and severe consequences due to poor maintenance by end users. Existing spreadsheet defect detection techniques fall short of effectiveness, either due to limited scopes or relying on rigid patterns. In this paper, we discuss and improve one state-of-the-art technique, CUSTODES, which uses cell clustering and anomaly detection to extend its scope and make its patterns adaptive to varying spreadsheet styles, but is prone to fragile clustering when involving irrelevant cells, leading to a largely reduced detection precision. We present WARDER to refine CUSTODES's cell clustering based on validity properties, and experimental results show that WARDER improves the precision by 20.7% on average or reach 100% for 79.8% worksheets on cell clustering, which contributes to a precision improvement of 23.1% for defect detection. WARDER also exhibits satisfactory results, against other spreadsheet defect detection techniques, and on another large-scale spreadsheet corpus VEnron2.

With the increasing adoption of Deep Neural Network (DNN) models as integral parts of software systems, efficient operational testing of DNNs is much in demand to ensure these models' actual performance in field conditions. A challenge is that the testing often needs to produce precise results with a very limited budget for labeling data collected in field.

Mobile applications (apps for short) often need to display images. However, inefficient image displaying (IID) issues are pervasive in mobile apps, and can severely impact app performance and user experience. This paper presents an empirical study of 162 real-world IID issues collected from 243 popular open-source Android apps, validating the presence and severity of IID issues, and then sheds light on these issues' characteristics to support future research on effective issue detection. Based on the findings of this study, we developed a static IID issue detection tool TAPIR and evaluated it with real-world Android apps. The experimental evaluations show encouraging results: TAPIR detected 43 previously-unknown IID issues in the latest version of the 243 apps, 16 of which have been confirmed by respective developers and 13 have been fixed.

Likely more than many other software artifacts, business processes constantly evolve to adapt to ever changing application requirements. To enable dynamic process evolution, where changes are applied to in-flight processes, running process instances have to be migrated. On the one hand, as many instances as possible should be migrated to the changed process. On the other hand, the validity to migrate an instance should be guaranteed to avoid introducing dynamic change bugs after migration. As our theoretical results show, when the state of variables is taken into account, migration validity of data-aware process instances is undecidable. Based on the trace of an instance, existing approaches leverage trace replaying to check migration validity. However, they err on the side of caution, not identifying many instances as potentially safe to migrate. We present a more relaxed migration validity checking approach based on the dependence graph of a trace. We evaluate effectiveness and efficiency of our approach experimentally showing that it allows for more instances to safely migrate than for existing approaches and that it scales in the number of instances checked.

Volumes of studies on resource scheduling are proposed to improve the efficiency of computing clusters. As users usually overestimate the resource requirements for their jobs, further, most schedulers ignore the dynamic variation of jobs' runtime resource usage, the utilization of real-world clusters is significantly limited. In this paper, we argue that resource oversubscription, which allocates more resources than the physical capacity, is a necessary complement to existing systems. To alleviate resource contention, we augment oversubscription with lightweight prediction and dynamic CPU throttling. We implemented our approach called Datom, which is an extension module of the Apache Mesos cluster manager. We evaluated Datom with real-world video transcoding workloads and simulations with Google cluster trace. The results show that comparing to original Mesos, Datom increased CPU utilization, memory utilization and overall task throughput by up to 22%, 23%, 20% respectively, and shortened jobs' complete time by up to 20%, at the expenses of moderate penalty on job execution.

Assertions are intensively used to facilitate correctness reasoning and error detection in daily programming. However, composing assertions for mobile robotic programs can be painfully inconvenient, because classic Hoare logic lacks the expressing power on spatial knowledge, which is crucial when robots interact with their physical environments. The problem is especially evident for Behavior-Based Robotics (BBR) where the world is not explicitly represented with program variables. In this paper, we propose to incorporate spatial reasoning capability in the assertion framework of Hoare logic. The proposed framework features a two-dimensional region calculus and additional axioms for robot movements. The calculus makes the world representation and the specification of mobile robotic program natural and intuitive, and the axioms enable the reasoning about program correctness. We illustrate the use of the framework with a typical behavior-based robotic program. In addition, we present a runtime error detection and recovery mechanism for BBR programs based on the assertion framework. Preliminary experiments with NAO robots demonstrate the effectiveness.

Dynamic software updating (DSU) is a technique to upgrade a running software system on the fly without stopping the system. During updating, the runtime state of the modified components of the system needs to be properly transformed into a new state, so that the modified components can still correctly interact with the rest of the system. However, the transformation is non-trivial to realize due to the gap between the low-level implementations of two versions of a program. This paper presents AOTES, a novel approach to automating object transformations for dynamic updating of Java programs. AOTES bridges the gap by abstracting the old state of an object to a history of method invocations, and re-invoking the new version of all methods in the history to get the desired new state. AOTES requires no instrumentation to record any data and thus has no overhead during normal execution. We propose and implement a novel technique that can synthesize an equivalent history of method invocations based on the current object state only. We evaluated AOTES on software updates taken from Apache Commons Collections, Tomcat, FTP Server and SSHD Server. Experimental results show that AOTES successfully handled 51 of 61 object transformations of 21 updated classes, while two state-of-the-art approaches only handled 11 and 6 of 61, respectively.

Regular expression (regex) with modern extensions is one of the most popular string processing tools. However, poorly-designed regexes can yield exponentially many matching steps, and lead to regex Denial-of-Service (ReDoS) attacks under well-conceived string inputs. This paper presents Rescue, a three-phase gray-box analytical technique, to automatically generate ReDoS strings to highlight vulnerabilities of given regexes. Rescue systematically seeds (by a genetic search), incubates (by another genetic search), and finally pumps (by a regex-dedicated algorithm) for generating strings with maximized search time. We implemenmted the Rescue tool and evaluated it against 29,088 practical regexes in real-world projects. The evaluation results show that Rescue found 49% more attack strings compared with the best existing technique, and applying Rescue to popular GitHub projects discovered ten previously unknown ReDoS vulnerabilities.

Nowadays statistical machine learning is widely adopted in various domains such as data mining, image recognition and automated driving. However, software quality assurance for machine learning is still in its infancy. While recent efforts have been put into improving the quality of training data and trained models, this paper focuses on code-level bugs in the implementations of machine learning algorithms. In this explorative study we simulated program bugs by mutating Weka implementations of several classification algorithms. We observed that 8%-40% of the logically non-equivalent executable mutants were statistically indistinguishable from their golden versions. Moreover, other 15%-36% of the mutants were stubborn, as they performed not significantly worse than a reference classifier on at least one natural data set. We also experimented with several approaches to killing those stubborn mutants. Preliminary results indicate that bugs in machine learning code may have negative impacts on statistical properties such as robustness and learning curves, but they could be very difficult to detect, due to the lack of effective oracles.

Machine learning (ML) programs are being widely used in various human-related applications. However, their testing always remains to be a challenging problem, and one can hardly decide whether and how the existing knowledge extracted from training scenarios suit new scenarios. Existing approaches typically have restricted usages due to their assumptions on the availability of an oracle, comparable implementation, or manual inspection efforts. We solve this problem by proposing a novel program synthesis based approach, SynEva, that can systematically construct an oracle-alike mirror program for similarity measurement, and automatically compare it with the existing knowledge on new scenarios to decide how the knowledge suits the new scenarios. SynEva is lightweight and fully automated. Our experimental evaluation with real-world data sets validates SynEva's effectiveness by strong correlation and little overhead results. We expect that SynEva can apply to, and help evaluate, more ML programs for new scenarios.

A multithreaded program's interleaving space is discrete and astronomically large, making effectively sampling thread schedules for manifesting concurrency bugs a challenging task. Observing that concurrency bugs can be manifested by adjusting thread relative speeds, this paper presents the new concept of speed space in which each vector denotes a family of thread schedules. A multithreaded program's speed space is approximately continuous, easy-to-sample, and preserves certain categories of concurrency bugs. We discuss the design, implementation, and evaluation of our speed-controlled scheduler for exploring adversarial/abnormal schedules. The experimental results confirm that our technique is effective in sampling diverse schedules. Our implementation also found previously unknown concurrency bugs in real-world multithreaded programs.

Cyber-Physical Systems (CPS) intrinsically combine hardware and physical systems with software and network, which are together creating complex and correlated interactions. CPS applications often experience uncertainty in interacting with environment through unreliable sensors. They can be faulty and exhibit runtime errors if developers have not considered environmental interaction uncertainty adequately. Existing work in verifying CPS applications ignores interaction uncertainty and thus may overlook uncertainty-related faults. To improve verification accuracy, in this article we propose a novel approach to verifying CPS applications with explicit modeling of uncertainty arisen in the interaction between them and the environment. Our approach builds an Interactive State Machine network for a CPS application and models interaction uncertainty by error ranges and distributions. Then it encodes both the application and uncertainty models to Satisfiability Modulo Theories (SMT) formula to leverage SMT solvers searching for counterexamples that represent application failures. The precision of uncertainty model can affect the verification results. However, it may be difficult to model interaction uncertainty precisely enough at the beginning, because of the uncontrollable noise of sensors and insufficient data sample size. To further improve the accuracy of the verification results, we propose an approach to identifying and calibrating imprecise uncertainty models. We exploit the inconsistency between the counterexamples’ estimate and actual occurrence probabilities to identify possible imprecision in uncertainty models, and the calibration of imprecise models is to minimize the inconsistency, which is reduced to a Search-Based Software Engineering problem. We experimentally evaluated our verification and calibration approaches with real-world CPS applications, and the experimental results confirmed their effectiveness and efficiency.

Apache HBase is a widely used non-relational database in the Hadoop ecosystem. However, it will be inefficient if users perform multidimensional queries. Some of existing approaches incur extra costs in write performance or consistency maintenance, others are limited to specific applications. In this paper, we propose a novel data model called CFIDM, short for Column Family Indexed Data Model. In CFIDM, we convert the queried column into multiple column families. Values in the specific column are partitioned. Each partition is manifested by a column family, turning column family into an index with no additional cost. Then we provide guides to build this data model. Finally, we evaluate the effectiveness and versatility of CFIDM on the Bixi data set and the TPC-DS benchmark. Results show that CFIDM can save 6.6% disk space for Bixi and 35% for TPC-DS, maximally speeding up the queries by 5X and 5.5X respectively.

The applications ("apps") running on Android need to be adequately tested to avoid faults. Researchers have developed a number of test input generation tools for automated app testing and tried to improve test coverage to detect as many faults as possible. However, existing testing tools achieve very low coverage for some specific apps because they highly depend on external factors to run properly such as business logic, content providers and so on. In this paper, we present Xdroid to catch when and what kind of dependencies apps require and inject them correspondingly in a lightweight way. Working with a built-in tool Xmonkey which generates GUI events directly on Android devices, Xdroid implements an effective testing engine to get a high coverage. We evaluate Xdroid with diverse Android apps and demonstrate that it outperforms Monkey for 17%, Sapienz for 22% in coverage and meanwhile reveals more bugs than manual testing. Overall, it combines the benefits of both manual testing and random testing to improve test coverage and detect bugs effectively.

Activities are the fundamental components of Android applications (apps). However, existing approaches to automated testing for Android apps cannot effectively manage the transitions between activities, e.g., too rarely or too often. Besides, some techniques need to repeatedly restart from scratch and revisit every intermediate activity to reach a specific one, which leads to unnecessarily long transitions and wasted time. To address these problems, we propose AimDroid, a practical model-based approach to automated testing for Android apps that aims to manage the exploration of activities and meantime minimize unnecessary transitions between them. Specifically, AimDroid applies an activity-insulated multi-level strategy during testing and replaying. It systematically discovers unexplored activities and then intensively exploits every discovered individual with a reinforcement learning guided random algorithm. We conduct comprehensive experiments on 50 popular closed-source commercial apps that in total have billions of daily usages in China. The results demonstrate that AimDroid outperforms both Sapienz and Monkey in activity, method and instruction coverage, respectively. In addition, AimDroid also reports more crashes than the other two.

Many smartphone applications suffer from energy inefficiency problems, but locating these problems is quite difficult and labor-intensive. Automated tools for detecting energy inefficiency bugs have been shown to be effective. Existing approaches generally consist of two parts, namely the simulation part and the monitor part. The simulation part explores an application's state space guided by an application execution model, and the monitor part checks for occurrences of energy inefficiency patterns. However, existing approaches might miss energy inefficiency bugs due to their imprecise application execution models and oversimplified energy inefficiency diagnosis policies. In this paper, we proposed NavyDroid, an approach to diagnosing energy inefficiency problems more effectively. We summarized a comprehensive application execution model from Android specifications and expressed it as a state machine. By considering multiple patterns of wake lock misuses, our approach is able to detect more complex energy bugs caused by wake lock misuses. We implemented NavyDroidon top of Java Pathfinder (JPF) and applied it to real-world applications. We evaluated NavyDroid with 17 real-world Android applications, and NavyDroid located more energy inefficiency bugs in these applications than the existing work E-GreenDroid did. The results of our experiments demonstrate that our approach can effectively locate real energy inefficiency bugs in Android applications, suggesting its effectiveness.

Software frameworks are widely used in application development. But APIs of a framework may change when it evolves to accommodate new feature requests or to fix bugs. Those changes may break existing client programs of the framework, so client programs need to be migrated to the updated release when the framework evolves. Some technologies (e.g. call dependency analysis) have been proposed to find replacement APIs between the old and new framework releases. However, existing approaches based on call dependency analysis take whole method body as an analysis unit. The context in which a method is called is ignored. In this paper, we present a fine-grained approach named AUC-Miner to infer API usage change rules between two releases of the framework. To take method invocation context into consideration, we propose an approach to get more precise call relationship changes by code splitting. We also analyze indirect method invocations to re-fine call dependency analysis. After elaborating API usage change transactions, we adopt frequent item-set mining to generate API replacement rules. Text similarity and some heuristics to identify evolution of root methods are also applied in the mining progress. The evaluation of AUC-Miner on three popular frameworks shows that its precision is higher than basic call dependency analysis and another API replacement recommendation tool named AURA.

Computing clouds have become the platform of choice for the deployment and execution of scientific workflows. Due to the uncertainty and unpredictability of scientific exploration, the execution plan for a scientific workflow may vary from the definition. It is therefore of great significance to be able to discover actual workflows from execution histories (event logs) to reproduce experimental results and to establish provenance. However, most existing process mining techniques focus on discovering control flow-oriented business processes in a centralized environment, and thus, they are mostly inapplicable to the discovery of data flow-oriented, unstructured scientific workflows in distributed cloud environments. In this paper, we present Scientific Workflow Mining as a Service (SWMaaS) to support both intra-cloud and inter-cloud scientific workflow mining. The approach is implemented as a ProM plug-in and is evaluated on event logs derived from real-world scientific workflows. Through experimental results, we demonstrate the effectiveness and efficiency of our approach.

Modern component-based distributed software systems are increasingly required to offer non-stop service and thus their updates must be carried out at runtime. Different authors have already proposed solutions for the safe management of dynamic updates. Our contribution aims at improving their efficiency without compromising safety. We propose a new criterion, called version consistency, which defines when a dynamic update can be safely and efficiently applied to the components that execute distributed transactions. Version consistency ensures that distributed transactions be served as if they were operated on a single coherent version of the system despite possible concurrent updates. The paper presents a distributed algorithm for checking version consistency efficiently, formalizes the proposed approach by means of a graph transformation system, and verifies its correctness through model checking. The paper also presents ConUp, a novel prototype framework that supports the approach and offers a viable, concrete solution for the use of version consistency. Both the approach and ConUp are evaluated on a significant third-party application. Obtained results witness the benefits of the proposed solution with respect to both timeliness and disruption.

Dynamic software updating (DSU) is a technique that can update running software systems without stopping them. Most existing approaches require programmer participation to guarantee the correctness of dynamic updating. However, manually preparing dynamic updating is error-prone and time-consuming. Therefore, other approaches prefer to aggressively perform updating without programmer intervention, which may definitely lead to unanticipated runtime errors. To reduce human effort and enhance the reliability for dynamic updating, we leverage automatic runtime recovery (ARR) techniques to recover runtime errors caused by improper dynamic updating. This paper presents ADSU, a fully automatic DSU system using ARR. We evaluate ADSU with real updates from widely used open source software systems, i.e., Apache Tomcat, Apache FTP Server and jEdit. The preliminary results have shown that ADSU succeeds in automatically applying 11 of 16 real-world updates that existing counterparts cannot.

Smartphones are indispensable in people's daily lives. As smartphone apps are being increasingly concurrent, developers are increasingly unable to tackle the complexity and to avoid subtle concurrency bugs. To better address this issue, we propose a novel approach to manifesting concurrency bugs in Android apps based on the fact that one can simultaneously generate input events and their schedules for an app. We conduct static-dynamic hybrid analysis to find potentially conflicting resource accesses in an app. The app is then automatically pressure-tested by guided event and schedule generation. We implemented the prototype tool AATT and evaluated it over thirteen popular real-world open-source apps. AATT successfully found 9 concurrency bugs out of which 7 were previously unknown.

Mobile applications (apps) are mostly driven by touch gestures whose interactions are natural to human beings. However, generating gesture events for effective and efficient testing of such apps remains to be a challenge. Existing event generation techniques either feed the apps under test with random gestures or exhaustively enumerate all possible gestures. While the former strategy leads to incomplete test coverage, the latter suffers from efficiency issues. In this paper, we study the particular problem of gesture event generation for Android apps. We present a static analysis technique to obtain the gesture information: each UI component's potentially relevant gestures, so as to reduce the amount of gesture events to be delivered in the automated testing. We implemented our technique as a prototype tool GAT and evaluated it with real-world Android apps. The experimental results show that GAT is both effective and efficient in covering more code as well as detecting gesturerelated bugs.

Dynamic software updating (DSU) aims to patch software for fixing bugs or adding functions while it is running. Before update, developers need to make a dynamic patch ready, which includes update points, state transformers and a corresponding code patch. Existing practice mostly assumes manual preparation of dynamic patches, but this process can be both time-consuming and error-prone. Some pioneer work attempts to automate this process, but cannot guarantee the generation of safe dynamic patches for most updates. This paper presents a novel approach CURE to automatically generating safe dynamic patches. CURE takes two versions of software and their test cases as input, and automatically synthesizes state transformers and selects update points. We applied CURE to 28 updates for three real-world server software. The experimental results show that CURE generated safe dynamic patches automatically and their corresponding updates achieved an 88.7% success rate, as compared to 74.3% for TOS and 61.2% for default patches.

Physical devices are valuable resources for mobile application testing, especially for compatibility testing on diverse Android devices with customized specifications of manufacturers and different operating system versions. In order to cover as many kinds of devices as possible, large quantity of physical devices are needed. Therefore, how to allocate mobile devices efficiently among testing tasks becomes a problem for engineers. We address this challenge by proposing efficient resource scheduling policy across diverse application testing frameworks. Specifically, we abstract the components of testing platforms into valid testing models. Based on the testing models, a Wait-time Fairness scheduling strategy is proposed to efficiently allocate devices among testing jobs. We have implemented our approach in a platform called Apsaras and conducted experiments on 80 physical Android devices. Results show that our approach, comparing with traditional testing methods, can carry out testing jobs more efficiently and more fairly.

Energy inefficiency of smartphone apps is one of the important non-functional issues. It is common, but difficult to diagnose, and often involves sensor usage. GreenDroid provides a novel approach to systematically diagnose energy inefficiency problems in smartphone apps running on Android platforms. It derives an application execution model (AEM) from Android framework and leverages it to realistically simulate an application's runtime behaviors. It also automatically analyzes an application's sensory data utilization, monitors sensor listener and wake lock usage, and reports actionable information to developers.

Software systems are often subject to unexpected runtime errors. Automatic runtime recovery (ARR) techniques aim at recovering them from erroneous states and maintaining them functional in the field. This paper proposes Ares , a novel, practical approach to performing ARR. Our key insight is to leverage a system's already built-in error handling support to recover from unexpected errors. To this end, we synthesize error handlers via two methods: error transformation and early return. We also equip Ares with a lightweight in-vivo testing infrastructure to select the right synthesis methods and avoid potentially dangerous error handlers. Unlike existing ARR techniques based on heavyweight mechanisms (e.g., checkpoint-restart and runtime monitoring), our approach expands the intrinsic capability of runtime error resilience already existing in software systems to handle unexpected errors. Ares's lightweight mechanism makes it practical and easy to be integrated into production environments. We have implemented Ares on top of both the Java HotSpot VM and Android ART, and applied it to 52 real-world bugs. The results are promising — Ares successfully recovers from 39 of them and incurs low overhead.

Controllers restrict systems to behave only in good manners. Different from controlling monolithic systems where controllers can be automatically synthesized from specifications, controlling distributed systems often has to use distributed controllers that are manually programmed. To ensure their correctness, manually programmed controllers themselves need to be formally verified. This task can be challenging due to the complexity caused by the autonomy and asynchrony of distributed controllers. The limited scalability of existing model checkers also exacerbates the problem. In this paper we explore the modeling and verification of distributed controllers using Alloy. Besides resorting to the Small Scopes Hypothesis of the Alloy methodology, we also leverage local invariant based modular verification techniques for better scalability. A local invariant characterizes a logical relationship between a local sub-system and its neighbors and abstracts away the concrete interactions. These concrete interactions would otherwise explode the system state space during verification. The approach is first illustrated with the well-understood Two-Phase Commit protocol, and then is applied to the verification of several dynamic software update protocols, which gives an initial evidence of its effectiveness.

Software should behave correctly even in adverse conditions. Particularly, we study the problem of automated validation of crash consistency, i.e., file system data safety when systems crash. Existing work requires non-trivial manual efforts of specifying checking scripts and workloads, which is an obstacle for software developers. Therefore, we propose C3, a novel approach that makes crash consistency validation as easy as pressing a single button. With a program and an input, C3 automatically reports inconsistent crash sites. C3 not only exempts developers from the need of writing crash site checking scripts (by an algorithm that computes editing distance between file system snapshots) but also reduces the reliance on dedicated workloads (by test amplification). We implemented C3 as an open-source tool. With C3, we found 14 bugs in open-source software that have severe consequences at crash and 11 of them were previously unknown to the developers, including in highly mature software (e.g., GNU zip and GNU coreutils sort) and popular ones being actively developed (e.g., Adobe Brackets and TeXstudio).

Order of shared memory accesses, known as the shared memory dependence, is the cornerstone of dynamic analyses of concurrent programs. In this paper, we study the problem of reducing shared memory dependences. We present the first online software-only algorithm to reduce shared memory dependences without vector clock maintenance, opening a new direction to a broad range of applications (e.g., deterministic replay and data race detection). Our algorithm exploits a simple yet effective observation, that adaptive variable grouping can recognize and match spatial locality in shared memory accesses, to reduce shared memory dependences. We designed and implemented the bisectional coordination protocol, which dynamically maintains a partition of the program's address space without its prior knowledge, such that shared variables in each partitioned interval have consistent thread and spatial locality properties. Evaluation on a set of real-world programs showed that by paying a 0--54.7% (median 21%) slowdown, bisectional coordination reduced 0.95--97% (median 55%) and 16--99.99% (median 99%) shared memory dependences compared with RWTrace and LEAP, respectively.

Pervasive applications are involving more and more autonomous computing and communicating devices, augmented with the abilities of sensing and controlling the logical/physical environment. To enable context-awareness for such applications, we are challenged by the intrinsic asynchrony of the computing environment. Predicate detection is a well studied technique dedicated to detecting global predicates over asynchronous computations and can be employed to achieve context-awareness of the asynchronous environment. However, there is no methodological framework which guides us to systematically apply the abstract predicate detection theory to the development of concrete context-aware applications. To this end, we present the Predicate Detection-based ContextAwareness (PD-CA) framework. PD-CA maps the concepts of context-awareness to concepts of predicate detection. PD-CA also presents a design process of providing middleware support for context-aware applications. Under the guidance of the PD-CA framework, we design and implement the Middleware Infrastructure for Predicate detection in Asynchronous environments (MIPA). We also propose the programming toolkit to facilitate the development of context-aware applications based on MIPA, and demonstrate the use of the toolkit by a case study of a chemical plant safety management application. Experimental evaluations show the performance of MIPA in enabling context-awareness despite of the asynchrony.

Process mining, especially process discovery, has been utilized to extract process models from event logs. One challenge faced by process discovery is to identify concurrency effectively. State-of-the-art approaches employ activity orders in traces to undertake process discovery and they require stringent completeness notions of event logs. Thus, they may fail to extract appropriate processes when event logs cannot meet the completeness criteria. To address this problem, we propose in this paper a novel technique which leverages activity dependences in traces. Based on the observation that activities with no dependencies can be executed in parallel, our technique is in a position to discover processes with concurrencies even if the logs fail to meet the completeness criteria. That is, our technique calls for a weaker notion of completeness. We evaluate our technique through experiments on both real-world and synthetic event logs, and the conformance checking results demonstrate the effectiveness of our technique and its relative advantages compared with state-of-the-art approaches.

Software building is recurring and time-consuming. Based on the finding that a significant portion of compilations in incremental build is unnecessary, we propose by path compilation, an efficient build technique that avoids unnecessary recompilation with automated detection of redundant dependencies and unessential changes in source files. The technique is lightweight and transparent to software developers, and can be easily applied to existing build systems. We evaluated our approach on a set of real-world open source projects. The results show that 83% ~ 97% of the recompilations are unnecessary and our approach can accelerate the incremental build up to 44.20%.

Debugging is challenging and labor-intensive. Debugging programs with weak or no oracle is even more difficult due to lack of passing and failing test runs as well as their comparisons. To address these challenges, we exploit metamorphic relations to construct new programs that are enhanced with synthesized oracle, and combine concolic testing and branch-switching debugging to localize potentially faulty places in original programs. We name our approach concolic metamorphic debugging (or Comedy for short). We experimentally evaluated Comedy with real-world Java programs. The experimental results reported that Comedy successfully generated debugging report for 88.4% of 2,330 faulty programs. The average branch distance between the reported locations and the real fault places is only 1.68. Besides, 36% of the debugging reports precisely locate the fault.

Smartphone applications are becoming increasingly popular. However, these applications can suffer limited power budgets or malfunctioned sensing issues from their host devices. Computation offloading addresses this issue by delegating local computation workloads to remote servers. In this paper, we present Cose Droid, a framework that supports dynamic computation- and sensing-offloading across different Android mobile devices. This enables Android applications to virtually "borrow" computation or sensing resources from other devices. We experimentally evaluated Cose Droid with real-world Android applications. The experimental results confirmed Cose Droid's effectiveness in on-demand offloading, as well as supporting sensor variety and spontaneous sensing recovery.

Inter-thread shared memory dependences are crucial to understanding the behavior of concurrent systems, as such dependences are the cornerstone of time-travel debugging and further predictive trace analyses. To enable effective and efficient shared memory dependence tracing, we present an optimistic scheme addressing the challenge of capturing exact dependences between unsynchronized events to reduce the probe effect of program instrumentation. Specifically, our approach achieved a wait-free fast path for thread-local reads on x86-TSO relaxed memory systems, and simultaneously achieved precise tracing of exact read-after-write, write-after-write and write-after-read dependences on the fly. We implemented an open-source RWTrace tool, and evaluation results show that our approach not only achieves efficient shared memory dependence tracing, but also scales well on a multi-core computer system.

Dynamic Software Update (DSU) is a technique to upgrade running programs without shutting them down. DSU can improve system availability and maintenance flexibility. However, its adoption in practice is still limited due to the risk of system misbehavior that careless DSU may bring. To reduce this risk we propose a formal framework for the specification and verification of DSU. Different from previous approaches where DSU is described from the viewpoint of program's internal state transitions, our framework focuses on program's external behavior and its effect on its environment. This more abstract view avoids over specification of DSU and allows for better DSU flexibility. Based on this framework, we also devise a mechanism that automatically synthesizes runtime monitors to improve DSU timeliness without compromising its safety.

Context-aware applications adapt their behavior based on contexts. Contexts can, however, be incorrect. A popular means to build dependable applications is to augment them with a set of constraints to govern the consistency of context values. These constraints are evaluated upon context changes to detect inconsistencies so that they can be timely handled. However, we observe that many context inconsistencies are unstable. They vanish by themselves and do not require handling. Such inconsistencies are detected due to misaligned sensor sampling or improper inconsistency detection scheduling. We call them unstable context inconsistencies (or STINs). STINs should be avoided to prevent unnecessary inconsistency handling and unstable behavioral adaptation to applications. In this article, we study STINs systematically, from examples to theoretical analysis, and present algorithms to suppress their detection. Our key insight is that only certain patterns of context changes can make a consistency constraint subject to the detection of STINs. We derive such patterns and proactively use them to suppress the detection of STINs. We implemented our idea and applied it to real-world applications. Experimental results confirmed its effectiveness in suppressing the detection of numerous STINs with negligible overhead, while preserving the detection of stable context inconsistencies that require inconsistency handling.

Mobile devices are gradually taking over traditional computers' dominance in human lives. With the ever-increasing shipment of mobile apps running on these devices, their quality issues become a severe challenge. Although automated testing techniques are being widely studied, they mostly fall short of handling mobile apps' complex interactions, e.g., A finger swipe or device shaking gesture, leading to inadequate testing. In this paper, we present a novel User Guided Automation (UGA) technique to address testing challenges incurred by such complex interactions. UGA exploits user insights to complement automated testing techniques by recording user-guided app executions, replaying apps to certain stop points, and systematically exploring state space from these stop points. We implemented our work as a prototype UGA tool on Android platform and evaluated it on seven real-world Android apps. Evaluation results show that UGA achieved 1.59-21.78× improvement in terms of method coverage over state-of-the-art automated techniques in testing mobile apps.

Applications in pervasive computing are often context-aware. However, due to uncontrollable environmental noises, contexts collected by applications can be distorted or even conflicting with each other. This is known as the context inconsistency problem. To provide reliable services, applications need to validate contexts before using them. One promising approach is to check contexts against consistency constraints at the runtime of applications. However, this can bring heavy computations due to tremendous amounts of contexts, thus leading to deteriorated performance to applications. Previous work has proposed incremental or concurrent checking techniques to improve the checking performance, but they heavily rely on CPU computing. In this paper, we propose a novel technique GAIN to exploit GPU computing to improve the checking performance. GAIN can automatically recognize parallel units in a constraint and schedule their checking in parallel on GPU cores. We evaluated GAIN with various constraints under different workloads. Our evaluation results show that, compared to CPU-based computing, GAIN saves CPU computing resources for pervasive applications while checks constraints much more efficiently.

Context-aware applications rely on contexts derived from sensory data to adapt their behavior. However, contexts can be inconsistent and cause application anomaly or crash. One popular solution is to detect and resolve context inconsistencies at runtime. However, we observe that many detected inconsistencies do not indicate real context problems. Instead, they are caused by improper inconsistency detection. These inconsistencies are harmless, and their resolution is unnecessary or may even cause new problems. We name them inconsistency hazards. Inconsistency hazards should be suppressed, but their occurrences resemble normal inconsistencies. In this paper, we present a pattern-learning based approach SHAP to suppressing the detection of inconsistency hazards. Our key insight is that the detection of such hazards is subject to certain patterns of context changes. These patterns, although difficult to specify manually, can be learned effectively from historical inconsistency detection data. We evaluated our SHAP experimentally through three context-aware applications. The results reported that SHAP can automatically suppress the detection of over 90% inconsistency hazards, while preserving the detection of over 98% normal inconsistencies, with only negligible overhead.

Deterministic replay tools help programmers debug concurrent programs. However, for long-running programs, a replay tool may generate huge log of shared memory access dependences. In this paper, we present CARE, an application-level deterministic record and replay technique to reduce the log size. The key idea of CARE is logging read-write dependences only at per-thread value prediction cache misses. This strategy records only a subset of all exact read-write dependences, and reduces synchronizations protecting memory reads in the instrumented code. Realizing that such record strategy provides only value-deterministic replay, CARE also adopts variable grouping and action prioritization heuristics to synthesize sequentially consistent executions at replay in linear time. We implemented CARE in Java and experimentally evaluated it with recognized benchmarks. Results showed that CARE successfully resolved all missing read-write dependences, producing sequentially consistent replay for all benchmarks. CARE exhibited 1.7--40X (median 3.4X) smaller runtime overhead, and 1.1--309X (median 7.0X) smaller log size against state-of-the-art technique LEAP.

Due to the demand for bugs fixing and feature enhancements, developers inevitably need to update in-use software systems. Instead of shutting down a running system before updating, it is often desirable and sometimes mandatory to patch the running software system on the fly, with a mechanism generally referred as dynamic software updating (DSU). Practical DSU strategies often require manual specification of update points in the program for performing dynamic updates. At these points DSU systems will update the program code, and also migrate the program state to the new version program (using transformation functions). However, finding appropriate update points is non-trivial because the choice of update points has great influence on two competing factors: the timeliness of DSU and the complexity of transformation functions; and to strike a good balance between them requires a deep understanding of both versions of the program. In this exploratory paper, we conceive an automated approach to the recommendation of update points for developers. We conduct a set of preliminary experiments with a real world software update case to examine the feasibility of the approach.

Self-adaptive applications address environmental dynamics systematically. They can be faulty and exhibit runtime errors when environmental dynamics are not considered adequately. It becomes more severe when uncertainty exists in their sensing and adaptation to environments. Existing work verifies self-adaptive applications, but does not explicitly consider environmental constraints or uncertainty. This gives rise to inaccurate verification results. In this paper, we address this problem by proposing a novel approach to verifying self-adaptive applications suffering uncertainty in their environmental interactions. It builds Interactive State Machine (ISM) models for such applications and verifies them with explicit consideration of environmental constraints and uncertainty. It then refines verification results by prioritizing counterexamples according to their probabilities. We experimentally evaluated our approach with real-life self-adaptive applications, and the experimental results confirmed its effectiveness. Our approach reported 200-660% more counterexamples than not considering uncertainty, and eliminated all false counterexamples caused by ignoring environmental constraints.

The event stream model of computation has a wide range of applications, e.g, computer system monitoring, physical environment sensing/surveillance, and stock trade monitoring. Sliding windows are widely used to facilitate effective event stream processing. However, it is greatly challenged when the event sources are distributed and asynchronous. One important technique to cope with the asynchrony is to utilize that the meaningful snapshots of an asynchronous computation form a distributive lattice. It thus becomes the central challenge whether this lattice structure still preserves and how to maintain it at runtime, when we restrict our attention to events within sliding windows. To address this challenge, we first prove that the snapshots of the asynchronous event streams within the sliding windows form a convex distributive lattice (denoted by Lat-Win). This enables us to easily integrate existing predicate specification and detection techniques, to express and monitor properties of our concern over asynchronous event streams. Then we propose an algorithm to maintain Lat-Win at runtime. The proposed scheme is evaluated in a context-aware smart office scenario, where activities of the user can be recognized by monitoring multiple streams of sensed events. The Lat-Win algorithm is implemented on the open-source context-aware middleware we developed. The evaluation results first show the advantage of adopting sliding windows over asynchronous event streams. Then they show the performance of detecting specified predicates within Lat-Win, with dynamic changes in the computing environment.

Runtime reconfigurations of component-based systems must be undertaken with careful considerations of dependency between components. The safer and less disruptive a reconfiguration strategy is, the more accurate dependency information it needs. This paper proposes to manage dynamic dependency between components with mealy machine automatically derived from the implementation of components. To maintain the current dependency information for a component at runtime, the corresponding machine is instrumented into the component implementation in such a way that it is always synchronized with the execution of the component. We implemented a prototypical tool for this approach and evaluated it with a realistic benchmark application. The results show that our approach achieves a high accuracy and keeps low overheads without introducing any manual work.

Cyber-physical systems are systems that integrate the digital computational world with the real physical world, often using sensors and actuators as interfaces. There exist many application domains of cyber-physical systems such as autonomous systems, process control systems, robotic systems, and context-aware systems. The physical world is a complex and continuous world that changes in real-time while the computational world is a simplified and discrete world that often stores a delayed, likely inaccurate image of the physical world using sensory data. The mismatch between these two worlds poses unique challenges of developing software for cyber-physical systems.

Processes are an effective and efficient way to construct on-demand Internetware applications. It is often needed to evaluate whether two process-driven applications are consistent, or whether the implemented process conforms to the process specification. Most existing methods only return qualitative results (i.e., true or false), so slight inconsistencies may lead to a false result. To address this problem, based on activity constraints, we have presented a quantitative approach to process consistency analysis. In this paper, we focus on the implementation issues of our approach and introduce how to use our tool in practice.

Self-adaptive applications can easily contain faults. Existing approaches detect faults, but can still leave some undetected and manifesting into failures at runtime. In this paper, we study the correlation between occurrences of application failure and those of consistency failure. We propose fixing consistency failure to reduce application failure at runtime. We name this environment rematching, which can systematically reconnect a self-adaptive application to its environment in a consistent way. We also propose enforcing atomicity for application semantics during the rematching to avoid its side effect. We evaluated our approach using 12 self-adaptive robot-car applications by both simulated and real experiments. The experimental results confirmed our approach's effectiveness in improving dependability for all applications by 12.5-52.5%.

Formal specification and runtime detection of contextual properties is one of the primary approaches to enabling context awareness in pervasive computing environments. Due to the intrinsic dynamism of the pervasive computing environment, dynamic properties, which delineate concerns of context-aware applications on the temporal evolution of the environment state, are of great importance. However, detection of dynamic properties is challenging, mainly due to the intrinsic asynchrony among computing entities in the pervasive computing environment. Moreover, the detection must be conducted at runtime in pervasive computing scenarios, which makes existing schemes do not work. To address these challenges, we propose the property detection for asynchronous context (PDAC) framework, which consists of three essential parts: 1) Logical time is employed to model the temporal evolution of environment state as a lattice. The active surface of the lattice is introduced as the key notion to model the runtime evolution of the environment state; 2) Specification of dynamic properties is viewed as a formal language defined over the trace of environment state evolution; and 3) The SurfMaint algorithm is proposed to achieve runtime maintenance of the active surface of the lattice, which further enables runtime detection of dynamic properties. A case study is conducted to demonstrate how the PDAC framework enables context awareness in asynchronous pervasive computing scenarios. The SurfMaint algorithm is implemented and evaluated over MIPA--the open-source context-aware middleware we developed. Performance measurements show the accuracy and cost-effectiveness of SurfMaint, even when faced with dynamic changes in the asynchronous pervasive computing environment.

To stay on the cutting edge, Web services ought to adapt themselves to the evolving business requirements and the changing environments. For a long-running service choreography, its member services may need to evolve even at run-time. However, inconsistencies or spurious results (e.g., unspecified receptions and deadlocks) may occur if these services evolve dynamically in an uncoordinated manner. To cope with this problem, we propose an approach that supports the dynamic evolution of choreographies. In our approach, two mechanisms are proposed to make sure that the choreography evolution can be conducted in an orderly fashion. First, an evolution protocol is proposed to support dynamic co-evolution of the member services in a choreography. Second, the proposed approach restricts choreography changes to one single service only if the relevant partner services can evolve simultaneously. A typical purchase order application is used to motivate our proposal and illustrate the viability of our approach.

Practical software systems are subject to frequent updates for fixing their bugs or addressing new requirements. Updating a software system without stopping and restarting it is desired, as this helps reduce the redeployment cost as well as achieving the high availability. Existing techniques for dynamically updating Java programs may introduce noticeable pauses during which these programs are unable to function. We in this paper present Javelus, a dynamic Java update system with greatly reduced pausing time but without sacrificing update flexibility and system efficiency. Different from previous approaches, Javelus uses a lazy update mechanism with which an object-to-update will not be updated until it is really used. We implemented Javelus on top of an industry-strength OpenJDK HotSpot VM. We evaluated Javelus with real updates to Tomcat 7 and the same micro array benchmark used in evaluating Jvolve and DCE VM. The experiments report promising results that Javelus only incurred a pausing time two orders of magnitude smaller than those of Jvolve and DCE VM.

Self-adaptive systems are attractive due to their ability of adapting to changeable environments automatically. However, such systems may be subject to runtime failures when all environmental dynamics cannot be adequately considered at design time. When such failures occur at runtime, a system's internal adaptation logic usually has become inconsistent with its environment, according to our observation. We call this inconsistency sync-loss error. From our project experiences, we empirically identified a strong correlation between sync-loss error and system failure. This motivated us to fix sync-loss error in order to reduce failure for self-adaptive systems. In this paper, we formulate the problem of detecting sync-loss error, and present a framework ReSync to automatically fix sync-loss errors by desynchronizing a system with its environment. We experimentally evaluated ReSync on real robot cars with 20 different system versions. The evaluation reported promising results that ReSync can automatically recover our robot car systems from sync-loss errors, and significantly reduce the failure rate from 90.9% to 11.7-28.8%.

Detecting and resolving context inconsistency is critical to pervasive computing applications and infrastructures. Context inconsistency occurs when an application perceives contexts that breach predefined consistency constraints. This can drive an application to behave abnormally or even cause failure. Existing work commonly assumes the presence of a single application suffering from context inconsistency, such that specific repair actions can be taken to resolve the inconsistency for this application. However, when multiple applications run on the same infrastructure, they may impose conflicting requirements on resolving context inconsistency. In this paper, we propose a novel view-based approach ConsView to address such conflicting requirements. In ConsView, each application has a specific view to its own contexts that satisfy its own requirement on resolving context inconsistency. Such views are called consistent context views. We discuss the challenges of doing so and our ideas for addressing them. We implemented a prototype infrastructure supporting consistent context views, and evaluated it experimentally with simulated applications of real-life settings. The results confirmed the effectiveness and efficiency of our ConsView approach.

Efficient detection of RFID-tagged physical objects is one of the key enabling technologies to build pervasive Internet-of-Things applications. However, the detection of tagged-objects is faced with the critical challenge of tag dynamics, which mainly arises from the movement of tagged physical objects. To capture tag dynamics, the application needs to detect the presence/absence of tags in an accurate, timely and cost-effective way. To address these challenges, we propose the Prediction of Tag Dynamics (PTD) algorithm. PTD achieves runtime detection of tagged-objects by i) streaming of the temporally-correlated tag readings obtained from persistent tracking of the tagged-object, and ii) runtime prediction of tag dynamics based on the streaming of tag readings. The performance of PTD is investigated based on real implementation and experimental evaluation, where PTD processes tag readings gathered with high fidelity from persistent tracking of real activities of tagged objects. The evaluation results demonstrate the accuracy, timeliness and cost-effectiveness of PTD.

Service composition provides an effective way to conduct cross-organizational business transactions. Some protocols and frameworks have been proposed to ensure ACID properties of transactional service requisitions from the perspective of a service requester. However, few of them have focused on how to optimize the services' profits from the perspective of a service provider. In this paper, we present a priority-based transaction commit protocol for composite Web services. For this protocol, Nash Bargaining Solution (NBS) is used to differentiate service requesters so that services (i.e., resources) can be allocated with different priorities. In this way, the profit of a service provider can be maximized with proportional fairness. For service requesters, the proposed protocol can guarantee the atomicity of service requisitions. Our experimental results reveal that the proposed protocol can significantly enhance the profit of service providers without violating atomicity of Web service transactions.

Internetware applications are context-aware and adaptive to their environmental changes. Faulty adaptation may arise when these applications face unexpected situations. Such adaptation faults can be difficult to detect at design time. The recent Adaptation Finite-State Machine (A-FSM) approach proposes to statically analyze model-based context-aware applications for adaptation faults. However, this approach may suffer expressiveness and precision problems. To address these limitations, we propose an Adaptation Model (AM) approach. As compared with A-FSM, AM offers increased expressive power to model complex rules, and guarantees soundness in fault detection. Besides, AM deploys an efficient rule evaluation technique to cater for context-aware applications that are subject to continual environmental changes. We evaluated our AM approach using both simulated and real-world experiments with two applications. The experimental results confirmed that AM can detect real faults missed by A-FSM, and avoid false positives that were misreported otherwise.

Formal specification and runtime detection of temporal properties for pervasive context is one of the primary approaches to achieving context-awareness. Though temporal logics have been widely used in specification of temporal properties, they are faced with severe challenges in Pervasive Computing (PvC) scenarios. First, temporal logics are traditionally defined over infinite traces of possible system behavior. However in PvC scenarios, applications observe finite prefixes of (potentially infinite) traces of environment state evolution, and adapt their behavior accordingly. Second, specification and detection of temporal properties are challenged by the intrinsic asynchrony of PvC environments. Discussions above necessitate a systematic approach to formal specification and runtime detection of temporal properties for asynchronous context. To this end, we propose CTL3(3-valued Computation Tree Logic), which i) adopts 3-valued semantics to capture the inconclusiveness when applications only observe finite prefixes of environment state evolution; ii) inherits the notion of branching time to capture the uncertainty resulting from the asynchrony of PvC environments. A case study is conducted to demonstrate how CTL3supports context-awareness in PvC scenarios. The runtime checking algorithm of CTL3is implemented and evaluated over MIPA - the open-source context-aware middle-ware we developed. The case study demonstrates the necessity of adopting CTL3in PvC scenarios, while the performance measurements show the cost-effectiveness of runtime checking contextual properties in CTL3.

Runtime detection of contextual properties is one of the primary approaches to enabling context-awareness in pervasive computing scenarios. Among various properties the applications may specify, the concurrency property, i.e., property delineating concurrency among contextual activities, is of great importance. It is because the concurrency property is one of the most frequently specified properties by context-aware applications. Moreover, the concurrency property serves as the basis for specification of many other properties. Existing schemes implicitly assume that context collecting devices share the same notion of time. Thus, the concurrency property can be easily detected. However, this assumption does not necessarily hold in pervasive computing environments, which are characterized by the asynchronous coordination among heterogeneous computing entities. To cope with this challenge, we identify and address three essential issues. First, we introduce logical time to model behavior of the asynchronous pervasive computing environment. Second, we propose the logic for specification of the concurrency property. Third, we propose the Concurrent contextual Activity Detection in Asynchronous environments (CADA) algorithm, which achieves runtime detection of the concurrency property. Performance analysis and experimental evaluation show that CADA effectively detects the concurrency property in asynchronous pervasive computing scenarios.

WS-BPEL processes can facilitate service discovery when the services have multiple interfaces in certain order. Current approaches derive the abstract WS-BPEL processes directly from the corresponding executable ones by hiding or omitting the internal activities. However, these simple approaches may prevent the services from being found by valuable potential partners at service discovery stage. To address this problem, we propose a novel approach to refactoring the executable and abstract WS-BPEL processes for service discovery. We show the application of our approach through a typical travel agency service.

There is an increasing demand for the runtime reconfiguration of distributed systems in response to changing environments and evolving requirements. Reconfiguration must be done in a safe and low-disruptive way. In this paper, we propose version consistency of distributed transactions as a safe criterion for dynamic reconfiguration. Version consistency ensures that distributed transactions be served as if there were operating on a single coherent version of the system despite possible reconfigurations that may happen meanwhile. The paper also proposes a distributed algorithm to maintain dynamic dependences between components at architectural level and enable low-disruptive version-consistent dynamic reconfigurations. An initial assessment through simulation shows the benefits of the proposed approach with respect to timeliness and low degree of disruption.

Self-adaptive software is expected to adjust itself attributes or structures at runtime in response to changes. Aiming at addressing some challenging problems such as difficult mathematically modeling software using the current control theoretical methods, we propose a novel fuzzy-control-based approach to achieve self-adaptive software, which is presented as framework of fuzzy self-adaptive software (FFSAS). In this framework, the general model, the implementation architecture, and the design methodology are put forward and discussed in detail. The fuzzy-control-based approach is evaluated with a news-website case study.

Internetware is envisioned as a new software paradigm for resource integration and sharing in the open, dynamic and autonomous network environment. In this paper we discuss our visions and explorations of this new paradigm, with focus placed on the methodological perspective. A set of enabling techniques on flexible coordination of autonomous services, automatic adaptation to changing environment and trust management-based assurance of dependability are proposed to help the development of Internetware applications.

This demo displays the use of the prototypical ARTEMIS middleware system, which is developed at Nanjing University to support the construction, execution and evolution of applications in the open, dynamic and decentralized network environment of the Internet. To adapt to such a new environment, software application systems must be more flexible, more reactive, and more evolvable than before [1]. Built upon services from autonomous external sources, these application systems also have to explicitly consider the trustworthiness of the services. With these considerations, this version of ARTEMIS middleware is featured by its support for (1) multiple coordination modes based on various software architecture styles; (2) dynamic software architecture-based online reconfigurations, in reaction to the runtime changes in the environment and requirements; (3) trustworthiness evaluation at both the service level and the system level, which helps users to ensure and improve user's satisfaction on the system constructed.

Contexts, the pieces of information that capture the characteristics of computing environments, are often inconsistent in the dynamic and uncertain pervasive computing environments. Various schemes have been proposed to check context consistency for pervasive applications. However, existing schemes implicitly assume that the contexts being checked belong to the same snapshot of time. This limitation makes existing schemes do not work in pervasive computing environments, which are characterized by the asynchronous coordination among computing devices. The main challenge imposed on context consistency checking by asynchronous environments is how to interpret and detect concurrent events. To this end, we propose in this paper the concurrent events detection for asynchronous consistency checking (CEDA) algorithm. An analytical model, together with corresponding numerical results, is derived to study the performance of CEDA. We also conduct extensive experimental evaluation to investigate whether CEDA is desirable for context-aware applications. Both theoretical analysis and experimental evaluation show that CEDA accurately detects concurrent events in time in asynchronous pervasive computing environments, even with dynamic changes in message delay, duration of events and error rate of context collection.

Facing changing environments and evolving business rules, composite services ought to be adaptable, even at run-time. Existing mainstream service composition languages and execution engines exhibit insufficient support for variability and adaptability to cater for dynamic changes. Research efforts have been put on the extension of the languages and argumentation of the engines. However, how to ensure the correctness for the adaptation of a running composite service instance and minimize unnecessary re-execution of component services remains a challenge. To address this problem, we propose a model-based approach that allows run-time adaptation of composite services. It is based on an instance transfer mechanism that transfers an active instance of the old service composition schema to a appropriate state of the new schema. Algorithms are proposed to find the appropriate destination states of the transformation. After the migration, the suspended instances can resume their execution according to the new schema. An example based on a FindRoute composite service is also included.

Abstract This paper presents a graph‐oriented framework, called WebGOP, for architecture modeling and programming of Web‐based distributed applications. WebGOP is based on the graph‐oriented programming (GOP) model, under which the components of a distributed program are configured as a logical graph and implemented using a set of operations defined over the graph. WebGOP reshapes GOP with a reflective object‐oriented design, which provides powerful architectural support in the World Wide Web environment. In WebGOP, the architecture graph is reified as an explicit object which itself is distributed over the network, providing a graph‐oriented context for the execution of distributed applications. The programmer can specialize the type of graph to represent a particular architecture style tailored for an application. WebGOP also has built‐in support for flexible and dynamic architectures, including both planned and unplanned dynamic reconfiguration of distributed applications. We describe the WebGOP framework, a prototypical implementation of the framework on top of SOAP, and a performance evaluation of the prototype. The prototype demonstrated the feasibility of our approach. Results of the performance evaluation showed that the overhead introduced by WebGOP over SOAP is reasonable and acceptable. Copyright © 2003 John Wiley & Sons, Ltd.

This paper presents a novel approach, called WebGOP, for architecture modeling and programming of web-based distributed applications. WebGOP uses the graph-oriented programming (GOP) mode, under which the components of a distributed program are configured as a logical graph and implemented using a set of operations defined over the graph. WebGOP extends the application of GOP to the World Wide Web environment and provides more powerful architectural support. In WebGOP, the architecture graph is reified as an explicit object which itself is distributed over the network providing a graph-oriented context for the execution of distributed applications. The programmer can specialize the type of a graph to represent a particular architecture style tailored for an application. WebGOP also has built-in support for flexible and dynamic architectures, including dynamic reconfiguration. We describe the WebGOP framework, a prototypical implementation of the framework on top of SOAP, and performance evaluation of the prototype. Results of the performance evaluation showed that the overhead introduced by WebGOP over SOAP is reasonable and acceptable.

Software coordination is central to the construction of large-scale high-performance distributed applications with software services scattered over the decentralized Internet. In this paper, a new mobile-agent-based architecture is proposed for the utilization and coordination of geographically distributed computing resources. Under this architecture, a user application is built with a set of software agents that can travel across the network autonomously. These agents utilize the distributed resources and coordinate with each other to complete their task. This approach’s advantages include the natural expression and flexible deployment of the coordination logic, the dynamic adaptation to the network environment and the potential of better application performance. This coordination architecture, together with an object-oriented hierarchical parallel application framework and a graphical application construction tool, is implemented in the HOOPE environment, which provides a systematic support for the development and execution of Internet-based distributed and parallel applications in the petroleum exploration industry.