Post-release user feedback is a major control signal for maintenance and evolution in modern software development, yet it is noisy, fragmented, and difficult to translate into developer-usable issue specifications. Large Language Models (LLMs) can assist this transformation, but they often hallucinate or over-commit when evidence is weak, conflicting, or incomplete, limiting their robustness in automated software engineering workflows. We propose AGR (Agent-Governed Retrieval-Augmented Generation), a framework that regulates evidence acquisition and generation decisions via agentic control. AGR first applies an agentic triage step to filter low-signal or off-topic feedback, then retrieves evidence from a three-category hierarchy comprising official documentation, historical bug reports, and targeted web sources. It further performs confidence-weighted fusion across authoritative categories and uses an agentic decision module to verify relevance and sufficiency, trigger additional retrieval or online search when needed, reuse prior reports via memory, and abstain when evidence-supported grounding cannot be established. We evaluate AGR on two open-source software ecosystems, Firefox and VS Code. Results show that AGR achieves strong decision accuracy in triage and evidence verification, and produces more actionable and engineering-useful issue specifications than both raw feedback and a strong LLM baseline, while reducing unsupported details.

The scalability and efficiency of software testing are persistently hindered by a reliance on manual practices for creating test cases and bug reports. Moreover, the valuable insights from post-release user feedback are often lost due to the lack of an automated pipeline connecting them to regression testing. To overcome these challenges, we present a novel framework that synergizes the structural representation of software with the generative power of Large Language Models (LLMs). We first represent the application’s Graphical User Interface (GUI) as a directed graph, capturing its components and navigational logic. This queryable graph provides essential, structured context for a Retrieval-Augmented Generation (RAG) model, which then autonomously generates and populates high-quality test cases and bug reports. A key innovation of our work is a fully automated pipeline that processes unstructured user feedback and error reports, transforming them into standardized test cases. We selected some reviews from a popular mobile App for preliminary experiments and verified the feasibility and efficiency improvement of this method.

In architecture-based self-adaptation, the managed system is represented as a collection of components that adapt to environmental changes by reconfiguring their composition. When time constraints are involved, process flow diagrams are typically used for verification. However, the ambiguity between flow diagrams and component diagrams often causes confusion, complicating system design. This paper establishes a clear relationship between components and process flows, proposing a framework that facilitates component-oriented system development. Furthermore, it introduces an implementation API for self-adaptive systems with time-constraint verification capabilities and outlines a design procedure for developing such systems. To validate the proposed framework, we implemented and verified the operation of a transportation system, demonstrating its feasibility. Notably, the framework’s system structure ensures that even when a component is involved in multiple functions, the system configuration search can be completed within a fixed amount of time, regardless of the number of functions.

In software testing, traceability links between software requirements and test cases are crucial for managing test coverage and detecting defects effectively. Accurate traceability enables comprehensive coverage analysis, identification of untested requirements, and targeted defect detection. The manual effort required to establish and update traceability links often leads to high labor costs and a greater risk of human error. Furthermore, as requirements evolve during the development lifecycle, the effort needed to maintain accurate links increases, driving up maintenance costs and further complicating test management.This study proposes a graph-based approach to establish and maintain traceability throughout the software testing process. By comparing various models for their ability to identify semantic relationships between software requirements and test cases, we selected the most effective method to create accurate traceability links. These links are further utilized through graph queries, enabling efficient analysis of test coverage, identification of untested requirements, and discovery of high-similarity requirement clusters, thereby enhancing the overall testing process. Automatically generating test cases based on query results, our approach seamlessly integrates into the software testing lifecycle, enhancing both coverage and efficiency. In a case study involving real-world industrial data, we effectively identified previously untested requirements and generated a substantial number of high-quality test cases. The results validate the applicability and effectiveness of our approach, demonstrating its potential to improve test traceability and reliability in practical software development environments.

Recently, automated program repair using large language models (LLMs) has attracted growing attention. In the context of Ethereum smart contracts, where addressing vulnerabilities before deployment is essential, several studies have begun exploring LLM-based vulnerability repair. These studies typically evaluate repair methods on publicly available contracts. However, the effectiveness of LLMs in fixing vul-nerabilities in previously unseen contracts remains unclear. To address this question, we applied an obfuscation technique to simulate unknown contracts and used Code Llama - Instruct and GPT-3.S Turbo to attempt automated repairs. We collected 11 publicly available vulnerable contracts and generated obfuscated versions of each to simulate previously unseen contracts. We then evaluated the performance of the LLMs on both sets. Code Llama - Instruct successfully repaired one original contract and four obfuscated ones. In contrast, GPT-3.5 Turbo correctly fixed seven contracts in each group. These results suggest that LLMs are capable of consistently addressing vulnerabilities in both existing and obfuscated (i.e., simulated unknown) contracts.

Testers often need to manually write black-box test cases based on software artifacts such as requirement documents. In agile development, this process is often time-consuming and is further complicated by frequent requirement changes, leading to continuous maintenance overhead. Automating this process is therefore essential. Given the strong natural language understanding and generation capabilities of large language models (LLMs), combined with Retrieval-Augmented Generation (RAG), we propose a RAG-based framework for automated test case generation. Before generation, we embed software artifacts to construct a vectorbased knowledge database. At runtime, software requirements are used as queries to retrieve relevant context, which is integrated into a prompt and passed to the LLM for test case generation. This approach addresses several shortcomings of LLMs, including limited context length, attention dilution over large inputs, and the tendency to hallucinate or over-look key domain-specific constraints. By providing query-specific external knowledge, RAG enhances both accuracy and efficiency. We deploy the framework with different models locally and conduct experiments on two open-source datasets. Compared with the manually written benchmark test cases, our method achieves full requirement coverage with fewer test cases, improved efficiency, reduced error potential, and realized better readability.

