We propose a lightweight scheme for fault diagnosis in time-triggered (TT) systems. An existing scheme is preferable in its capability but incurs computation time that can be prohibitively large for some real-time systems, such as automotive control systems. Our proposed scheme, which we call voting sharing, can substantially reduce the computation time by sharing the diagnosis result obtained by each node with all nodes in the system. We clarify the properties of the voting sharing scheme with respect to fault tolerance and show some experimental results.

A Peer-To-Peer (P2P) application uses an overlay network which is a virtual network constructed over the physical network. Traditional overlay construction methods do not take physical location of nodes into consideration, resulting in a large amount of redundant traffic. Some proximity-aware construction methods have been proposed to address this problem. These methods typically connect nearby nodes in the physical network. However, as the number of nodes increases, the path length of a route between two distant nodes rapidly increases. To alleviate this problem, we propose a technique which can be incorporated in existing overlay construction methods. The idea behind this technique is to employ long links to directly connect distant nodes. Through simulation experiments, we show that using our proposed technique, networks can achieve small path length and low communication cost while maintaining high resiliency to failures.

This letter discusses the applicability of boolean satisfiability (SAT) solving to pairwise testing in practice. Due to its recent rapid advance, using SAT solving seems a promising approach for search-based testing and indeed has already been practiced in test generation for pairwise testing. The previous approaches use SAT solving either for finding a small test set in the absence of parameter constraints or handling constraints, but not for both. This letter proposes an approach that uses a SAT solver for constructing a test set for pairwise testing in the presence of parameter constraints. This allows us to make full use of SAT solving for pairwise testing in practice.

We propose a two-level hierarchical method for dependability evaluation of distributed systems with replicated programs and data files. Since Markov modeling is limited only to each component in this method, state explosion can be circumvented successfully. Simulation results show that the method can accomplish evaluation even for large systems for which Markov modeling is not feasible.

Pair-wise testing is an effective test planning technique for finding interaction faults using a small set of test cases. Constraint elicitation is an important process in the pair-wise testing design since constraints determine the test space; however, the constraint elicitation process has not been well studied. It usually requires manual capturing and precise definition of constraints. In this paper, we propose a constraint elicitation process that helps combinatorial test design. Our elicitation process consists of two steps: parameter combination identification and value pair determination. We conduct experiments on some test models, and demonstrate that some extracted rules match constraints and others helps to define constraints.

This letter proposes a broadcast scheme for use in ad hoc networks using variable-range transmission power. Preserving energy and ensuring a high delivery ratio of broadcast packets are crucial tasks for broadcasting in ad hoc networks. Using individual broadcast relaying nodes to dynamically vary the transmission range can help saving power and reduce interference during communication. We analyzed the performance of the proposed scheme and compared it to other prevalent broadcast schemes for wireless ad hoc networks based on common-range transmission power.

Feature interaction is the term used in telephony systems to refer to inconsistent conflict between multiple communication services. Feature interaction is considered a major obstacle to developing reliable telephony systems and many approaches have been explored to resolve it. In this paper we present an automatic method for detecting latent feature interaction in service specifications. This method uses bounded model checking as its basis. The basic idea behind bounded model checking is to reduce the detection problem to the propositional satisfiability (SAT) decision problem. For asynchronous systems like telecommunication systems, however, traditional bounded model checking does not work well because resulting propositional formulas tend to become very large. We propose a new encoding scheme to overcome this problem and show the effectiveness through comparative experiments with traditional bounded model checking and other model checking methods.

A schedule for a parallel program is said to be 1-fault-secure if a system that uses the schedule can either produce correct output for the program or detect the presence of any faults in a single processor. Although several fault-secure scheduling algorithms have been proposed, they can all only be applied to a class of tree-structured task graphs with a uniform computation cost. Besides, they assume a stringent error model, called the redeemable error model, that considers extremely unlikely cases. In this paper, we first propose two new plausible error models which restrict the manner of error propagation. Then we present three fault-secure scheduling algorithms, one for each of the three models. Unlike previous algorithms, the proposed algorithms can deal with any task graphs with arbitrary computation and communication costs. Through experiments, we evaluate these algorithms and study the impact of the error models on the lengths of fault-secure schedules.

Goal modeling is a method that describes requirements structurally. Goal modeling mainly consists of two tasks: extraction of goals and organization of the extracted goals. Generally, the process of the goal modeling requires intensive manual intervention and higher modeling skills than the process of the usual requirements description. In order to mitigate this problem, we propose a method that provides systematic supports for constructing goal models. In the method, the requirement analyst answers questions and a goal model is semi-automatically constructed based on the answers made. We develop a prototype tool that implements the proposed method and apply it to two systems. The results demonstrate the feasibility of the method.

