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

Comprehensive List of Researchers "Information Knowledge"

Department of Information Engineering

Software Science and Technology Group
Assistant Professor
M. of Engineering
Research Field
Formal specification / Software development / Program verification

Current Research

Software Development with Formal Specification

We are engaged in the research of software development using formal specification description. In particular, we have been researching a method of efficiently developing software with high reliability using algebraic specification, which is one kind of formal specification. Strict specification can be described by using algebraic specification, but description and comprehension take time, and acquisition is difficult. Therefore, it is necessary to improve the facility of description and the comprehension of algebraic specification.


We are currently researching the support of software porting using algebraic specification. Computer systems have started to be used in various platforms, and much work to port one set of software to various platforms is being done. To use the software operated in a certain environment in a different environment, modification is required based on the environment. To shorten the computer system's development period and to decrease development cost, cost reduction of software porting is needed. Our research aims to achieve an efficient porting support environment. Using algebraic specification, this method can be expected to reduce software porting cost and improve the development speed of software systems. When the platform changes, software specifications should change the part that depends on the platform. In this technique, porting is supported by using platform and software specifications. Both specifications are described algebraically. The API specification, the parameter limitations of the differences between hardware, etc. are described in platform specifications. Porting that holds the correspondence becomes possible because it uses an algebraic specification description method for both the software and platform specifications. It only has to prepare a platform specification for each platform once. The procedure follows for porting software specifications developed by using this technique's porting support environment on a certain platform and the program to another platform. The procedure of porting by this technique is as follows.
  • Extraction of platform specification differences
  • Automatic change in software specifications based on platform specification differences
  • Generation of program templates from software specifications and program differences

Contradiction might be caused when porting software to another platform even if intended to be platform-independent. Establishing a method for detecting contradiction on specifications is necessary.
Figure : Support of software porting using algebraic specificaiton

Figure : Support of software porting using algebraic specificaiton


  • Takeshi Hamaguchi finished the doctorate course in Nagoya University in 1995.
  • He was a Res. Assoc. of Graduate School of Engineering in Nagoya University, from 1995 to 2003.
  • He was a Res. Assoc. of Graduate School of Information Science, Nagoya University, from 2003 to 2007.
  • Since 2007, he has been a Assistant Professor of Graduate School of Information Science, Nagoya University.

Academic Societies



  1. Error Description on Algebraic Specification and Its Automatic Addition, IEICE Trans. Inf. & Syst., vol. J78-D-I, no. 3, 1995.