This study addresses software bloat, a prevalent issue in modern software development, causing excessive size and complexity due to feature additions and unnecessary functions. Such bloat leads to decreased efficiency, performance degradation, and increased vulnerability. To combat this issue, the concept of software 3R (reduce, reuse, recycle) is proposed; however, accurately reproducing the internal state of black-box software for 3R requires both source code and execution log data, posing practical challenges. In this paper, we conduct a software execution status estimation using limited execution log. Graph Neural Networks (GNNs) are employed for analysis, offering effective processing of graph data. The task is framed as link prediction and node classification, comparing traditional deep learning methods with GNNs using Apache OFBiz ERP software logs. Preliminary results validate GNN applicability.

In order for a system to provide services in any environment, it is expected to establish a technique for constructing a self-adaptive system that can adapt to its environment by changing its own behavior. Real-world systems often have time constraints. While time constraints are involved in safety and usability concerns, the execution time of a system is uncertain due to uncertainties in the external environment, and this uncertainty should be considered when verifying the system. In this paper, we propose a self-adaptive system implementation framework that can handle time constraints and has a dynamic verification function that considers execution time uncertainty. The framework uses UPPAAL-SMC, a statistical model checking tool that can handle time, to represent execution time uncertainty and perform dynamic verification. We evaluate the usefulness of the proposed framework by implementing a simple self-adaptive system using the framework and verifying the system behavior.

In application marketplace platforms like the Google Play Store, reviews left by users on applications play a vital role for developers. By analyzing user reviews, developers identify potential requirements. The goal model is a commonly used model in requirements analysis. Utilizing reviews to generate goal models can help developers comprehensively understand user requirements. However, manually analyzing a large volume of reviews is a time-consuming and labor-intensive task. To address this problem, an automatic method for clustering user reviews and identifying goal models has been proposed. Nevertheless, the goal model generated by this method has poor accuracy, and the goals generated are difficult for developers to understand. To more comprehensively extract requirements from user reviews, we propose a goal model generation method based on large language models (LLMs). The proposed method consists of two parts: first, a Latent Dirichlet Allocation (LDA) model divides user reviews into different topics; second, we use specific prompts and examples to extract requirements and generate goal models. Experiments show that our LLM-based goal model generation method improves the accuracy of goal model generation and identifies more requirements compared to the existing method.

Robotic process automation (RPA) is a technique for automating desktop tasks by developing bots. While RPA enables automatic repetition of tasks, various defects can occur during actual operations. Some defects manifesting as smells in bot codes during the development phase are considered to possess distinct characteristics compared to conventional programs. This study aims to classify these smells in RPA and facilitate their detection. We first categorize RPA smells using code reviews that highlight smells in actual bot development. Based on the categorization, we also develop a preliminary smell detection tool. The categorization result reveals that the most prominent category is substitutable process, highlighting the importance of replacing a sequence of commands with single RPA commands. Experimental results show that the detection tool can find smells with a high degree of accuracy. This high accuracy seems to be attributable to the stronger constraints present in RPA code compared to conventional programming code.

This study aims to solve the problem of selecting a given number of nodes to protect and minimize the impact of the initial failures of unprotected nodes in interdependent networks. We propose a method for quantifying the impact of each node by the Shapley values, a concept from the cooperative game, considering the probability of initial node failures. This method allows us to select the nodes with the highest impact in order. We conducted simulation experiments to evaluate the proposed method.

Designing distributed algorithms is challenging owing to asynchrony and faults. In this study, we formally describe two malicious fault-tolerant consensus algorithms using two languages, PlusCAL and C, and perform model checking on them. We report the observations obtained through this attempt.

Writing a sequential program in an imperative programming language is much easier than writing a distributed algorithm. This paper describes an approach to representing, testing, and verifying distributed algorithms by treating them as sequential programs. This approach allows for the use of testing and verification techniques typically applied to sequential programs.

This study investigated mutation testing for graph database queries. Database queries serve a significant role in many application programs. SQL queries are the most common, but new types of databases and their query languages have emerged and begun gaining popularity. This paper focuses on queries written in Cypher, a language for accessing graph databases. Several mutation operators are proposed, and a tool for generating mutant Cypher queries from a given query is presented.

This study reports the results of model checking of two protocols that control vehicle traffic at intersections. One of the protocols uses a centralized controller that monitors and controls the vehicles at an intersection. The other one is a decentralized protocol in which vehicles communicates with each other with no centralized mechanism. We used the SPIN model checker to verify these protocols. Specifically, we check the safety property that no two vehicles enter the intersection at the same time if their routes are conflicting. As a result, we found a scenario in which the safety property can be violated for the centralized protocol. In addition, for the decentralized protocol, we detected a scenario where vehicles must wait arbitrarily long, which is a liveness error.

