Kokichi Futatsugi worked for JAIST (Japan Advanced Institute of Science and Technology, Nomi, Japan) from 1993 to 2017 as a professor and is a professor emeritus at JAIST. Professor Futatsugi now has a research position at NTT DATA ARC AL (NTT DATA ARC Advanced Laboratory, Yokohama, Japan). He worked for ETL (Electrotechnical Laboratory of Japanese Government) from 1975 to 1993, and stayed at SRI (Stanford Research Institute, Menlo Park, California) from 1983 to 1984 as an International Fellow. e-mail: futatsugi_AT_jaist.ac.jp

 Specialities

Formal Methods, System Verification, Language Design, Software Engineering

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:

• declarative and wide-spectrum: easy to read and understand, having simple semantics supporting the application of formal methods, and integrating specification and programming within the language;
  
• highly modular, reusable, and adaptable: so that programming large systems can be done as much as possible by combining and adapting small modules that are easy to understand and maintain;
  
• concurrent and cooperative: supporting the decentralized solution of problems by means of concurrent interaction and communication among components;
  
• formal and verifiable: supporting the formal semantics that is succinct enough for supporting transparent verification.

The following includes some research topics Professor Futatsugi is pursuing in order to achieve the above mentioned goals.

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.

 Publications

Major English publications of Professor Futatsugi can be found at DBLP: Kokichi Futatsugi or Kokichi FUTATSUGI - Google Scholar.

 Current Research Interests

Specification Verification, Formal Methods, Language Design, CafeOBJ, Security and Safety, Software Engineering