Formal Methods with CafeOBJ

Kokichi Futatsugi, Chair of Language Design

Graduate School of Information Science, JAIST.

Fri Dec 10 11:00:00 NZDT 2004 in Room 031, MSCS

Abstract

Formal methods are still expected to improve the practice of software engineering. The areas in which formal methods will play important roles include at least: (1) distributed component software, (2) network/system security, (3) embedded systems. Formal methods are better supported by formal specification languages equipped with formal verification capability.

CafeOBJ is a formal specification language equipped with verification methodologies based on algebraic specification technique. CafeOBJ is an executable wide spectrum language based on multiple logical foundations; mainly based on initial and hidden algebras. Static aspects of systems are specified in terms of initial algebras, and dynamic aspects of systems are specified in terms of hidden algebras.

CafeOBJ is the first algebraic specification language which incorporates observational (or behavioral) specifications based on hidden algebras in a serious way. Observational specifications in CafeOBJ can be seen as a nice combination of static and dynamic specifications, and facilitate natural and transparent specification and verification of complex systems.

This talk explains minimal fundamentals of CafeOBJ, an interactive equational proof method with it, and some practical applications of the method.