Reliability evaluation is imperative for developing safety-critical systems where failures can cause serious consequences. Thus, assuring the correctness of programs that compute reliability is indispensable. However, this is a challenging task when the correct output is not known a prior, since it is impossible to determine whether the calculated reliability is correct or not. To overcome this challenge, we propose the application of metamorphic testing to reliability calculating programs. Metamorphic testing tests software by checking whether particular relations, generally called metamorphic relations, hold or not between multiple inputs and outputs rather than solely focusing on the correctness of independent outputs. Therefore, this testing approach allows software to be tested without known correct outputs. In this study, we focus on programs that compute the reliability of coherent systems from a given set of pathsets. We developed several metamorphic relations, which allowed us to automatically test two programs. To the best of our knowledge, this is the first study where metamorphic testing was applied to reliability calculating software.

Concurrent algorithms are difficult to design correctly. This study focused on mutual exclusion and explored the benefits of employing a formal approach for specifying and verifying concurrent algorithms through case studies. This paper reports the findings and insight obtained from the case studies, including the detection of a design fault in one of the analyzed algorithms.

Self-adaptive systems can adapt to environmental changes by modifying their behavior and require runtime verification after adaptation.More efficient verification mechanisms are required because verification mechanisms such as model checking are computationally and memory intensive.A possible method is to generate expressions for model checking at design time and execute such expressions at runtime.Our previous work proposed a caching mechanism and parameterization to improve the expression generation method.In this study, we improve our previous work by generating expressions using Laplace expansion.This method expands the probabilistic model at the points where it is different from the design model and brings the model closer to a model in a cache for generating expressions.We also propose a method to generate candidate metrices to increase the number of cached matrices and improve the cache hit ratio.We conducted experiments with three types of changes, that is, adding, changing, and deleting states.We observed that our approach is effective when the model's states are added or changed.

Detecting arrays are mathematical structures aimed at fault identification in combinatorial interaction testing. However, they cannot be directly applied to systems that have constraints on the test parameters. These constraints are prevalent in real-world systems. This paper proposes constrained detecting arrays (CDAs), an extension of detecting arrays, which can be used for systems with constraints. The properties and capabilities of CDAs are examined with rigorous arguments. Moreover, two algorithms are proposed for constructing CDAs: one is aimed at generating minimum CDAs, and the other is a heuristic algorithm aimed at fast generation of CDAs. The algorithms were experimentally evaluated using a benchmark dataset. Experimental results show that the first algorithm can generate minimum CDAs if a sufficiently long generation time is allowed, and the second algorithm can generate minimum or near-minimum CDAs in a reasonable time. CDAs extend the range of application of detecting arrays to systems with constraints. The two proposed algorithms have different advantages with respect to array size and generation time.

Self-adaptive systems can decide autonomously to adapt their settings depending on the current situation of their operating environment. To increase their dependability in a dynamic environment, different techniques like evolutionary al-gorithms, artificial intelligence techniques, etc., have been widely used. Recently, machine learning has been leveraged to solve issues like discovering new knowledge at runtime or helping to cope with uncertainty. The adaptation space reduction problem and the interactions with human-in-the-loop problem are among the issues facing self-adaptive systems. In our work we propose a mechanism that can solve the former while contributing to a solution for the latter. The mechanism uses a deep learning approach that leverages explainable AI (XAI) in the process of the learning and predictions. Our approach uses a convolutional neural network (CNN) to implement the deep learning approach and the integrated gradients technique for the explainable AI (XAI). XAI helps to build trust in the system by explaining the predictions and the behavior of the deep learning model. We evaluated our approach on the MAPE-K framework of two simulated Internet of Things systems.

We study the applicability of graph queries to the coverage analysis of test cases for requirements specifications.First we show that when the similarity degrees between requirements specifications and test cases are available, they can be represented in the form of a graph.Then we identify several queries that are useful for extracting coverage information and show that all these queries can be written in the Cypher query language, a common graph query language.In a case study we apply these queries to data obtained from a real-world project in industry.The results of the case study show that coverage information can be retrieved in reasonable time.We also compare the graph queries with SQL queries with respect to conciseness and processing time.

Constrained Covering Arrays (CCAs) and Constrained Detecting Arrays (CDAs) are mathematical objects used as test suites in Combinatorial Interaction Testing (CIT). CCAs are able to detect faults in systems from the test results, while CDAs can not only detect faults but also locate them. In spite of this added value of CDAs, the existing algorithm for generating CDAs does not scale well, being hardly able to handle even moderate-size problems. In this paper, we propose a heuristic algorithm for faster CDA generation. We prove a property that relates CCAs and CDAs and design the algorithm by making use of it. Specifically, the algorithm first generates a CCA and then transforms the CCA to a CDA based on this property. Experimental results show that the new algorithm can solve much larger problems than can the existing algorithm.

Combinatorial interaction testing is an efficient software testing strategy. If all interactions among test parameters or factors needed to be covered, the size of a required test suite would be prohibitively large. In contrast, this strategy only requires covering t-wise interactions where t is ty pically very small. As a result, it becomes possible to significantly reduce test suite size. Locating arrays aim to enhance the ability of combinatorial interaction testing. In particular, (1¯,t) -locating arrays can not only execute all t-way interactions but also identify, if any, which of the interactions causes a failure. In spite of this useful property, there is only limited research either on how to generate locating arrays or on their minimum sizes. In this paper, we propose an approach to generating minimum locating arrays. In the approach, the problem of finding a locating array consisting of N tests is represented as a Constraint Satisfaction Problem (CSP) instance, which is in turn solved by a modern CSP solver. The results of using the proposed approach reveal many (1¯,t) -locating arrays that are smallest known so far. In addition, some of these arrays are proved to be minimum.

