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.

Responsive communication protocols must incorporate both real-time and fault-tolerant properties. In this paper, we propose a new method for detecting design faults in specifications of responsive communication protocols based on real-time temporal logic. We also present a case study where a connection establishment protocol for a plant control system is dealt with.

This paper discusses how a backup virtual path (VP) between each pair of a source node and a destination node is set up such that when some nodes and links in primary VP's fail, primary VP's are changed to backup VP's rapidly. Then, this paper proposes a multiagent-based method for such rapid restoration from primary VP's to backup VP's. The proposed method consists of the following three steps. The first step enumerates candidates of backup VP between each pair of a source node and a destination node. In the second step, capacities of shared links in backup VP candidates between different pairs of a source node and a destination node are obtained. The last step determines a backup VP with the minimum capacities of shared links between each pair of a source node and a destination node. The proposed method has potentially good adaptability for change of both network resource such as topology and link capacity and resource requirements such as capacities of primary VP and backup VP.

The responsiveness verification of a given communication protocol is to check whether the given protocol can recover from any abnormal state to a normal state within a permissible time or not. In order to make practical discussions, we assume that the lower and upper bounds of execution time are given for each message transfer and event. We propose a new responsiveness verification method which executes several events concurrently based on residual times of events, and develop a simulator which implements the proposed method. Then we present an experience which applies the simulator to the design of an actual connection establishment protocol for a certain plant control system. The system adopts the client server model and real time constraints exist on connection establishments. In the experience, we first specify the protocol straightforwardly. Then we apply the simulator to the specification and detect design faults against responsiveness. Next, we revise the specification successfully based on the state sequences generated by the simulator. The results of the experience conclude that the proposed method is effective for the case study.

We propose a timed reachability analysis method in order to generate system states of two classes of EFSM-based communication protocols; one class C1 consists of events such that the lower and upper bounds are all the same and the other class C2 consists of events such that they may be different. The proposed method enumerates only sequences of system states that are obtained through parallel execution of all possible events. Then, in order to evaluate the efficiency of the proposed method, we develop a verification tool based on the proposed method, and then apply the tool to a broadcasting protocol. The experimental results show that the total number of states generated by the proposed method is much less than that by the previous method.