Professor Futatsugi assumed a concurrent position at JAIST in April 1992 while he was working mainly for ETL (Electrotechnical Lab.) as Chief Senior Researcher. In April 1993, he starts to work mainly for JAIST. He received the Ph.D. degree from Tohoku University, and joined ETL in 1975. Professor Futatsugi stayed at SRI International as an International Fellow for one year from 1983 to 1984.  Professor Futatsugi was the Dean of Graduate School of Information Science, JAIST from 2001 to 2003.

Specialities :

Formal Methods, Software Engineering, Language Design, Concurrent and Cooperative Programming

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;
  
• concurrent and cooperative: supporting the decentralized solution of problems by means of concurrent interaction and communication between different components.

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.

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.

CAFE is the name of an environment for CafeOBJ language. The main purpose of CAFE is to provide a practical environment for development of formal specifications in CafeOBJ language. 

Selected Publications

• Kokichi Futatsugi, Joseph A. Goguen and Kazuhiro Ogata: Verifying Design with Proof Scores, 1st VSTTE, LNCS 4171, Springer, pp.277-290, 2008.
• Kazuhiro Ogata and Kokichi Futatsugi: Modeling and verification of real-time systems based on equations, Science of Computer Programming, 66(2): 162-180, Elsevier, 2007.
• Kokichi FUTATSUGI, Verifying Specifications with Proof Scores in CafeOBJ (an invited keynote paper at ASE 2006), Proc. of 21st IEEE International Conference on Automated Software Engineering, pp. 3-10, 2006.
• Formal Methods in CafeOBJ. FLOPS 2002, Lecture Notes in Computer Science, 2441, Springer, pp.1-20, 2002. (invited paper)
  
• CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, World Scientific, AMAST Series in Computing 6, 1998. (with Razvan Diaconescu)
  
• An Overview of CAFE Specification Environment, Proc. 1st IEEE Intl. Conf. of Formal Engineering Methods ( ICFEM 1997), pp.170-181, 1997. (invited paper, with A.Nakagawa)
  

Current Research

CafeOBJ, CAFE Language Environment; Formal Methods, Language Design; Behavioral Specification(Hidden Algebra), Rewriting Logic; Formal Specification and Verification of Component Based Sytems, Security and Safety Sytems, and Agent Sytems