Combinatorial interaction testing is known to be an efficient testing strategy for computing and information systems. Locating arrays are mathematical objects that are useful for this testing strategy, as they can be used as a test suite that permits fault localization as well as fault detection. In this application, each row of an array is used as an individual test. This paper proposes an algorithm for constructing locating arrays with a small number of rows. Testing cost increases as the number of tests increases; thus the problem of finding locating arrays of small sizes is of practical importance. The proposed algorithm uses simulated annealing, a meta-heuristic algorithm, to find locating array of a given size. The whole algorithm repeatedly executes the simulated annealing algorithm with the input array size being dynamically varied. Experimental results show (1) that the proposed algorithm is able to construct locating arrays for problem instances of large sizes and (2) that, for problem instances for which nontrivial locating arrays are known, the algorithm is often able to generate locating arrays that are smaller than or at least equal to the known arrays. Based on the results, we conclude that the proposed algorithm can produce small locating arrays and scale to practical problems.

This paper introduces the notion of Constrained Locating Arrays (CLAs), mathematical objects which can be used for fault localization in software testing. CLAs extend ordinary locating arrays to make them applicable to testing of systems that have constraints on test parameters. Such constraints are common in real-world systems; thus CLA enhances the applicability of locating arrays to practical testing problems. The paper also proposes an algorithm for constructing CLAs. Experimental results show that the proposed algorithm scales to problems of practical sizes.

This paper proposes a Boolean satisfiability (SAT)-based approach to the analysis of cascading failures in systems of interdependent networks. Typical examples of such systems are power systems, where a power transmission network and a SCADA (Supervisory Control And Data Acquisition) network are dependent on each other. The proposed approach reduces the problem of analyzing cascading failures to the SAT problem by constructing Boolean formulas that symbolically represent all possible failure scenarios under given conditions. This allows us to examine a numerous number of scenarios by means of fast modern SAT solvers. The results of experiments show that the proposed approach can deal with practical size systems, such as the IEEE 39 bus system, which ordinary approaches fail to handle.

Secure wireless routing protocols which use an authentication mechanism, such as digital signatures, prevent attacks whereby an attacker injects fake data in the route information in the process of establishing a route. In this paper, we focus on a multi-hop secure routing protocol called ISDSR, which is a secure variant of DSR with ID-based sequential aggregate signatures. ISDSR guarantees the correctness of route information that contains a collection of nodes that constitute a travel path of a received packet. Analytic results on the performance of this protocol were provided in previous work; but the performance in a practical situation has not been investigated so far. In this work, we present the results of our experiments using two types of emulation environments where the network are formed with nine to 100 nodes. The results show that ISDSR is superior to the RSA-based secure routing protocol with respect to packet loss rate.

Self-adaptive software systems change their behaviors to adapt to their environmental changes at runtime. Runtime verification, which checks the correctness of behaviors after adaptation, sometimes uses probabilistic model checking, because the verification has to deal with uncertainty. However, since probabilistic model checking is usually computation intensive and time consuming, a more efficient verification mechanism is desired. A possible approach is to pre-generate some expressions for model checking at design time and execute model checking simply by evaluating the expressions at runtime. A problem with this approach is that when environmental changes require changes of the system model, these expressions need to be re-generated at runtime. In order to cope with such significant changes, we develop a caching mechanism that reduces computational time at runtime. We also introduce a parameterization technique in order to improve the efficiency of caching. The experimental results show that our new implementation of the caching mechanism greatly improves the computational time of runtime verification.

Embedded systems that realize specific functions are usually hardware constrained systems running dedicated software. These embedded systems rarely take into account the possibility to change functions after their release. As a result, it would be difficult to change some function from outside an embedded system in its operational environment. In order to keep up with the need of quickly reacting to changes affecting requirements and environments, it is paramount to find a way to update the functions of these systems. We constructed a programming framework for updating functions based on the MAPE loop mechanism, which is generally used to develop self-adaptive systems. We regard MAPE loop as a set of independent components that make it easy to separate the updating functions from other functions. We apply our framework to a web application and an embedded system. The proposed framework is independent of the target embedded system and makes it possible to easily inject new functions into it.

Combinatorial Interaction Testing (CIT) is a well practiced strategy for testing of software systems. Ordinary CIT detects faults caused by interactions of parameters but cannot locate faulty interactions. This paper addresses the problem of adding fault localization capability to CIT. This is done by means of fault locating suites of test cases, which are named constrained locating arrays. An algorithm that derives a constrained locating array from a test suite for ordinary CIT is proposed. Experimental results show that the new algorithm can construct constrained locating arrays for fairly large sized problem instances in reasonable time.

Metamorphic testing has been advocated as a possible approach to testing of systems that have no useful test oracles; but it has not often been applied in practice. Here we report some of the results of applying metamorphic testing to real-world e-commerce product search engines.

Application users can submit reviews for downloaded applications.Recently, developers have received more and more user reviews.However, it is still difficult to extract beneficial comments from a large amount of reviews.Latent Dirichlet Allocation (LDA) is a promising way of topic modeling, which classifies documents according to implicit multiple topics.However, there is a gap between the documents that the developer wants to extract and the document extracted by LDA.In this paper, we propose a method to extract documents of each category, such as requirements descriptions or bug reports, more accurately.Our method first decomposes the topics.Then, the method uses the keyword list which is a set of semantically similar words collected by word2vec, to integrate the decomposed topics.We apply our method to the applications user reviews in Apple Store and demonstrate the validity of it.Our approach can help application developers to extract beneficial information.

