Current Research

Theory and Practice of Concurrency for Reliable Network Computing

Summary:'Network Computing' is the process of performing distributed concurrent computation over many machines inter-connected by computer network. Network computing, particularly over the Internet, becomes one of the essential fundamentals in the current society.'Reliability' is the key issue with more importance in software for network computing. The particular feature in network computing software is that intermediate states are observable by communication with the environment, while in the conventional sequential software only the initial and final states are observable. In addition to this, the distributed control is an inherent source of nondeterminism.
The above features of distributed computing motivates a new computation model for improving reliability, where computation is modeled based on communications. We study the communicating processes being formalized as process calculi to abstractly model and analyze the behavior of network computing software.
(1) Timed Extension of communicating processes: We give a formal characterization of time passage in communicating processes. We study the pi-calculus to have a congruence property of equivalences in the calculus.
(2) Behavioral Model of Web Applications: We model behavior of web applications with dynamic features by communicating processes. By name-passing in process calculi, the execution flow of web applications is better captured. We study reliability and security of web applications.
(3) Programming Languages based on communicating processes: We are developing a programming language in the form of communicating processes. This eases the behavioral analysis in the network environment to improve the reliability of network programs.
(4) Behavioral Model for Embedded Systems: We study component-based software for embedded systems by modeling the behavior with communicating processes.
In embedded systems, timed property and resource limitation require detailed analysis for control software.
We apply process calculi for abstract modeling of embedded system. This enables to apply various formal techniques to improve reliability of embedded systems.
Prospects: We consider the communicating process model in the form of process calculi is promising to enable the formal analysis by focusing following two types of software:
(1) Web Applications: Web applications becomes more dynamic and more distributed as seen in the Ajax framework. We study the development and analysis techniques by modeling such web applications by process calculi for better reliability and security.
(2) Embedded Systems: In small scale time-sensitive software, we apply process calculi with time extension. By giving formal proofs, we expect to improve reliability of embedded systems.