Professor Futatsugi is now working at Research Center for Software Verification of JAIST (Japan Advanced Institute of Science and Technology) as a Research Professor. He got a concurrent professorship at JAIST in April 1992 while he was working mainly for ETL (Electrotechnical Laboratory) of Japanese Government as a Chief Senior Researcher. In April 1993, he starts to work mainly for JAIST as a full professor, and was the Dean of Graduate School of Information Science of JAIST from 2001 to 2003. He received the Ph.D. degree from Tohoku University, Sendai, Japan and joined ETL in 1975. He stayed at SRI International, California, USA as an International Fellow for one year from 1983 to 1984.
Professor Futatsugi's primary research goal is to design and
develop new computer languages which can open up new application areas,
and/or improve the current software technology. A wish list of
desirable characteristics of new computer languages includes:
Algebraic Specification Method is one of the major formal methods. Systems are specified/designed based on algebraic modeling, and the specifications/designs are tested/verified against requirements using algebraic techniques. Recent developments of algebraic specification show that evolution of systems can be neatly modeled by rewriting logic algebraically. It also shows that behaviour of systems can also be nicely modeled by hidden algebras. Professor Futatsugi is trying to develop a new algebraic formal method which provides an unified basis for system design, specification, and verification.
CafeOBJ is multi-paradigm specification language which is a modern successor of the most noted algebraic specification language OBJ. OBJ language has been designed and developed by K.Futatsugi, J.Goguen, J.-P.Jouannaud, and J.Meseguer at SRI International in 1984. Professor Futatsugi have been trying to apply OBJ in many fields. Based on these experiences, CafeOBJ is designed and implemented by incorporating several important specification paradigms like behaviour, concurrency, object-orientation. CafeOBJ adopts hidden algebra and rewriting logic as its underlying logics. The application areas considered includes design and validation of fundamental and important systems such as component based systems, security/safety systems, computer language systems, etc. . In this context, interactive (semi-automatic) verification of requirements for systems should be the most challenging topic.