I would like to introduce myself to you. I am now studying computer science at Keio University in Japan, from which I will get the degree of Doctor of Philosophy in March, 1996.

I first want to outline my PhD thesis. The thesis constructs a theory to formulate temporal aspects of distributed systems through developing a new process calculus and its two further expressive extensions.

The calculus is defined by extending existing non-timed process calculi. It provides a simple but powerful framework for describing synchronously communicating time-dependent processes. It has two new constructions for delayed processing and timed restriction, in addition to operational constructors found in many non-timed process calculi: sequential execution, parallel composition, synchronous communication, message scope restriction, and recursion definition. As a verification method, we develop several time-sensitive equation theories for processes and study their basic properties.

The two extensions reinforce the framework with the ability to express temporal properties of distributed computing. One of the extensions consists of some supplementary language constructors concerning with non-blocking message sending and process locations. It can model the notion of asynchrony and delay in communication among remotely located processes. On the basis of it, we give algebraic order relations which can order two behaviorally equivalent processes with respect to their relative execution speeds. The relations offer suitable verification and optimization techniques for asynchronously communicating systems, in particular very-large distributed systems.

The other extension lets the original calculus embody the expressive capability of multiple inaccurate clocks. It allows us to analyze the influence of inaccuracy and difference among physical clocks upon distributed systems. We develop an equivalence relation which can equate two processes when their behaviors are completely matched and their timings are different within a given bound. It provides a method to verify distributed systems with time uncertainties and non-strict time constraints.

We present some comparison with related work and discuss open problems and further applications of this work.

After getting PhD thesis, I plan to reseach a theoretical framework to specify open distributed systems and a method to develope these systems.

Future distributed systems are considered as dynamical and open systems. In these systems, the structure of communication networks and computers are continusouly changings. For example, new subsystems and new services will always come into an open distributed system in runtime. As a result, the system itself is always incomplete and evolving. Also, the systems have to cooperate with their external world, called real-world, which include various non-computational entities such as sensors, actuators, humans, and nature. To cooperate with the real-world, future distributed systems need to be self-defensed, self-controled, and open to their external entities. I believe that it is important and necessary to model and analyze open distributed systems theoretically. However, most of the existing theories for computation, including distributed computing are essentially closed. That is to say, they can reason about only the closed systems which everything is well-defined and static. Therefore, they cannot deal with open systems which contain various unknown information and change dynamically. I believe that it is important and necessary to construct a new theory for reasoning about evolutional aspects of open distributed systems interacting with the real world.