One of the calculi is defined by extending existing non-timed process calculi, for example CCS. 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 other calculi are constructed by extending the calculus with the ability to express temporal properties of distributed computing. One of the extended calculi 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 extended calculi 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.
Now I am trying to develop 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.
I would like to be grateful if you could give me any comment on my research, via Email: email@example.com