In a distributed system, the protocol entities must exchange some data values and synchronization messages in order to ensure the temporal ordering of the events described in a service specification for the distributed system. It is desirable that a correct protocol specification can be derived automatically from a given service specification. In this paper, we propose an algorithm which synthesizes automatically a correct protocol specification from a service specification described as a Marked Graph with Registers (MGR) model and resources (registers and gates) allocation information. This model has a finite control modeled as a marked graph. Therefore, parallel events can be described. In our method, to minimize the number of the exchanged messages, we use a procedure to calculate an optimum solution for 0-1 integer linear programming problems. The number of the steps which each protocol entity needs to simulate one transition in the service specification is also minimized. Ways to avoiding conflict of registers are also described. Our approach has the following advantages. First, parallel events can be described in a service specification. Secondly, many practical systems can be described in the MGR model. Finally, at the protocol specification level, we can understand what events can be executed in parallel.

Java is one of important program language today. In Java, in order to build sound software, we have to carefully implement two fundamental methods hashCode and equals. This requirement, however, is not easy to follow in real software development. Some existing studies for ensuring the correctness of these two methods rely on static analysis, which are limited to loop-free programs. This paper proposes a new solution to this important problem, using software analysis workbench (SAW), an open source tool. The efficiency is evaluated through experiments. We also provide a useful situation where cost of regression testing is reduced when program refactoring is conducted.

For the Internet, system developers often have to estimate the QoS by simulation techniques or mathematical analysis. Probabilistic model checking can evaluate performance, dependability and stability of information processing systems with random behaviors. We apply a hybrid analysis approach onto real-time distributed systems. In the hybrid analysis approach, we perform stepwise analysis using probabilistic models of target systems in different abstract levels. First, we create a probabilistic model with detailed behavior of the system (called detailed model), and apply simulation on the detailed model. Next, based on the simulation results, we create a probabilistic model in an abstract level (called simplified model). Then, we verify qualitative properties using the probabilistic model checking techniques. This prevents from state-explosion. We evaluate the validity of our approach by comparing to simulation results of NS-2 using a case study of a video data streaming system. The experiments show that the result of the proposed approach is very close to that of NS-2 simulation. The result encourages the approach is useful for the performance analysis on various domain.

Model checking techniques are useful for design of high-reliable information systems. The well-known problem of state explosion, however, might occur in model checking of large systems. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques have been proposed. Some of them are based on CounterExample-Guided Abstraction Refinement (CEGAR) loop technique proposed by E. Clarke et al.. This paper proposes a concrete abstraction technique for timed automata used in model checking of real time systems. Our technique is based on CEGAR, in which we use a counter example as a guide to refine the abstract model. Although, in general, the refinement operation is applied to abstract models, our method modifies the original timed automaton. Next, we generate refined abstract models from the modified automaton. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.