TOP > Research > Department of Systems and Social Informatics > Department of Information Engineering > Software Science and Technology Group > YUEN, Shoji

Comprehensive List of Researchers "Information Knowledge"

Department of Information Engineering

YUEN, Shoji
Software Science and Technology Group
Dr. of Engineering
Research Field
Concurency / Communicating processes / Program verification

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.

Figure : Software veri.cation by communicating processes

Figure : Software veri.cation by communicating processes


  • 1992 Research Associate, School of Engineering, Nagoya University
  • 1999 Associate Professor, Center for Information Media Studies, Nagoya University
  • 2003 Associate Professor, Graduate School of Information Science, Nagoya University

Academic Societies

  • ACM
  • IPSJ


  1. Process languages with discrete relative time based on the Ordered SOS format and rooted eager bisimulation, Journal of Logic and Algebraic Programming, Vol. 60-61, 2004, pages 401-460.
  2. Web Automata: A Behavioral Model of Web Applications Based on the MVC, Computer Software, Vol.22, 2005, pages 44-57.
  3. Testing Theory for Probabilistic Processes, Information and Computation, Vol. 154, 1999, pages 93-148.