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.

This paper discusses the collection of sensor data for power distribution systems. In current power distribution systems, this is usually performed solely by the Remote Terminal Unit (RTU) which is located at the root of a power distribution network. The recent rise of distributed power sources, such as photovoltaic generators, raises the demand to increase the frequency of data collection because the output of these distributed generators varies quickly depending on the weather. Increasing data collection frequency in turn requires shortening the time required for data collection. The paper proposes the use of aggregation points for this purpose. An aggregation point can collect sensor data concurrently with other aggregation points as well as with the RTU. The data collection time can be shortened by having the RTU receive data from aggregation points, instead of from all sensors. This approach then poses the problem of finding the optimal location of aggregation points. To solve this problem, the paper proposes a Mixed Integer Linear Problem (MILP) formulation of the problem. The MILP problem can then be solved with off-the-shelf mathematical optimization software. The results of experiments show that the proposed approach is applicable to rather large scale power distribution systems.

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 concurrent systems using this technique. Unlike other related work, which is tailored to specific systems, we are aimed at providing an approach that can be used to verify various kinds of systems against fault tolerance. The main obstacle in model checking is state explosion. To avoid the problem, we design this method so that it can use a symbolic model checking tool called SMV (Symbolic Model Verifier). 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 modeled as a guarded command program, we design a modeling language 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 feasibility of the method.

In automotive control systems, the potential risks of software defects have been increasing due to growing software complexity driven by advances in electric-electronic control. Some kind of defects such as race conditions can rarely be detected by testing or simulations because these defects manifest themselves only in some rare executions. Model checking, which employs an exhaustive state-space exploration, is effective for detecting such defects. This paper reports our approach to applying model checking techniques to real-world automotive control programs. It is impossible to directly model check such programs because of their large size and high complexity; thus, it is necessary to derive, from the program under verification, a model that is amenable to model checking. Our approach uses the SPIN model checker as well as in-house tools that facilitate this process. One of the key features implemented in these tools is boundary-adjustable program slicing, which allows the user to specify and extract part of the source code that is relevant to the verification problem of interest. The conversion from extracted code into Promela, SPIN's input language, is performed using one of the tools in a semi-automatic manner. This approach has been used for several years in practice and found to be useful even when the code size of the software exceeds 400 KLOC.

In this paper, we propose an unbounded model checking method for feature interaction verification for telecommunication systems. Unbounded model checking is a SAT-based verification method and has attracted recent attention as a powerful approach. The interpolation-based approach is one of the most promising unbounded model checking methods and has been proven to be effective for hardware verification. However, the application of unbounded model checking to asynchronous systems, such as telecommunication systems, has rarely been practiced. This is because, with the conventional encoding, the behavior of an asynchronous system can only be represented as a large propositional formula, thus resulting in large computational cost. To overcome this problem we propose to use a new scheme for encoding the behavior of the system and adapt the unbounded model checking algorithm to this encoding. By exploiting the concurrency of an asynchronous system, this encoding scheme allows a very concise formula to represent system's behavior. To demonstrate the effectiveness of our approach, we conduct experiments where 21 pairs of telecommunication services are verified using several methods including ours. The results show that our approach exhibits significant speed-up over unbounded model checking using the traditional encoding.

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.