Efficient software testing requires precise test space definition.To determine the test space, constraint elicitation is one of the important processes in a test design; however, the process usually requires manual capturing and precise definition of constraints.We have developed a constraint elicitation process that helps to define constraints from documents relevant to the test model.In this paper, we propose a refined metric that finds parameter combinations to be extracted more precisely.This metric determines the parameter correlation on the basis of word co-occurrences in the specification document.We conduct experiments on some test models and demonstrate that our metric allows us to find parameter combinations that form constraints with a high recall rate.

Pair-wise testing is a widely used strategy of software testing. It requires testing every pair of parameter values at least once. This paper focuses weighting of parameter values for this testing strategy. Weighting is an added feature which allows the tester to prioritize different parameter values by specifying their desired frequency of occurrence in a test suite. This feature is desirable as it allows the tester to have more control over the resulting test suite. However, there has been not much research on weighting: to our knowledge, all existing weighting methods treat weights as a second class requirement and cannot generate a test suite that sufficiently respects the given weights. Aiming to overcome this problem, this paper proposes a weighting method which can be used in combination of any one-test-at-a-time greedy test case generation algorithm. By comparing the parameter value distribution in the current test suite and the ideal one specified by the given weights, the method generates each test case so that the resulting test suite can reflect the weights as accurately as possible. The usefulness of the method is demonstrated through empirical results.

Parallel and distributed algorithms, including those for fault tolerance, often use timestamps to coordinate the behaviors of processes. These algorithms are hard to correctly design and often subject to subtle design faults. Model checking, which is a state exploration-based verification method, has been very successful in finding design faults in many practical systems. However model checking of timestamp-based algorithms is difficult when the values of timestamps are not bounded, because then the state space is infinite. This paper addresses the problem of infinite state space by proposing a data abstraction technique for timestamps. This technique transforms the infinite-state algorithm to a finite-state abstract model which simulates the original algorithm. The applicability of this approach is demonstrated through a case study where Lamport's bakery algorithm is verified in the absence and presence of process failures.

Combinatorial interaction testing is a well practiced method for detecting faults for various computing systems. This method requires that any t-wise parameter interactions must be exercised by at least one test case. The value of t is usually referred to as strength. A large body of research exists about constructing test suites of small or moderate strength, typically t = 2 or 3; but very few techniques are known for constructing those of very high strength. This paper proposes the use of ZDD-based graph algorithms to construct a very high strength combinatorial test suite. Constructing high strength test suites is challenging because of the large number of interactions that must be handled during test suite construction. A ZDD is a data structure that can be used to enumerate a very large number of paths in an undirected graph and to perform operations on large sets of graphs. In our approach test cases and interactions are represented as subgraphs of the same graph. Using a ZDDbased graph library to operate on the graphs, we succeeded in constructing test suites of high strength up to t = 11 for some problem instances.

Feedback comments, such as mailing lists and reviews, contain beneficial suggestion for software developers.Recently, developers have received more and more feedback comments; but it is still difficult to extract beneficial comments from a large amount of e-mail message or reviews.Latent Dirichlet Allocation (LDA) is a promising way of topic modeling, which classifies documents according to implicit multiple topics.In this paper, we tried to apply a requirements elicitation based on LDA to two different sources, i.e., Apache Commons User List and App Store reviews, and discuss the feasibility of this approach.An interesting finding was that some usual stop words indicated requirements description.This suggests that these words should be removed from the stop word list before applying LDA.

This article discusses the location of faulty interactions in software testing. We propose an algorithm to generate a test suite that can be used to identify a faulty pair-wise interaction. This approach works as follows. First, a test suite is generated using an existing method for pair-wise testing. Pair-wise testing requires testing all pair-wise interactions but does not guarantee that the faulty interaction can be located. Second, pair-wise interactions that cannot be located by the test suite are enumerated. Finally, test cases are repeatedly added to the test suite until all pair-wise interactions can be located. The results of applying the algorithm to several problem instances show that the test suites obtained using the algorithm are nearly twice as large as those for ordinary pair-wise testing which does not ensure fault locating ability.

In this paper, we propose a weighting method for pair-wise testing. Pair-wise testing is a software testing strategy that tests every pair of parameter values at least once. Weighting allows the tester to specify desired frequency of occurrence in a test suite for each parameter value. Pair-wise testing is a widely used strategy because of its effectiveness in finding faults in software. Weighting makes this strategy more effective by allowing the tester to have more control over the resulting test suite. However, there is not much research on weighting. To our knowledge, all existing weighting methods treat weights as a second class requirement and cannot generate a test suite that sufficiently respects the given weights. The proposed method aims to overcome the problem. By taking into consideration the parameter value distribution in the current test suite and the ideal one specified by the given weights, the method generates each test case so that the resulting test suite can reflect the weights as accurately as possible. We implement the method in our testing tool and show some results to demonstrate how accurately test suites generated by this tool satisfy given weights.

Decentralized train control is ideal in that by distributing computation load over multiple cars, it allows extensibility to, for example, newly installed modules. Besides, compared to centralized control, the delay occurring in cooperative control over multiple devices can be significantly reduced. A technical challenge here is that the legacy software program has a monolithic structure and thus is not amenable to distributed execution. In this paper we present our attempt to tackle this challenge. In the attempt we proceed in two steps. First, we perform a reconstruction of the architecture of the control software. Specifically we decompose the existing software system into several modules that perform independent functions. Second, we devise a mechanism that can manage distributed execution of these modules. A timeliness analysis shows that the new architecture can accommodate addition of new features that the existing architecture could not perform without violating real-time deadlines.