In this paper, we propose a new scheduling algorithm to achieve fault tolerance in multiprocessor systems. This algorithm first partitions a parallel program into subsets of tasks, based on the notion of height of a task graph. For each subset, the algorithm then duplicates and schedules the tasks in the subset successively. We prove that schedules obtained by the proposed algorithm can tolerate a single processor failure and show that the computational complexity of the algorithm is O(|V|4) where V is the set of nodes of a task graph. We conduct simulations by applying the algorithm to two kinds of practical task graphs (Gaussian elimination and LU-decomposition). The results of this experiment show that fault tolerance can be achieved at the cost of small degree of time redundancy, and that performance in the case of a processor failure is improved compared to a previous algorithm.

In interdependent systems, such as electric power systems, entities or components mutually depend on each other. Due to these interdependencies, a small number of initial failures can propagate throughout the system, resulting in catastrophic system failures. This paper addresses the problem of finding the set of entities whose failures will have the worst effects on the system. To this end, a two-phase algorithm is developed. In the first phase, the tight bound on failure propagation steps is computed using a Boolean Satisfiablility (SAT) solver. In the second phase, the problem is formulated as an Integer Linear Programming (ILP) problem using the obtained step bound and solved with an ILP solver. Experimental results show that the algorithm scales to large problem instances and outperforms a single-phase algorithm that uses a loose step bound.

The distributed program reliability (DPR) is a useful measure for reliability evaluation of distributed systems. In previous methods, a two-mode failure model (working or failed) is assumed for each computing node. However, this assumption is not realistic because data transfer may be possible by way of a computing node even when this node can neither execute programs nor handle its data files. In this paper, we define a new three-mode failure model for representing such a degraded operational state of computing nodes, and present a simple and efficient analysis method based on graph theory. In order to represent the degraded operational state, a given graph expressing a distributed system is augmented by adding new edges and vertices. By traversing this augmented graph, the reliability measure can be computed. Examples show the clear difference between the results of our proposed method and those of the previous ones.

The exact time complexity of Hsu and Huan's self-stabilizing maximal matching algorithm is provided. It is n2 + n - 2 if the number of nodes n is even and n2 + n - if n is odd.

Probabilistic model checking is an emerging verification technology for probabilistic analysis. Its use has been started not only in computer science but also in interdisciplinary fields. In this paper, we show that probabilistic model checking allows one to analyze the magnetic behaviors of the one-dimensional Ising model, which describes physical phenomena of magnets. The Ising model consists of elementary objects called spins and its dynamics is often represented as the Metropolis method. To analyze the Ising model with probabilistic model checking, we build Discrete Time Markov Chain (DTMC) models that represent the behavior of the Ising model. Two representative physical quantities, i.e., energy and magnetization, are focused on. To assess these quantities using model checking, we devise formulas in Probabilistic real time Computation Tree Logic (PCTL) that represent the quantities. To demonstrate the feasibility of the proposed approach, we show the results of an experiment using the PRISM model checker.

The k-mutual exclusion problem is the problem of guaranteeing that no more than k computing nodes enter a critical section simultaneously. The use of a k-coterie, which is a special set of node groups, is known as a robust approach to this problem. In general, k-coteries are classified as either dominated or nondominated, and a mutual exclusion mechanism has maximal availability when it employs a nondominated k-coterie. In this paper, we propose two new schemes called VOT and D-VOT for constructing nondominated k-coteries. We conduct a comparative evaluation of the proposed schemes and well-known previous schemes. The results clearly show the superiority of the proposed schemes.

The SDP (Sum of Disjoint Products) approach is a well-known technique for computing network reliability measures. So far several algorithms have been developed based on this approach. In this letter, we present a general framework for parallelization of these SDP algorithms. Based on the framework, we implemented a parallel version of an SDP algorithm called CAREL on a network of workstations. Experimental results show that it works fairly well with almost linear speedups.

2-Factor covering designs, a type of combinatorial designs, have recently received attention since they have industrial applications including software testing. For these applications, even a small reduction on the size of a design is significant, because it directly leads to the reduction of testing cost. In this letter, we report ten new designs that we constructed, which improve on the previously best known results.

In this letter we give a lower bound on the worst-case time complexity of Dijkstra's three-state mutual exclusion algorithm by specifying a concrete behavior of the algorithm. We also show that our result is more accurate than the known best bound.

A distributed system is said to be self-stabilizing if it converges to some legitimate state from an arbitrary state in a finite number of steps. The number of steps required for convergence is usually referred to as the stabilization time, and its reduction is one of the main performance issues in the design of self-stabilizing systems. In this paper, we propose an automated method for computing the stabilization time. The method uses Boolean functions to represent the state space in order to assuage the state explosion problem, and computes the stabilization time by manipulating the Boolean functions. To demonstrate the usefulness of the method, we apply it to the analysis of existing self-stabilizing algorithms. The results show that the method can perform stabilization time analysis very fast, even when an underlying state space is very huge.