We address the issue of maximization of the availability of replicated data that are distributed in a wide area network. We consider a system that uses majority voting, which is a common mechanism for providing consistency of replicated data in the presence of failures. The data availability provided by this mechanism critically depends on the vote assignment to the replicas. In this paper we formulate the problem of finding the optimal vote assignment into a specific form of a combinatorial optimization problem, namely the MAX-SMT problem. This formulation allows us to use a modern, fast MAX-SMT solver to solve the vote assignment problem. To evaluate the effectiveness of this approach, we build a failure repair model of underlying networks and estimate the data availability using that model. The results of the estimation show that data availability can be significantly improved using the optimal vote assignment in the presence of failures.

This paper proposes a model checking-based approach to verification of asynchronous consensus algorithms, an important class of distributed fault-tolerant algorithms. The proposed approach can be used to verify these algorithms against agreement, which is the key safety property of this class of algorithms. A consensus algorithm typically has runs of unbounded length and unbounded queues or sets of messages in transit, thus its state space is often infinite. This property makes application of model checking difficult, because model checking is based on state space exploration. Our approach can limit the use of model checking to a single round of an algorithm, by using a finite state model that over approximates the behavior of any single round. As a result, the problem of infinite state spaces can be circumvented. In case studies, two consensus algorithms are verified using this approach.

We consider the problem of finding an allocation of program modules to computing nodes in a network. The objective of this problem is to maximize the probability of successfully executing these modules. Nodes and links of the network are assumed to be subject to failures. We propose an algorithm for this problem which uses Binary Decision Diagrams (BDDs) extensively. BDDs have been used as a powerful means for reliability evaluation. In this paper we show that BDDs are also useful for reliability optimization. Through experiments, we show that the intensive use of BDD operations leads to a significant saving of computation time.

Gossip is a scalable and easy-to-deploy broadcast method for distributed systems. In gossip a broadcast message is disseminated through repeated information exchanges between randomly chosen nodes. Gossip can also achieve high reliability using a large amount of redundant messages, but this also incurs high load on the network. This paper proposes a new gossip algorithm which incorporates network coding techniques to mitigate the high load. With random linear coding, each message propagated in the new algorithm is randomly generated from the broadcast message. Unlike in ordinary gossip, this feature prevents nodes from receiving an identical message more than once, allowing to achieve the same reliability at a lower message cost.

Triple modular redundancy (TMR) is a well-known technique for building fault-tolerant systems. In TMR, a module unit is triplicated, and the outputs of these three units are compared by a voter. In this paper we consider systems that consist of multiple TMR units in series. Only recently has it been found that even such simple systems can be configured into various structures. We propose (i) a method of calculating the reliability of cascaded TMR systems and (ii) an algorithm for finding a structure that maximizes reliability. The algorithm uses the branch and bound search algorithm, where candidate solutions are evaluated by means of the proposed reliability calculation method. We also show that some new structures have optimal reliability within some ranges of voter and module reliability.

This paper presents an approach to facilitating model checking of consensus protocols, a class of distributed protocols. Model checking is a successful formal verification method. However its application to these protocols is still not a common practice because of the following problems. First, model checking requires non-negligible users' efforts in representing the protocol under verification in the input language of a model checker. Second, these protocols usually induce an infinite state space, making model checking infeasible. To alleviate these problems, the proposed approach provides (i) a language for concisely describing consensus protocols and (ii) a translator from the proposed language to a mathematical formula that symbolically represents the entire behavior of the protocol. Once the formula is generated, one can model check the protocol by checking the satisfiability of the formula with a satisfiability modulo theories (SMT) solver. Several case studies demonstrate the usefulness of the proposed approach both in correctness proving and bug hunting.

Testing is essential to ensure the dependability of software systems. This paper proposes an automatic test case generation method using the NuSMV model checker. We consider state-transition testing based on Statechart specifications. Given a Statechart specification, our proposed method can automatically generate test cases that cover all states or all transitions in the Statechart. Finding such test cases requires traversing the state space of the system under test. In practice, however, the state space can often be very large and thus a fast search method is required. To this end our method makes full use of NuSMV. We devise a technique for modeling and analyzing Statecharts so that test cases can be extracted from the counterexamples produced by the model checker. The feasibility of our method is demonstrated through case studies.

We consider systems comprised of multiple triple modular redundancy (TMR) units in series. Only recently have researchers found that even such simple systems can be configured into various structures. We develop an algorithm for finding a structure that maximizes reliability. Using this algorithm we show that new structures have optimal reliability within some ranges of voter and module reliability.

Model checking is a successful formal verification technique; however, its application to fault-tolerant distributed algorithms is still not common practice. One major reason for this is that model checking requires non-negligible users¿ efforts in representing the algorithm to be verified in the input language of a model checker. To alleviate this problem we propose an approach which encompasses (i) a language for concisely describing fault-tolerant distributed algorithms and (ii) a translator from the proposed language to PROMELA, the input language of the SPIN model checker. To demonstrate the feasibility of our approach, we show the results of an experiment where we described and verified several algorithms for consensus, a well-known distributed agreement problem.

In overlay networks, which are virtual networks for P2P applications, topology mismatching is known as a serious problem to be solved. So far several distributed algorithms have been proposed to reduce link cost caused by this problem. However, they often create long routes with a large number of hops, especially for long distance communications. In this paper, we propose a distributed algorithm to address this issue. This algorithm designates nodes in an overlay network as special nodes with some probability. A special node iteratively exchanges one of its links with a new, longer distance link, instead of a shorter one. The new links are extensively used for long distance communications. The simulation studies show that in the overlay networks constructed by this algorithm, the number of hops per route is reduced for long distance communications, at the cost of a slight increase in link cost.

Consensus is one of the most fundamental problems in fault-tolerant distributed computing. This paper proposes a mechanical method for analyzing the condition that allows one to solve consensus. Specifically, we model check a distributed algorithm that implements a communication predicate, which is an alternative system abstraction to failure detectors. This model checking problem is challenging because it involves both continuous time and unbounded integers. We solve the problem by reducing it to the satisfiability problem of linear arithmetic constraints over real and integer variables. The proposed method can be used to determine the length of a synchronous period required for implementing a communication predicate for solving consensus.

We show for the first time that standard model checking allows one to completely verify asynchronous algorithms for solving consensus, a fundamental problem in fault-tolerant distributed computing. Model checking is a powerful verification methodology based on state exploration. However it has rarely been applied to consensus algorithms, because these algorithms induce huge, often infinite state spaces. Here we focus on consensus algorithms based on the Heard-Of model, a new computation model for distributed computing. By making use of the high abstraction level provided by this computation model and by devising a finite representation of unbounded timestamps, we develop a methodology for verifying consensus algorithms in every possible state by model checking.

This paper presents a framework to specify and verify integrated services of a home network system (HNS). We first develop a modeling language to describe the HNS and the integrated services. Complementing our previous work, the language captures each appliance as an object consisting of properties and methods, encapsulating the underlying protocols and platforms. We then present a method that verifies the integrated services with symbolic model checking, by translating the proposed language into the SMV (symbolic model verifier) language. Thus, it is possible to validate if the integrated service is specified as intended, automatically and exhaustively. Using the proposed framework, service developers can effectively detect design flaws in a single integrated service, as well as feature interactions among multiple services, in early stages of service development.

This paper proposes a self-organizing technique for enhancing the coverage of wireless micro-sensor networks after an initial random placement of sensors. A randomized back-off delay time is introduced to resolve the problem of simultaneous movement of sensors in the neighborhood which leads to unnecessary excessive movement and hence consume more sensors' energy. A sensor node relocates itself when the time calculated through randomized back-off delay computation is reached. The new location of the sensor is determined by a virtual force-directed algorithm where virtual attractive or repulsive forces exerted by other sensors or obstacles are used to guide the sensor to the desired location. The proposed self-organizing algorithm for sensor placement is proved to be effective through simulation.

Combinatorial testing is a specification-based testing criterion, which requires that for each t-way combination of input parameters of a system, every combination of valid values of these t parameters be covered by at least one test case. This approach is motivated by the observation that in many applications a significant number of faults are caused by interactions of a smaller number of parameters. We propose new test generation algorithms for combinatorial testing based on two artificial life techniques: a genetic algorithm (GA) and an ant colony algorithm (ACA). The usefulness of these algorithms is demonstrated through experiments. In the case t = 3 in particular, our algorithms exhibited impressive results.

Gossip-based multicast schemes have attracted increasing interest, because they are easy to deploy and resilient to failures. However, traditional gossip-based protocols rely on each process having knowledge of the global membership, thus limiting their scalability. To overcome this problem several protocols have been developed that can operate with processes having only a partial view of the global membership. We discuss the effects of partial views on the reliability of gossip-based multicast protocols. Specifically, we identify three desirable properties for views and show constructions of views satisfying these properties. Numerical results obtained show that reliability can be considerably affected by views adopted, especially in the presence of faulty processes.

Feature interaction is a kind of inconsistent conflict between multiple communication services and considered an obstacle to developing reliable telephony systems. In this paper we present an automatic method for detecting feature interactions in service specifications. This method uses bounded model checking, a SAT-based automatic verification technique.

Testing is a crucial part of the development of software systems. In this paper, we consider testing of an implementation that is intended to satisfy a Boolean formula. In the literature, specification-based testing has been suggested for this purpose. Typically, such methods first hypothesize a fault class and then generate tests. However, there is almost no research that justifies fault classes proposed previously. Moreover, specifications amenable to automatic test generation are not always available to testers in practice. Based on these observations, we examine the applicability of non-specification-based approaches, which need no specification in the form of a Boolean formula to create tests. We compare a specification-based approach to three non-specification-based approaches, namely, random testing, antirandom testing, and combinatorial testing. The results of an experiment show that combinatorial testing is often comparative to specification-based testing and is superior to both random testing and antirandom testing.

In a previous paper, Kuhn [1999] showed that faults in Boolean specifications constitute a hierarchy with respect to detectability, and drew the conclusion that missing condition faults should be hypothesized to generate tests. However this conclusion was premature, since the relationships between missing condition faults and faults in other classes have not been sufficiently analyzed. In this note, we investigate such relationships, aiming to complement the work of Kuhn. As a result, we obtain an extended hierarchy of fault classes and reach a different conclusion.

Testing is a crucial part of the development of highly dependable systems. In this paper, we consider the testing of an implementation that is intended to satisfy a Boolean formula. In the literature, specification-based testing has been suggested for this purpose. Typically, such methods first hypothesise a fault class and then generate tests. However, there is almost no research that justifies the fault classes proposed previously. Moreover, the specifications available for automatic test generation are not always available to testers in practice. Based on these observations, we examine the applicability of non-specification-based approaches, which need no specification in the form of a Boolean formula to create tests. We compare a specification-based approach to two non-specification-based approaches, namely random testing and combinatorial testing, which is an emerging technique based on combinatorial designs. The results of an experiment show that combinatorial testing is often comparative to specification-based testing and is always much superior to random testing.

Model checking is a technique that can make a verification for finite state systems absolutely automatic. We propose a method for automatic verification of fault-tolerant systems using this technique. Unlike other related work, which is tailored to specific systems, we are aimed at providing a general approach to verification of fault tolerance. The main obstacle in model checking is state explosion. To avoid the problem, we design this method so that it can use SMV, a symbolic model checking tool. Symbolic model checking can overcome the problem by expressing the state space and the transition relation by Boolean functions. Assuming that a system to be verified is specified by guarded commands, we define a modeling language suited for describing guarded command programs and propose a translation method from the modeling language to the input language of SMV. We show the results of applying the proposed method to various examples to demonstrate the usefulness.

A distributed system is said to be self-stabilizing if it converges to safe states regardless of its initial state. In this paper we present our results of using symbolic model checking to verify distributed algorithms against the self-stabilizing property. In general, the most difficult problem with model checking is state explosion; it is especially serious in verifying the self-stabilizing property, since it requires the examination of all possible initial states. So far applying model checking to self-stabilizing algorithms has not been successful due to the problem of state explosion. In order to overcome this difficulty, we propose to use symbolic model checking for this purpose. Symbolic model checking is a verification method which uses Ordered Binary Decision Diagrams (OBDDs) to compactly represent state spaces. Unlike other model checking techniques, this method has the advantage that most of its computations do not depend on the initial states. We show how to verify the correctness of algorithms by means of SMV, a well-known symbolic model checker. By applying the proposed approach to several algorithms in the literature, we demonstrate empirically that the state spaces of self-stabilizing algorithms can be represented by OBDDs very efficiently. Through these case studies, we also demonstrate the usefulness of the proposed approach in detecting errors.

Proposes new scheduling algorithms to achieve fault security in multiprocessor systems. We consider the scheduling of parallel programs represented by directed acyclic graphs with arbitrary computation and communication costs. A schedule is said to be 1-fault-secure if the system either produces correct output for a parallel program or it detects the presence of any single fault in the system. Although several 1-fault-secure scheduling algorithms have been proposed so far, they can all only be applied to a class of tree-structured task graphs with a uniform computation cost. In contrast, the proposed algorithms can generate a 1-fault-secure schedule for any given task graph with arbitrary computation costs. Applying the new algorithms to two kinds of practical task graphs (Gaussian elimination and LU-decomposition), we conduct simulations. Experimental results show that the proposed algorithms achieves 1-fault security at the cost of a small increase in schedule length.

The use of quorums is a well-known approach to achieving mutual exclusion in distributed environments. In this paper, we propose a new availability evaluation method for quorum-based mutual exclusion schemes in the presence of failures. Most of the previously proposed methods take neither the topology of systems nor link failures into consideration, and exhaustive state enumeration has been the only approach that can deal with them so far. By incorporating a notion called Minimal Quorum Spanning Trees, this method can efficiently evaluate the availability of quorum-based mutual exclusion schemes in general topology networks with unreliable nodes and links. Through experimental results, we show the superiority of the proposed method over exhaustive state enumeration.

The use of quorums is a well-known approach to achieving mutual exclusion in distributed computing systems. This approach works based on a coterie, a special set of node groups where any pair of the node groups shares at least one common node. Each node group in a coterie is called a quorum. Mutual exclusion is ensured by imposing that a node gets consensus from all nodes in at least one of the quorums before it enters a critical section. In a quorum-based mutual exclusion scheme, the delay for reaching consensus depends critically on the coterie adopted and, thus, it is important to find a coterie with small delay. Fu (1997) introduced two related measures called max-delay and mean-delay. The former measure represents the largest delay among all nodes, while the latter is the arithmetic mean of the delays. She proposed polynomial-time algorithms for finding max-delay and mean-delay optimal coteries when the network topology is a tree or a ring. In this paper, we first propose a polynomial-time algorithm for finding max-delay optimal coteries and, then, modify the algorithm so as to reduce the mean-delay of generated coteries. Unlike the previous algorithms, the proposed algorithms can be applied to systems with arbitrary topology.

We propose a new scheduling algorithm for achieving fault tolerance in multiprocessor systems. The new algorithm partitions a parallel program into subsets of tasks based on some characteristics of a task graph. Then for each subset, the algorithm duplicates and schedules its tasks successively. Applying the proposed algorithm to three kinds of practical task graphs (Gaussian elimination, Laplace equation solver and LU decomposition), we conduct simulations. Experimental results show that fault tolerance can be achieved at the cost of a small degree of time redundancy, and that performance in the case of a processor failure is improved compared to a previous algorithm.

This paper discusses safety analysis of design documents constructed by object-oriented development approaches. In our previously proposed method, whether design documents satisfy safety requirements is checked using some information tables, and these safety requirements are assumed to be given in advance. However, any systematic method that can derive such safety requirements from requirements specification and safety standards has not been developed. To overcome this problem, we propose a new FTA (Fault Tree Analysis)-based technique to derive safety requirements from requirements specification, component library, and design documents. Then, we apply the proposed method to typical examples taken from previous reports.